Initial program 25.6
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
Applied simplify25.6
\[\leadsto \color{blue}{\frac{y.re \cdot x.im - x.re \cdot y.im}{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
- Using strategy
rm Applied add-sqr-sqrt25.6
\[\leadsto \frac{y.re \cdot x.im - 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-identity25.6
\[\leadsto \frac{\color{blue}{1 \cdot \left(y.re \cdot x.im - 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-frac25.7
\[\leadsto \color{blue}{\frac{1}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}} \cdot \frac{y.re \cdot x.im - x.re \cdot y.im}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}\]
Applied simplify25.7
\[\leadsto \color{blue}{\frac{1}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \frac{y.re \cdot x.im - x.re \cdot y.im}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
Applied simplify16.5
\[\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 div-sub16.5
\[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \color{blue}{\left(\frac{x.im \cdot y.re}{\sqrt{y.im^2 + y.re^2}^*} - \frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}\right)}\]
- Using strategy
rm Applied add-cube-cbrt16.8
\[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \left(\frac{x.im \cdot y.re}{\sqrt{y.im^2 + y.re^2}^*} - \color{blue}{\left(\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\right) \cdot \sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}}\right)\]
Applied add-sqr-sqrt16.9
\[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \left(\frac{x.im \cdot y.re}{\color{blue}{\sqrt{\sqrt{y.im^2 + y.re^2}^*} \cdot \sqrt{\sqrt{y.im^2 + y.re^2}^*}}} - \left(\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\right) \cdot \sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\right)\]
Applied times-frac9.7
\[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \left(\color{blue}{\frac{x.im}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}} \cdot \frac{y.re}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}}} - \left(\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\right) \cdot \sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\right)\]
Applied prod-diff9.8
\[\leadsto \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot \color{blue}{\left((\left(\frac{x.im}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}}\right) \cdot \left(\frac{y.re}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}}\right) + \left(-\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \left(\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\right)\right))_* + (\left(-\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\right) \cdot \left(\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\right) + \left(\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \left(\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\right)\right))_*\right)}\]
Applied distribute-lft-in9.8
\[\leadsto \color{blue}{\frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot (\left(\frac{x.im}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}}\right) \cdot \left(\frac{y.re}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}}\right) + \left(-\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \left(\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\right)\right))_* + \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot (\left(-\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\right) \cdot \left(\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\right) + \left(\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \left(\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\right)\right))_*}\]
Applied simplify9.5
\[\leadsto \color{blue}{\frac{(\left(\frac{y.re}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}}\right) \cdot \left(\frac{x.im}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}}\right) + \left(\frac{-y.im}{\frac{\sqrt{y.im^2 + y.re^2}^*}{x.re}}\right))_*}{\sqrt{y.im^2 + y.re^2}^*}} + \frac{1}{\sqrt{y.im^2 + y.re^2}^*} \cdot (\left(-\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\right) \cdot \left(\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\right) + \left(\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \left(\sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}} \cdot \sqrt[3]{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}\right)\right))_*\]
Applied simplify1.2
\[\leadsto \frac{(\left(\frac{y.re}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}}\right) \cdot \left(\frac{x.im}{\sqrt{\sqrt{y.im^2 + y.re^2}^*}}\right) + \left(\frac{-y.im}{\frac{\sqrt{y.im^2 + y.re^2}^*}{x.re}}\right))_*}{\sqrt{y.im^2 + y.re^2}^*} + \color{blue}{\frac{0}{\sqrt{y.im^2 + y.re^2}^*}}\]
