Initial program 16.7
\[\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-sqrt16.7
\[\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-identity16.7
\[\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-frac16.7
\[\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 simplify16.7
\[\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 simplify16.7
\[\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.8
\[\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.8
\[\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.8
\[\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.8
\[\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.8
\[\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.8
\[\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 37.7
\[\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 simplify37.6
\[\leadsto \color{blue}{\frac{\frac{\log base}{\left|\log base\right|}}{\frac{\left|\log base\right|}{\log \left(-im\right)}}}\]