Derivation

Split input into 3 regimes
if t < -1.274691845662227e-134
1. Initial program 23.5
  \[\frac{2}{\left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right) \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)}\]
2. Simplified13.0
  \[\leadsto \color{blue}{\frac{\frac{\frac{2}{\tan k}}{\frac{t}{\frac{\ell}{t} \cdot \frac{\ell}{t}} \cdot \sin k}}{\frac{k}{t} \cdot \frac{k}{t} + 2}}\]
3. Using strategy rm
4. Applied *-un-lft-identity13.0
  \[\leadsto \frac{\frac{\frac{2}{\tan k}}{\frac{t}{\frac{\ell}{t} \cdot \frac{\ell}{t}} \cdot \sin k}}{\color{blue}{1 \cdot \left(\frac{k}{t} \cdot \frac{k}{t} + 2\right)}}\]
5. Applied div-inv13.0
  \[\leadsto \frac{\color{blue}{\frac{2}{\tan k} \cdot \frac{1}{\frac{t}{\frac{\ell}{t} \cdot \frac{\ell}{t}} \cdot \sin k}}}{1 \cdot \left(\frac{k}{t} \cdot \frac{k}{t} + 2\right)}\]
6. Applied times-frac13.0
  \[\leadsto \color{blue}{\frac{\frac{2}{\tan k}}{1} \cdot \frac{\frac{1}{\frac{t}{\frac{\ell}{t} \cdot \frac{\ell}{t}} \cdot \sin k}}{\frac{k}{t} \cdot \frac{k}{t} + 2}}\]
7. Simplified13.0
  \[\leadsto \color{blue}{\frac{2}{\tan k}} \cdot \frac{\frac{1}{\frac{t}{\frac{\ell}{t} \cdot \frac{\ell}{t}} \cdot \sin k}}{\frac{k}{t} \cdot \frac{k}{t} + 2}\]
8. Simplified8.3
  \[\leadsto \frac{2}{\tan k} \cdot \color{blue}{\frac{\frac{\frac{\frac{\ell}{t}}{t}}{2 + \frac{k}{t} \cdot \frac{k}{t}}}{\frac{\sin k}{\frac{\ell}{t}}}}\]
9. Using strategy rm
10. Applied *-un-lft-identity8.3
  \[\leadsto \frac{2}{\tan k} \cdot \frac{\frac{\frac{\frac{\ell}{t}}{t}}{2 + \frac{k}{t} \cdot \frac{k}{t}}}{\color{blue}{1 \cdot \frac{\sin k}{\frac{\ell}{t}}}}\]
11. Applied add-sqr-sqrt8.4
  \[\leadsto \frac{2}{\tan k} \cdot \frac{\frac{\frac{\frac{\ell}{t}}{t}}{\color{blue}{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}} \cdot \sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}}}}{1 \cdot \frac{\sin k}{\frac{\ell}{t}}}\]
12. Applied div-inv8.4
  \[\leadsto \frac{2}{\tan k} \cdot \frac{\frac{\color{blue}{\frac{\ell}{t} \cdot \frac{1}{t}}}{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}} \cdot \sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}}}{1 \cdot \frac{\sin k}{\frac{\ell}{t}}}\]
13. Applied times-frac8.3
  \[\leadsto \frac{2}{\tan k} \cdot \frac{\color{blue}{\frac{\frac{\ell}{t}}{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}} \cdot \frac{\frac{1}{t}}{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}}}}{1 \cdot \frac{\sin k}{\frac{\ell}{t}}}\]
14. Applied times-frac7.4
  \[\leadsto \frac{2}{\tan k} \cdot \color{blue}{\left(\frac{\frac{\frac{\ell}{t}}{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}}}{1} \cdot \frac{\frac{\frac{1}{t}}{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}}}{\frac{\sin k}{\frac{\ell}{t}}}\right)}\]
15. Applied associate-*r*4.8
  \[\leadsto \color{blue}{\left(\frac{2}{\tan k} \cdot \frac{\frac{\frac{\ell}{t}}{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}}}{1}\right) \cdot \frac{\frac{\frac{1}{t}}{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}}}{\frac{\sin k}{\frac{\ell}{t}}}}\]
