Initial program 40.5
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
Initial simplification40.5
\[\leadsto \frac{x.im \cdot y.re - x.re \cdot y.im}{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}\]
- Using strategy
rm Applied add-sqr-sqrt40.5
\[\leadsto \frac{x.im \cdot y.re - x.re \cdot y.im}{\color{blue}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*} \cdot \sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}\]
Applied *-un-lft-identity40.5
\[\leadsto \frac{\color{blue}{1 \cdot \left(x.im \cdot y.re - x.re \cdot y.im\right)}}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*} \cdot \sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
Applied times-frac40.5
\[\leadsto \color{blue}{\frac{1}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}\]
Simplified40.5
\[\leadsto \color{blue}{\frac{1}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
Simplified26.4
\[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \color{blue}{\frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\]
- Using strategy
rm Applied associate-*l/26.3
\[\leadsto \color{blue}{\frac{1 \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*}}\]
Simplified26.3
\[\leadsto \frac{\color{blue}{\frac{y.re \cdot x.im - x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}}{\sqrt{y.im^2 + y.re^2}^*}\]
- Using strategy
rm Applied div-sub26.3
\[\leadsto \frac{\color{blue}{\frac{y.re \cdot x.im}{\sqrt{y.im^2 + y.re^2}^*} - \frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}}{\sqrt{y.im^2 + y.re^2}^*}\]
Applied div-sub26.3
\[\leadsto \color{blue}{\frac{\frac{y.re \cdot x.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*} - \frac{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*}}\]
- Using strategy
rm Applied *-un-lft-identity26.3
\[\leadsto \frac{\frac{y.re \cdot x.im}{\color{blue}{1 \cdot \sqrt{y.im^2 + y.re^2}^*}}}{\sqrt{y.im^2 + y.re^2}^*} - \frac{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*}\]
Applied times-frac7.2
\[\leadsto \frac{\color{blue}{\frac{y.re}{1} \cdot \frac{x.im}{\sqrt{y.im^2 + y.re^2}^*}}}{\sqrt{y.im^2 + y.re^2}^*} - \frac{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*}\]
Simplified7.2
\[\leadsto \frac{\color{blue}{y.re} \cdot \frac{x.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*} - \frac{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*}\]
Initial program 18.6
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
Initial simplification18.6
\[\leadsto \frac{x.im \cdot y.re - x.re \cdot y.im}{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}\]
- Using strategy
rm Applied add-sqr-sqrt18.6
\[\leadsto \frac{x.im \cdot y.re - x.re \cdot y.im}{\color{blue}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*} \cdot \sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}\]
Applied *-un-lft-identity18.6
\[\leadsto \frac{\color{blue}{1 \cdot \left(x.im \cdot y.re - x.re \cdot y.im\right)}}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*} \cdot \sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
Applied times-frac18.6
\[\leadsto \color{blue}{\frac{1}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}\]
Simplified18.6
\[\leadsto \color{blue}{\frac{1}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
Simplified11.6
\[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \color{blue}{\frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\]
- Using strategy
rm Applied associate-*l/11.5
\[\leadsto \color{blue}{\frac{1 \cdot \frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*}}\]
Simplified11.5
\[\leadsto \frac{\color{blue}{\frac{y.re \cdot x.im - x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}}{\sqrt{y.im^2 + y.re^2}^*}\]
- Using strategy
rm Applied div-sub11.5
\[\leadsto \frac{\color{blue}{\frac{y.re \cdot x.im}{\sqrt{y.im^2 + y.re^2}^*} - \frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}}{\sqrt{y.im^2 + y.re^2}^*}\]
Applied div-sub11.5
\[\leadsto \color{blue}{\frac{\frac{y.re \cdot x.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*} - \frac{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*}}\]
- Using strategy
rm Applied associate-/l*2.7
\[\leadsto \frac{\frac{y.re \cdot x.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{y.im^2 + y.re^2}^*} - \frac{\color{blue}{\frac{x.re}{\frac{\sqrt{y.im^2 + y.re^2}^*}{y.im}}}}{\sqrt{y.im^2 + y.re^2}^*}\]