- Started with
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
19.4
- Using strategy
rm 19.4
- Applied div-sub to get
\[\color{red}{\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}} \leadsto \color{blue}{\frac{x.im \cdot y.re}{y.re \cdot y.re + y.im \cdot y.im} - \frac{x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}}\]
19.5
- Using strategy
rm 19.5
- Applied associate-/l* to get
\[\frac{x.im \cdot y.re}{y.re \cdot y.re + y.im \cdot y.im} - \color{red}{\frac{x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}} \leadsto \frac{x.im \cdot y.re}{y.re \cdot y.re + y.im \cdot y.im} - \color{blue}{\frac{x.re}{\frac{y.re \cdot y.re + y.im \cdot y.im}{y.im}}}\]
20.2
- Applied simplify to get
\[\frac{x.im \cdot y.re}{y.re \cdot y.re + y.im \cdot y.im} - \frac{x.re}{\color{red}{\frac{y.re \cdot y.re + y.im \cdot y.im}{y.im}}} \leadsto \frac{x.im \cdot y.re}{y.re \cdot y.re + y.im \cdot y.im} - \frac{x.re}{\color{blue}{\frac{{y.re}^2 + y.im \cdot y.im}{y.im}}}\]
20.2
- Using strategy
rm 20.2
- Applied *-un-lft-identity to get
\[\frac{x.im \cdot y.re}{\color{red}{y.re \cdot y.re + y.im \cdot y.im}} - \frac{x.re}{\frac{{y.re}^2 + y.im \cdot y.im}{y.im}} \leadsto \frac{x.im \cdot y.re}{\color{blue}{1 \cdot \left(y.re \cdot y.re + y.im \cdot y.im\right)}} - \frac{x.re}{\frac{{y.re}^2 + y.im \cdot y.im}{y.im}}\]
20.2
- Applied times-frac to get
\[\color{red}{\frac{x.im \cdot y.re}{1 \cdot \left(y.re \cdot y.re + y.im \cdot y.im\right)}} - \frac{x.re}{\frac{{y.re}^2 + y.im \cdot y.im}{y.im}} \leadsto \color{blue}{\frac{x.im}{1} \cdot \frac{y.re}{y.re \cdot y.re + y.im \cdot y.im}} - \frac{x.re}{\frac{{y.re}^2 + y.im \cdot y.im}{y.im}}\]
17.6
- Applied simplify to get
\[\frac{x.im}{1} \cdot \color{red}{\frac{y.re}{y.re \cdot y.re + y.im \cdot y.im}} - \frac{x.re}{\frac{{y.re}^2 + y.im \cdot y.im}{y.im}} \leadsto \frac{x.im}{1} \cdot \color{blue}{\frac{y.re}{{y.re}^2 + y.im \cdot y.im}} - \frac{x.re}{\frac{{y.re}^2 + y.im \cdot y.im}{y.im}}\]
17.6