16. Using strategy rm
17. Applied add-sqr-sqrt4.8
  \[\leadsto \left(\frac{2}{\tan k} \cdot \frac{\frac{\frac{\ell}{t}}{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}}}{1}\right) \cdot \frac{\frac{\frac{1}{t}}{\sqrt{\color{blue}{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}} \cdot \sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}}}}}{\frac{\sin k}{\frac{\ell}{t}}}\]
18. Applied sqrt-prod4.8
  \[\leadsto \left(\frac{2}{\tan k} \cdot \frac{\frac{\frac{\ell}{t}}{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}}}{1}\right) \cdot \frac{\frac{\frac{1}{t}}{\color{blue}{\sqrt{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}} \cdot \sqrt{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}}}}}{\frac{\sin k}{\frac{\ell}{t}}}\]
19. Applied div-inv4.8
  \[\leadsto \left(\frac{2}{\tan k} \cdot \frac{\frac{\frac{\ell}{t}}{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}}}{1}\right) \cdot \frac{\frac{\color{blue}{1 \cdot \frac{1}{t}}}{\sqrt{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}} \cdot \sqrt{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}}}}{\frac{\sin k}{\frac{\ell}{t}}}\]
20. Applied times-frac4.8
  \[\leadsto \left(\frac{2}{\tan k} \cdot \frac{\frac{\frac{\ell}{t}}{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}}}{1}\right) \cdot \frac{\color{blue}{\frac{1}{\sqrt{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}}} \cdot \frac{\frac{1}{t}}{\sqrt{\sqrt{2 + \frac{k}{t} \cdot \frac{k}{t}}}}}}{\frac{\sin k}{\frac{\ell}{t}}}\]
if -1.274691845662227e-134 < t < 1.9344565600985913e-62
1. Initial program 59.1
  \[\frac{2}{\left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right) \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)}\]
2. Simplified44.9
  \[\leadsto \color{blue}{\frac{\frac{\frac{2}{\tan k}}{\frac{t}{\frac{\ell}{t} \cdot \frac{\ell}{t}} \cdot \sin k}}{\frac{k}{t} \cdot \frac{k}{t} + 2}}\]
3. Using strategy rm
4. Applied *-un-lft-identity44.9
  \[\leadsto \frac{\frac{\frac{2}{\tan k}}{\frac{t}{\frac{\ell}{t} \cdot \frac{\ell}{t}} \cdot \sin k}}{\color{blue}{1 \cdot \left(\frac{k}{t} \cdot \frac{k}{t} + 2\right)}}\]
5. Applied div-inv44.9
  \[\leadsto \frac{\color{blue}{\frac{2}{\tan k} \cdot \frac{1}{\frac{t}{\frac{\ell}{t} \cdot \frac{\ell}{t}} \cdot \sin k}}}{1 \cdot \left(\frac{k}{t} \cdot \frac{k}{t} + 2\right)}\]
6. Applied times-frac43.9
  \[\leadsto \color{blue}{\frac{\frac{2}{\tan k}}{1} \cdot \frac{\frac{1}{\frac{t}{\frac{\ell}{t} \cdot \frac{\ell}{t}} \cdot \sin k}}{\frac{k}{t} \cdot \frac{k}{t} + 2}}\]
7. Simplified43.9
  \[\leadsto \color{blue}{\frac{2}{\tan k}} \cdot \frac{\frac{1}{\frac{t}{\frac{\ell}{t} \cdot \frac{\ell}{t}} \cdot \sin k}}{\frac{k}{t} \cdot \frac{k}{t} + 2}\]
8. Simplified40.0
  \[\leadsto \frac{2}{\tan k} \cdot \color{blue}{\frac{\frac{\frac{\frac{\ell}{t}}{t}}{2 + \frac{k}{t} \cdot \frac{k}{t}}}{\frac{\sin k}{\frac{\ell}{t}}}}\]
9. Using strategy rm
10. Applied associate-/r/40.0
  \[\leadsto \frac{2}{\tan k} \cdot \frac{\frac{\frac{\frac{\ell}{t}}{t}}{2 + \frac{k}{t} \cdot \frac{k}{t}}}{\color{blue}{\frac{\sin k}{\ell} \cdot t}}\]
