Initial program 25.9
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
- Using strategy
rm Applied div-sub25.9
\[\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}}\]
- Using strategy
rm Applied *-un-lft-identity25.9
\[\leadsto \frac{x.im \cdot y.re}{y.re \cdot y.re + y.im \cdot y.im} - \frac{x.re \cdot y.im}{\color{blue}{1 \cdot \left(y.re \cdot y.re + y.im \cdot y.im\right)}}\]
Applied times-frac24.7
\[\leadsto \frac{x.im \cdot y.re}{y.re \cdot y.re + y.im \cdot y.im} - \color{blue}{\frac{x.re}{1} \cdot \frac{y.im}{y.re \cdot y.re + y.im \cdot y.im}}\]
Simplified24.7
\[\leadsto \frac{x.im \cdot y.re}{y.re \cdot y.re + y.im \cdot y.im} - \color{blue}{x.re} \cdot \frac{y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
Final simplification24.7
\[\leadsto \frac{x.im \cdot y.re}{y.re \cdot y.re + y.im \cdot y.im} - \frac{y.im}{y.re \cdot y.re + y.im \cdot y.im} \cdot x.re\]