Initial program 12.3
\[\frac{\sin ky}{\sqrt{{\left(\sin kx\right)}^{2} + {\left(\sin ky\right)}^{2}}} \cdot \sin th\]
Simplified11.1
\[\leadsto \color{blue}{\frac{\sin th \cdot \sin ky}{\sqrt{\left(\sin kx\right)^2 + \left(\sin ky\right)^2}^*}}\]
- Using strategy
rm Applied *-un-lft-identity11.1
\[\leadsto \frac{\sin th \cdot \sin ky}{\color{blue}{1 \cdot \sqrt{\left(\sin kx\right)^2 + \left(\sin ky\right)^2}^*}}\]
Applied times-frac8.8
\[\leadsto \color{blue}{\frac{\sin th}{1} \cdot \frac{\sin ky}{\sqrt{\left(\sin kx\right)^2 + \left(\sin ky\right)^2}^*}}\]
Simplified8.8
\[\leadsto \color{blue}{\sin th} \cdot \frac{\sin ky}{\sqrt{\left(\sin kx\right)^2 + \left(\sin ky\right)^2}^*}\]
- Using strategy
rm Applied log1p-expm1-u8.8
\[\leadsto \sin th \cdot \color{blue}{\log_* (1 + (e^{\frac{\sin ky}{\sqrt{\left(\sin kx\right)^2 + \left(\sin ky\right)^2}^*}} - 1)^*)}\]
- Using strategy
rm Applied expm1-log1p-u8.8
\[\leadsto \color{blue}{(e^{\log_* (1 + \sin th \cdot \log_* (1 + (e^{\frac{\sin ky}{\sqrt{\left(\sin kx\right)^2 + \left(\sin ky\right)^2}^*}} - 1)^*))} - 1)^*}\]
Final simplification8.8
\[\leadsto (e^{\log_* (1 + \sin th \cdot \log_* (1 + (e^{\frac{\sin ky}{\sqrt{\left(\sin kx\right)^2 + \left(\sin ky\right)^2}^*}} - 1)^*))} - 1)^*\]