11. Applied *-un-lft-identity40.0
  \[\leadsto \frac{2}{\tan k} \cdot \frac{\frac{\frac{\frac{\ell}{t}}{t}}{\color{blue}{1 \cdot \left(2 + \frac{k}{t} \cdot \frac{k}{t}\right)}}}{\frac{\sin k}{\ell} \cdot t}\]
12. Applied div-inv40.0
  \[\leadsto \frac{2}{\tan k} \cdot \frac{\frac{\color{blue}{\frac{\ell}{t} \cdot \frac{1}{t}}}{1 \cdot \left(2 + \frac{k}{t} \cdot \frac{k}{t}\right)}}{\frac{\sin k}{\ell} \cdot t}\]
13. Applied times-frac34.3
  \[\leadsto \frac{2}{\tan k} \cdot \frac{\color{blue}{\frac{\frac{\ell}{t}}{1} \cdot \frac{\frac{1}{t}}{2 + \frac{k}{t} \cdot \frac{k}{t}}}}{\frac{\sin k}{\ell} \cdot t}\]
14. Applied times-frac35.4
  \[\leadsto \frac{2}{\tan k} \cdot \color{blue}{\left(\frac{\frac{\frac{\ell}{t}}{1}}{\frac{\sin k}{\ell}} \cdot \frac{\frac{\frac{1}{t}}{2 + \frac{k}{t} \cdot \frac{k}{t}}}{t}\right)}\]
15. Applied associate-*r*35.4
  \[\leadsto \color{blue}{\left(\frac{2}{\tan k} \cdot \frac{\frac{\frac{\ell}{t}}{1}}{\frac{\sin k}{\ell}}\right) \cdot \frac{\frac{\frac{1}{t}}{2 + \frac{k}{t} \cdot \frac{k}{t}}}{t}}\]
16. Simplified20.2
  \[\leadsto \left(\frac{2}{\tan k} \cdot \frac{\frac{\frac{\ell}{t}}{1}}{\frac{\sin k}{\ell}}\right) \cdot \color{blue}{\frac{1}{k \cdot k + 2 \cdot \left(t \cdot t\right)}}\]
if 1.9344565600985913e-62 < t
1. Initial program 22.5
  \[\frac{2}{\left(\left(\frac{{t}^{3}}{\ell \cdot \ell} \cdot \sin k\right) \cdot \tan k\right) \cdot \left(\left(1 + {\left(\frac{k}{t}\right)}^{2}\right) + 1\right)}\]
2. Simplified12.1
  \[\leadsto \color{blue}{\frac{\frac{\frac{2}{\tan k}}{\frac{t}{\frac{\ell}{t} \cdot \frac{\ell}{t}} \cdot \sin k}}{\frac{k}{t} \cdot \frac{k}{t} + 2}}\]
3. Using strategy rm
4. Applied *-un-lft-identity12.1
  \[\leadsto \frac{\frac{\frac{2}{\tan k}}{\frac{t}{\frac{\ell}{t} \cdot \frac{\ell}{t}} \cdot \sin k}}{\color{blue}{1 \cdot \left(\frac{k}{t} \cdot \frac{k}{t} + 2\right)}}\]
5. Applied div-inv12.1
  \[\leadsto \frac{\color{blue}{\frac{2}{\tan k} \cdot \frac{1}{\frac{t}{\frac{\ell}{t} \cdot \frac{\ell}{t}} \cdot \sin k}}}{1 \cdot \left(\frac{k}{t} \cdot \frac{k}{t} + 2\right)}\]
6. Applied times-frac12.1
  \[\leadsto \color{blue}{\frac{\frac{2}{\tan k}}{1} \cdot \frac{\frac{1}{\frac{t}{\frac{\ell}{t} \cdot \frac{\ell}{t}} \cdot \sin k}}{\frac{k}{t} \cdot \frac{k}{t} + 2}}\]
7. Simplified12.1
  \[\leadsto \color{blue}{\frac{2}{\tan k}} \cdot \frac{\frac{1}{\frac{t}{\frac{\ell}{t} \cdot \frac{\ell}{t}} \cdot \sin k}}{\frac{k}{t} \cdot \frac{k}{t} + 2}\]
8. Simplified7.4
  \[\leadsto \frac{2}{\tan k} \cdot \color{blue}{\frac{\frac{\frac{\frac{\ell}{t}}{t}}{2 + \frac{k}{t} \cdot \frac{k}{t}}}{\frac{\sin k}{\frac{\ell}{t}}}}\]
