\(\frac{1 - \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot \left(\frac{1}{2} \cdot \left(y.re \cdot y.re\right)\right)}{{\left(e^{y.im}\right)}^{\left(\tan^{-1}_* \frac{x.im}{x.re}\right)}} \cdot {\left(\sqrt{x.im \cdot x.im + {x.re}^2}\right)}^{y.re}\)
- Started with
\[e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \cos \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)\]
16.6
- Applied simplify to get
\[\color{red}{e^{\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.re - \tan^{-1}_* \frac{x.im}{x.re} \cdot y.im} \cdot \cos \left(\log \left(\sqrt{x.re \cdot x.re + x.im \cdot x.im}\right) \cdot y.im + \tan^{-1}_* \frac{x.im}{x.re} \cdot y.re\right)} \leadsto \color{blue}{\frac{\cos \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re} + \log \left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right) \cdot y.im\right)}{\frac{{\left(e^{y.im}\right)}^{\left(\tan^{-1}_* \frac{x.im}{x.re}\right)}}{{\left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right)}^{y.re}}}}\]
16.8
- Using strategy
rm 16.8
- Applied pow-exp to get
\[\frac{\cos \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re} + \log \left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right) \cdot y.im\right)}{\frac{\color{red}{{\left(e^{y.im}\right)}^{\left(\tan^{-1}_* \frac{x.im}{x.re}\right)}}}{{\left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right)}^{y.re}}} \leadsto \frac{\cos \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re} + \log \left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right) \cdot y.im\right)}{\frac{\color{blue}{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}}{{\left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right)}^{y.re}}}\]
17.0
- Applied taylor to get
\[\frac{\cos \left(y.re \cdot \tan^{-1}_* \frac{x.im}{x.re} + \log \left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right) \cdot y.im\right)}{\frac{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}{{\left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right)}^{y.re}}} \leadsto \frac{1 - \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot \left(y.im \cdot \left(\log x.re \cdot y.re\right)\right) + \frac{1}{2} \cdot \left({\left(\tan^{-1}_* \frac{x.im}{x.re}\right)}^2 \cdot {y.re}^2\right)\right)}{\frac{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}{{\left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right)}^{y.re}}}\]
22.5
- Taylor expanded around 0 to get
\[\frac{\color{red}{1 - \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot \left(y.im \cdot \left(\log x.re \cdot y.re\right)\right) + \frac{1}{2} \cdot \left({\left(\tan^{-1}_* \frac{x.im}{x.re}\right)}^2 \cdot {y.re}^2\right)\right)}}{\frac{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}{{\left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right)}^{y.re}}} \leadsto \frac{\color{blue}{1 - \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot \left(y.im \cdot \left(\log x.re \cdot y.re\right)\right) + \frac{1}{2} \cdot \left({\left(\tan^{-1}_* \frac{x.im}{x.re}\right)}^2 \cdot {y.re}^2\right)\right)}}{\frac{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}{{\left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right)}^{y.re}}}\]
22.5
- Applied taylor to get
\[\frac{1 - \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot \left(y.im \cdot \left(\log x.re \cdot y.re\right)\right) + \frac{1}{2} \cdot \left({\left(\tan^{-1}_* \frac{x.im}{x.re}\right)}^2 \cdot {y.re}^2\right)\right)}{\frac{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}{{\left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right)}^{y.re}}} \leadsto \frac{1 - \left(0 + \frac{1}{2} \cdot \left({\left(\tan^{-1}_* \frac{x.im}{x.re}\right)}^2 \cdot {y.re}^2\right)\right)}{\frac{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}{{\left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right)}^{y.re}}}\]
14.3
- Taylor expanded around 0 to get
\[\frac{1 - \left(\color{red}{0} + \frac{1}{2} \cdot \left({\left(\tan^{-1}_* \frac{x.im}{x.re}\right)}^2 \cdot {y.re}^2\right)\right)}{\frac{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}{{\left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right)}^{y.re}}} \leadsto \frac{1 - \left(\color{blue}{0} + \frac{1}{2} \cdot \left({\left(\tan^{-1}_* \frac{x.im}{x.re}\right)}^2 \cdot {y.re}^2\right)\right)}{\frac{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}{{\left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right)}^{y.re}}}\]
14.3
- Applied simplify to get
\[\frac{1 - \left(0 + \frac{1}{2} \cdot \left({\left(\tan^{-1}_* \frac{x.im}{x.re}\right)}^2 \cdot {y.re}^2\right)\right)}{\frac{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}{{\left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right)}^{y.re}}} \leadsto \frac{1 - \left(\left(\frac{1}{2} \cdot y.re\right) \cdot y.re\right) \cdot \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}{{\left(e^{y.im}\right)}^{\left(\tan^{-1}_* \frac{x.im}{x.re}\right)}} \cdot {\left(\sqrt{x.im \cdot x.im + x.re \cdot x.re}\right)}^{y.re}\]
14.3
- Applied final simplification
- Applied simplify to get
\[\color{red}{\frac{1 - \left(\left(\frac{1}{2} \cdot y.re\right) \cdot y.re\right) \cdot \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot \tan^{-1}_* \frac{x.im}{x.re}\right)}{{\left(e^{y.im}\right)}^{\left(\tan^{-1}_* \frac{x.im}{x.re}\right)}} \cdot {\left(\sqrt{x.im \cdot x.im + x.re \cdot x.re}\right)}^{y.re}} \leadsto \color{blue}{\frac{1 - \left(\tan^{-1}_* \frac{x.im}{x.re} \cdot \tan^{-1}_* \frac{x.im}{x.re}\right) \cdot \left(\frac{1}{2} \cdot \left(y.re \cdot y.re\right)\right)}{{\left(e^{y.im}\right)}^{\left(\tan^{-1}_* \frac{x.im}{x.re}\right)}} \cdot {\left(\sqrt{x.im \cdot x.im + {x.re}^2}\right)}^{y.re}}\]
14.3