Metamath Proof Explorer

Theorem tanhadd

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

Ref Expression
Assertion tanhadd 
|- ( ( ( ( A e. CC /\ B e. CC ) /\ ( cosh ` A ) =/= 0 ) /\ ( ( cosh ` B ) =/= 0 /\ ( cosh ` ( A + B ) ) =/= 0 ) ) -> ( tanh ` ( A + B ) ) = ( ( ( tanh ` A ) + ( tanh ` B ) ) / ( 1 + ( ( tanh ` A ) x. ( tanh ` B ) ) ) ) )

Proof

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