9. Using strategy rm
10. Applied *-un-lft-identity7.4
  \[\leadsto \frac{2}{\tan k} \cdot \frac{\frac{\frac{\frac{\ell}{t}}{t}}{2 + \frac{k}{t} \cdot \frac{k}{t}}}{\color{blue}{1 \cdot \frac{\sin k}{\frac{\ell}{t}}}}\]
11. Applied *-un-lft-identity7.4
  \[\leadsto \frac{2}{\tan k} \cdot \frac{\frac{\frac{\frac{\ell}{t}}{t}}{\color{blue}{1 \cdot \left(2 + \frac{k}{t} \cdot \frac{k}{t}\right)}}}{1 \cdot \frac{\sin k}{\frac{\ell}{t}}}\]
12. Applied div-inv7.4
  \[\leadsto \frac{2}{\tan k} \cdot \frac{\frac{\color{blue}{\frac{\ell}{t} \cdot \frac{1}{t}}}{1 \cdot \left(2 + \frac{k}{t} \cdot \frac{k}{t}\right)}}{1 \cdot \frac{\sin k}{\frac{\ell}{t}}}\]
13. Applied times-frac7.7
  \[\leadsto \frac{2}{\tan k} \cdot \frac{\color{blue}{\frac{\frac{\ell}{t}}{1} \cdot \frac{\frac{1}{t}}{2 + \frac{k}{t} \cdot \frac{k}{t}}}}{1 \cdot \frac{\sin k}{\frac{\ell}{t}}}\]
14. Applied times-frac6.4
  \[\leadsto \frac{2}{\tan k} \cdot \color{blue}{\left(\frac{\frac{\frac{\ell}{t}}{1}}{1} \cdot \frac{\frac{\frac{1}{t}}{2 + \frac{k}{t} \cdot \frac{k}{t}}}{\frac{\sin k}{\frac{\ell}{t}}}\right)}\]
15. Applied associate-*r*3.7
  \[\leadsto \color{blue}{\left(\frac{2}{\tan k} \cdot \frac{\frac{\frac{\ell}{t}}{1}}{1}\right) \cdot \frac{\frac{\frac{1}{t}}{2 + \frac{k}{t} \cdot \frac{k}{t}}}{\frac{\sin k}{\frac{\ell}{t}}}}\]
16. Simplified3.4
  \[\leadsto \left(\frac{2}{\tan k} \cdot \frac{\frac{\frac{\ell}{t}}{1}}{1}\right) \cdot \color{blue}{\frac{\frac{\frac{\ell}{t}}{2 + \frac{k}{t} \cdot \frac{k}{t}}}{t \cdot \sin k}}\]
Recombined 3 regimes into one program.
Final simplification7.9
\[\leadsto \begin{array}{l} \mathbf{if}\;t \le -1.274691845662227 \cdot 10^{-134}:\\ \;\;\;\;\frac{\frac{\frac{1}{t}}{\sqrt{\sqrt{\frac{k}{t} \cdot \frac{k}{t} + 2}}} \cdot \frac{1}{\sqrt{\sqrt{\frac{k}{t} \cdot \frac{k}{t} + 2}}}}{\frac{\sin k}{\frac{\ell}{t}}} \cdot \left(\frac{\frac{\ell}{t}}{\sqrt{\frac{k}{t} \cdot \frac{k}{t} + 2}} \cdot \frac{2}{\tan k}\right)\\ \mathbf{elif}\;t \le 1.9344565600985913 \cdot 10^{-62}:\\ \;\;\;\;\left(\frac{2}{\tan k} \cdot \frac{\frac{\ell}{t}}{\frac{\sin k}{\ell}}\right) \cdot \frac{1}{2 \cdot \left(t \cdot t\right) + k \cdot k}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\frac{\ell}{t}}{\frac{k}{t} \cdot \frac{k}{t} + 2}}{t \cdot \sin k} \cdot \left(\frac{\ell}{t} \cdot \frac{2}{\tan k}\right)\\ \end{array}\]

Error

Derivation

`if t < -1.274691845662227e-134`

`if -1.274691845662227e-134 < t < 1.9344565600985913e-62`

`if 1.9344565600985913e-62 < t`

Reproduce