\(\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)}{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re} - \log \left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right) \cdot 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)\]
15.9
- 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}}}}\]
17.3
- Using strategy
rm 17.3
- 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
- Using strategy
rm 17.0
- Applied add-exp-log 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}}}{{\color{red}{\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{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}{{\color{blue}{\left(e^{\log \left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right)}\right)}}^{y.re}}}\]
17.0
- 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{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}{\color{red}{{\left(e^{\log \left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right)}\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{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}{\color{blue}{e^{\log \left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right) \cdot y.re}}}}\]
17.0
- Applied div-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)}{\color{red}{\frac{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re}}}{e^{\log \left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right) \cdot 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)}{\color{blue}{e^{y.im \cdot \tan^{-1}_* \frac{x.im}{x.re} - \log \left(\sqrt{{x.re}^2 + x.im \cdot x.im}\right) \cdot y.re}}}\]
15.9