Metamath Proof Explorer

Theorem tanhadd

Description: Addition formula for tanh. (Contributed by Jon Pennant, 9-Sep-2026)

Ref Expression
Assertion tanhadd ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( tanh ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( tanh ‘ 𝐴 ) + ( tanh ‘ 𝐵 ) ) / ( 1 + ( ( tanh ‘ 𝐴 ) · ( tanh ‘ 𝐵 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simplll ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → 𝐴 ∈ ℂ )
2 simpllr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → 𝐵 ∈ ℂ )
3 1 2 addcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
4 simprr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 )
5 tanhval ⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℂ ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) → ( tanh ‘ ( 𝐴 + 𝐵 ) ) = ( ( sinh ‘ ( 𝐴 + 𝐵 ) ) / ( cosh ‘ ( 𝐴 + 𝐵 ) ) ) )
6 3 4 5 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( tanh ‘ ( 𝐴 + 𝐵 ) ) = ( ( sinh ‘ ( 𝐴 + 𝐵 ) ) / ( cosh ‘ ( 𝐴 + 𝐵 ) ) ) )
7 sinhadd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sinh ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) )
8 coshadd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cosh ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) )
9 7 8 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sinh ‘ ( 𝐴 + 𝐵 ) ) / ( cosh ‘ ( 𝐴 + 𝐵 ) ) ) = ( ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) / ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) ) )
10 9 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( sinh ‘ ( 𝐴 + 𝐵 ) ) / ( cosh ‘ ( 𝐴 + 𝐵 ) ) ) = ( ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) / ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) ) )
11 sinhcl ⊢ ( 𝐴 ∈ ℂ → ( sinh ‘ 𝐴 ) ∈ ℂ )
12 11 ad3antrrr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( sinh ‘ 𝐴 ) ∈ ℂ )
13 coshcl ⊢ ( 𝐵 ∈ ℂ → ( cosh ‘ 𝐵 ) ∈ ℂ )
14 13 ad3antlr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( cosh ‘ 𝐵 ) ∈ ℂ )
15 12 14 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ∈ ℂ )
16 coshcl ⊢ ( 𝐴 ∈ ℂ → ( cosh ‘ 𝐴 ) ∈ ℂ )
17 16 ad3antrrr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( cosh ‘ 𝐴 ) ∈ ℂ )
18 sinhcl ⊢ ( 𝐵 ∈ ℂ → ( sinh ‘ 𝐵 ) ∈ ℂ )
19 18 ad3antlr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( sinh ‘ 𝐵 ) ∈ ℂ )
20 17 19 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ∈ ℂ )
21 15 20 addcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) ∈ ℂ )
22 17 14 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ∈ ℂ )
23 12 19 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ∈ ℂ )
24 22 23 addcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) ∈ ℂ )
25 8 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( cosh ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) )
26 25 4 eqnetrrd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) ≠ 0 )
27 simplr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( cosh ‘ 𝐴 ) ≠ 0 )
28 simprl ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( cosh ‘ 𝐵 ) ≠ 0 )
29 17 14 27 28 mulne0d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ≠ 0 )
30 21 24 22 26 29 divcan7d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) / ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ) / ( ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) / ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ) ) = ( ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) / ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) ) )
31 12 17 19 14 27 28 divadddivd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) + ( ( sinh ‘ 𝐵 ) / ( cosh ‘ 𝐵 ) ) ) = ( ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( sinh ‘ 𝐵 ) · ( cosh ‘ 𝐴 ) ) ) / ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ) )
32 tanhval ⊢ ( ( 𝐴 ∈ ℂ ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) → ( tanh ‘ 𝐴 ) = ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) )
33 1 27 32 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( tanh ‘ 𝐴 ) = ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) )
34 tanhval ⊢ ( ( 𝐵 ∈ ℂ ∧ ( cosh ‘ 𝐵 ) ≠ 0 ) → ( tanh ‘ 𝐵 ) = ( ( sinh ‘ 𝐵 ) / ( cosh ‘ 𝐵 ) ) )
35 2 28 34 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( tanh ‘ 𝐵 ) = ( ( sinh ‘ 𝐵 ) / ( cosh ‘ 𝐵 ) ) )
36 33 35 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( tanh ‘ 𝐴 ) + ( tanh ‘ 𝐵 ) ) = ( ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) + ( ( sinh ‘ 𝐵 ) / ( cosh ‘ 𝐵 ) ) ) )
37 17 19 mulcomd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) = ( ( sinh ‘ 𝐵 ) · ( cosh ‘ 𝐴 ) ) )
38 37 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) = ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( sinh ‘ 𝐵 ) · ( cosh ‘ 𝐴 ) ) ) )
39 38 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) / ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ) = ( ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( sinh ‘ 𝐵 ) · ( cosh ‘ 𝐴 ) ) ) / ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ) )
40 31 36 39 3eqtr4rd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) / ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ) = ( ( tanh ‘ 𝐴 ) + ( tanh ‘ 𝐵 ) ) )
41 22 23 22 29 divdird ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) / ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ) = ( ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) / ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ) + ( ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) / ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ) ) )
42 22 29 dividd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) / ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ) = 1 )
43 33 35 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( tanh ‘ 𝐴 ) · ( tanh ‘ 𝐵 ) ) = ( ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) · ( ( sinh ‘ 𝐵 ) / ( cosh ‘ 𝐵 ) ) ) )
44 12 17 19 14 27 28 divmuldivd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( sinh ‘ 𝐴 ) / ( cosh ‘ 𝐴 ) ) · ( ( sinh ‘ 𝐵 ) / ( cosh ‘ 𝐵 ) ) ) = ( ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) / ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ) )
45 43 44 eqtr2d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) / ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ) = ( ( tanh ‘ 𝐴 ) · ( tanh ‘ 𝐵 ) ) )
46 42 45 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) / ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ) + ( ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) / ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ) ) = ( 1 + ( ( tanh ‘ 𝐴 ) · ( tanh ‘ 𝐵 ) ) ) )
47 41 46 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) / ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ) = ( 1 + ( ( tanh ‘ 𝐴 ) · ( tanh ‘ 𝐵 ) ) ) )
48 40 47 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) / ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ) / ( ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) / ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) ) ) = ( ( ( tanh ‘ 𝐴 ) + ( tanh ‘ 𝐵 ) ) / ( 1 + ( ( tanh ‘ 𝐴 ) · ( tanh ‘ 𝐵 ) ) ) ) )
49 30 48 eqtr3d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( ( ( ( sinh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( cosh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) / ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) ) = ( ( ( tanh ‘ 𝐴 ) + ( tanh ‘ 𝐵 ) ) / ( 1 + ( ( tanh ‘ 𝐴 ) · ( tanh ‘ 𝐵 ) ) ) ) )
50 6 10 49 3eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( tanh ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( tanh ‘ 𝐴 ) + ( tanh ‘ 𝐵 ) ) / ( 1 + ( ( tanh ‘ 𝐴 ) · ( tanh ‘ 𝐵 ) ) ) ) )