- Split input into 2 regimes
if (- (/ (/ x.im (hypot y.im y.re)) (/ (hypot y.im y.re) y.re)) (/ (/ (* x.re y.im) (hypot y.im y.re)) (* (sqrt (hypot y.im y.re)) (sqrt (hypot y.im y.re))))) < -1.9988990777228786e+296 or 7.145262622020625e+256 < (- (/ (/ x.im (hypot y.im y.re)) (/ (hypot y.im y.re) y.re)) (/ (/ (* x.re y.im) (hypot y.im y.re)) (* (sqrt (hypot y.im y.re)) (sqrt (hypot y.im y.re)))))
Initial program 54.3
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
Initial simplification54.3
\[\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-sqrt54.3
\[\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-identity54.3
\[\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-frac54.3
\[\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))_*}}}\]
Simplified54.3
\[\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))_*}}\]
Simplified52.1
\[\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/52.1
\[\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}^*}}\]
Simplified52.1
\[\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}^*}\]
Taylor expanded around 0 40.4
\[\leadsto \frac{\color{blue}{-1 \cdot x.re}}{\sqrt{y.im^2 + y.re^2}^*}\]
Simplified40.4
\[\leadsto \frac{\color{blue}{-x.re}}{\sqrt{y.im^2 + y.re^2}^*}\]
if -1.9988990777228786e+296 < (- (/ (/ x.im (hypot y.im y.re)) (/ (hypot y.im y.re) y.re)) (/ (/ (* x.re y.im) (hypot y.im y.re)) (* (sqrt (hypot y.im y.re)) (sqrt (hypot y.im y.re))))) < 7.145262622020625e+256
Initial program 20.4
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
Initial simplification20.4
\[\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-sqrt20.4
\[\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-identity20.4
\[\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-frac20.4
\[\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))_*}}}\]
Simplified20.4
\[\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))_*}}\]
Simplified9.8
\[\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/9.7
\[\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}^*}}\]
Simplified9.7
\[\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 add-sqr-sqrt9.9
\[\leadsto \frac{\frac{y.re \cdot x.im - x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}{\color{blue}{\sqrt{\sqrt{y.im^2 + y.re^2}^*} \cdot \sqrt{\sqrt{y.im^2 + y.re^2}^*}}}\]
- Using strategy
rm Applied div-sub9.9
\[\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{\sqrt{y.im^2 + y.re^2}^*} \cdot \sqrt{\sqrt{y.im^2 + y.re^2}^*}}\]
Applied div-sub9.9
\[\leadsto \color{blue}{\frac{\frac{y.re \cdot x.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{\sqrt{y.im^2 + y.re^2}^*} \cdot \sqrt{\sqrt{y.im^2 + y.re^2}^*}} - \frac{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{\sqrt{y.im^2 + y.re^2}^*} \cdot \sqrt{\sqrt{y.im^2 + y.re^2}^*}}}\]
Simplified1.3
\[\leadsto \color{blue}{\frac{\frac{x.im}{\sqrt{y.im^2 + y.re^2}^*}}{\frac{\sqrt{y.im^2 + y.re^2}^*}{y.re}}} - \frac{\frac{x.re \cdot y.im}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{\sqrt{y.im^2 + y.re^2}^*} \cdot \sqrt{\sqrt{y.im^2 + y.re^2}^*}}\]
- Recombined 2 regimes into one program.
Final simplification7.6
\[\leadsto \begin{array}{l}
\mathbf{if}\;\frac{\frac{x.im}{\sqrt{y.im^2 + y.re^2}^*}}{\frac{\sqrt{y.im^2 + y.re^2}^*}{y.re}} - \frac{\frac{y.im \cdot x.re}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{\sqrt{y.im^2 + y.re^2}^*} \cdot \sqrt{\sqrt{y.im^2 + y.re^2}^*}} \le -1.9988990777228786 \cdot 10^{+296}:\\
\;\;\;\;\frac{-x.re}{\sqrt{y.im^2 + y.re^2}^*}\\
\mathbf{elif}\;\frac{\frac{x.im}{\sqrt{y.im^2 + y.re^2}^*}}{\frac{\sqrt{y.im^2 + y.re^2}^*}{y.re}} - \frac{\frac{y.im \cdot x.re}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{\sqrt{y.im^2 + y.re^2}^*} \cdot \sqrt{\sqrt{y.im^2 + y.re^2}^*}} \le 7.145262622020625 \cdot 10^{+256}:\\
\;\;\;\;\frac{\frac{x.im}{\sqrt{y.im^2 + y.re^2}^*}}{\frac{\sqrt{y.im^2 + y.re^2}^*}{y.re}} - \frac{\frac{y.im \cdot x.re}{\sqrt{y.im^2 + y.re^2}^*}}{\sqrt{\sqrt{y.im^2 + y.re^2}^*} \cdot \sqrt{\sqrt{y.im^2 + y.re^2}^*}}\\
\mathbf{else}:\\
\;\;\;\;\frac{-x.re}{\sqrt{y.im^2 + y.re^2}^*}\\
\end{array}\]