Initial program 15.6
\[\frac{\log \left(\sqrt{re \cdot re + im \cdot im}\right) \cdot \log base + \tan^{-1}_* \frac{im}{re} \cdot 0}{\log base \cdot \log base + 0 \cdot 0}\]
- Using strategy
rm Applied add-sqr-sqrt15.6
\[\leadsto \frac{\log \left(\sqrt{re \cdot re + im \cdot im}\right) \cdot \log base + \tan^{-1}_* \frac{im}{re} \cdot 0}{\color{blue}{\sqrt{\log base \cdot \log base + 0 \cdot 0} \cdot \sqrt{\log base \cdot \log base + 0 \cdot 0}}}\]
Applied *-un-lft-identity15.6
\[\leadsto \frac{\color{blue}{1 \cdot \left(\log \left(\sqrt{re \cdot re + im \cdot im}\right) \cdot \log base + \tan^{-1}_* \frac{im}{re} \cdot 0\right)}}{\sqrt{\log base \cdot \log base + 0 \cdot 0} \cdot \sqrt{\log base \cdot \log base + 0 \cdot 0}}\]
Applied times-frac15.6
\[\leadsto \color{blue}{\frac{1}{\sqrt{\log base \cdot \log base + 0 \cdot 0}} \cdot \frac{\log \left(\sqrt{re \cdot re + im \cdot im}\right) \cdot \log base + \tan^{-1}_* \frac{im}{re} \cdot 0}{\sqrt{\log base \cdot \log base + 0 \cdot 0}}}\]
Applied simplify15.6
\[\leadsto \color{blue}{\frac{1}{\sqrt{\log base \cdot \log base}}} \cdot \frac{\log \left(\sqrt{re \cdot re + im \cdot im}\right) \cdot \log base + \tan^{-1}_* \frac{im}{re} \cdot 0}{\sqrt{\log base \cdot \log base + 0 \cdot 0}}\]
Applied simplify15.6
\[\leadsto \frac{1}{\sqrt{\log base \cdot \log base}} \cdot \color{blue}{\frac{\log base \cdot \log \left(\sqrt{im \cdot im + re \cdot re}\right)}{\sqrt{\log base \cdot \log base}}}\]
Initial program 29.2
\[\frac{\log \left(\sqrt{re \cdot re + im \cdot im}\right) \cdot \log base + \tan^{-1}_* \frac{im}{re} \cdot 0}{\log base \cdot \log base + 0 \cdot 0}\]
- Using strategy
rm Applied add-sqr-sqrt29.2
\[\leadsto \frac{\log \left(\sqrt{re \cdot re + im \cdot im}\right) \cdot \log base + \tan^{-1}_* \frac{im}{re} \cdot 0}{\color{blue}{\sqrt{\log base \cdot \log base + 0 \cdot 0} \cdot \sqrt{\log base \cdot \log base + 0 \cdot 0}}}\]
Applied *-un-lft-identity29.2
\[\leadsto \frac{\color{blue}{1 \cdot \left(\log \left(\sqrt{re \cdot re + im \cdot im}\right) \cdot \log base + \tan^{-1}_* \frac{im}{re} \cdot 0\right)}}{\sqrt{\log base \cdot \log base + 0 \cdot 0} \cdot \sqrt{\log base \cdot \log base + 0 \cdot 0}}\]
Applied times-frac29.2
\[\leadsto \color{blue}{\frac{1}{\sqrt{\log base \cdot \log base + 0 \cdot 0}} \cdot \frac{\log \left(\sqrt{re \cdot re + im \cdot im}\right) \cdot \log base + \tan^{-1}_* \frac{im}{re} \cdot 0}{\sqrt{\log base \cdot \log base + 0 \cdot 0}}}\]
Applied simplify29.2
\[\leadsto \color{blue}{\frac{1}{\sqrt{\log base \cdot \log base}}} \cdot \frac{\log \left(\sqrt{re \cdot re + im \cdot im}\right) \cdot \log base + \tan^{-1}_* \frac{im}{re} \cdot 0}{\sqrt{\log base \cdot \log base + 0 \cdot 0}}\]
Applied simplify29.2
\[\leadsto \frac{1}{\sqrt{\log base \cdot \log base}} \cdot \color{blue}{\frac{\log base \cdot \log \left(\sqrt{im \cdot im + re \cdot re}\right)}{\sqrt{\log base \cdot \log base}}}\]
Taylor expanded around -inf 30.9
\[\leadsto \frac{1}{\sqrt{\log base \cdot \log base}} \cdot \frac{\log base \cdot \log \color{blue}{\left(-1 \cdot im\right)}}{\sqrt{\log base \cdot \log base}}\]
Applied simplify30.9
\[\leadsto \color{blue}{\frac{\log base \cdot \log \left(-im\right)}{\log base \cdot \log base}}\]