Metamath Proof Explorer

Theorem coshadd

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

Ref Expression
Assertion coshadd 
|- ( ( A e. CC /\ B e. CC ) -> ( cosh ` ( A + B ) ) = ( ( ( cosh ` A ) x. ( cosh ` B ) ) + ( ( sinh ` A ) x. ( sinh ` B ) ) ) )

Proof

Step Hyp Ref Expression
1 addcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
2 coshval-named 
 |-  ( ( A + B ) e. CC -> ( cosh ` ( A + B ) ) = ( cos ` ( _i x. ( A + B ) ) ) )
3 1 2 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cosh ` ( A + B ) ) = ( cos ` ( _i x. ( A + B ) ) ) )
4 ax-icn 
 |-  _i e. CC
5 adddi 
 |-  ( ( _i e. CC /\ A e. CC /\ B e. CC ) -> ( _i x. ( A + B ) ) = ( ( _i x. A ) + ( _i x. B ) ) )
6 4 5 mp3an1 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. ( A + B ) ) = ( ( _i x. A ) + ( _i x. B ) ) )
7 6 fveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cos ` ( _i x. ( A + B ) ) ) = ( cos ` ( ( _i x. A ) + ( _i x. B ) ) ) )
8 4 a1i 
 |-  ( ( A e. CC /\ B e. CC ) -> _i e. CC )
9 simpl 
 |-  ( ( A e. CC /\ B e. CC ) -> A e. CC )
10 8 9 mulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. A ) e. CC )
11 simpr 
 |-  ( ( A e. CC /\ B e. CC ) -> B e. CC )
12 8 11 mulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. B ) e. CC )
13 cosadd 
 |-  ( ( ( _i x. A ) e. CC /\ ( _i x. B ) e. CC ) -> ( cos ` ( ( _i x. A ) + ( _i x. B ) ) ) = ( ( ( cos ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) - ( ( sin ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) ) )
14 10 12 13 syl2anc 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cos ` ( ( _i x. A ) + ( _i x. B ) ) ) = ( ( ( cos ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) - ( ( sin ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) ) )
15 3 7 14 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cosh ` ( A + B ) ) = ( ( ( cos ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) - ( ( sin ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) ) )
16 coshval-named 
 |-  ( A e. CC -> ( cosh ` A ) = ( cos ` ( _i x. A ) ) )
17 coshval-named 
 |-  ( B e. CC -> ( cosh ` B ) = ( cos ` ( _i x. B ) ) )
18 16 17 oveqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cosh ` A ) x. ( cosh ` B ) ) = ( ( cos ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) )
19 18 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( cosh ` A ) x. ( cosh ` B ) ) - ( ( sin ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) ) = ( ( ( cos ` ( _i x. A ) ) x. ( cos ` ( _i x. B ) ) ) - ( ( sin ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) ) )
20 15 19 eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cosh ` ( A + B ) ) = ( ( ( cosh ` A ) x. ( cosh ` B ) ) - ( ( sin ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) ) )
21 ixi 
 |-  ( _i x. _i ) = -u 1
22 21 a1i 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. _i ) = -u 1 )
23 22 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( _i x. _i ) x. ( ( sinh ` A ) x. ( sinh ` B ) ) ) = ( -u 1 x. ( ( sinh ` A ) x. ( sinh ` B ) ) ) )
24 sinhval-named 
 |-  ( A e. CC -> ( sinh ` A ) = ( ( sin ` ( _i x. A ) ) / _i ) )
25 sinhval-named 
 |-  ( B e. CC -> ( sinh ` B ) = ( ( sin ` ( _i x. B ) ) / _i ) )
26 24 25 oveqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sinh ` A ) x. ( sinh ` B ) ) = ( ( ( sin ` ( _i x. A ) ) / _i ) x. ( ( sin ` ( _i x. B ) ) / _i ) ) )
27 26 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( _i x. _i ) x. ( ( sinh ` A ) x. ( sinh ` B ) ) ) = ( ( _i x. _i ) x. ( ( ( sin ` ( _i x. A ) ) / _i ) x. ( ( sin ` ( _i x. B ) ) / _i ) ) ) )
28 23 27 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( -u 1 x. ( ( sinh ` A ) x. ( sinh ` B ) ) ) = ( ( _i x. _i ) x. ( ( ( sin ` ( _i x. A ) ) / _i ) x. ( ( sin ` ( _i x. B ) ) / _i ) ) ) )
29 10 sincld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sin ` ( _i x. A ) ) e. CC )
30 ine0 
 |-  _i =/= 0
31 30 a1i 
 |-  ( ( A e. CC /\ B e. CC ) -> _i =/= 0 )
32 29 8 31 divcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` ( _i x. A ) ) / _i ) e. CC )
33 12 sincld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sin ` ( _i x. B ) ) e. CC )
34 33 8 31 divcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` ( _i x. B ) ) / _i ) e. CC )
35 8 8 32 34 mul4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( _i x. _i ) x. ( ( ( sin ` ( _i x. A ) ) / _i ) x. ( ( sin ` ( _i x. B ) ) / _i ) ) ) = ( ( _i x. ( ( sin ` ( _i x. A ) ) / _i ) ) x. ( _i x. ( ( sin ` ( _i x. B ) ) / _i ) ) ) )
36 29 8 31 divcan2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. ( ( sin ` ( _i x. A ) ) / _i ) ) = ( sin ` ( _i x. A ) ) )
37 33 8 31 divcan2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( _i x. ( ( sin ` ( _i x. B ) ) / _i ) ) = ( sin ` ( _i x. B ) ) )
38 36 37 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( _i x. ( ( sin ` ( _i x. A ) ) / _i ) ) x. ( _i x. ( ( sin ` ( _i x. B ) ) / _i ) ) ) = ( ( sin ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) )
39 28 35 38 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( -u 1 x. ( ( sinh ` A ) x. ( sinh ` B ) ) ) = ( ( sin ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) )
40 sinhcl 
 |-  ( A e. CC -> ( sinh ` A ) e. CC )
41 sinhcl 
 |-  ( B e. CC -> ( sinh ` B ) e. CC )
42 mulcl 
 |-  ( ( ( sinh ` A ) e. CC /\ ( sinh ` B ) e. CC ) -> ( ( sinh ` A ) x. ( sinh ` B ) ) e. CC )
43 40 41 42 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sinh ` A ) x. ( sinh ` B ) ) e. CC )
44 43 mulm1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( -u 1 x. ( ( sinh ` A ) x. ( sinh ` B ) ) ) = -u ( ( sinh ` A ) x. ( sinh ` B ) ) )
45 39 44 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) = -u ( ( sinh ` A ) x. ( sinh ` B ) ) )
46 45 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( cosh ` A ) x. ( cosh ` B ) ) - ( ( sin ` ( _i x. A ) ) x. ( sin ` ( _i x. B ) ) ) ) = ( ( ( cosh ` A ) x. ( cosh ` B ) ) - -u ( ( sinh ` A ) x. ( sinh ` B ) ) ) )
47 coshcl 
 |-  ( A e. CC -> ( cosh ` A ) e. CC )
48 9 47 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cosh ` A ) e. CC )
49 coshcl 
 |-  ( B e. CC -> ( cosh ` B ) e. CC )
50 11 49 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cosh ` B ) e. CC )
51 48 50 mulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cosh ` A ) x. ( cosh ` B ) ) e. CC )
52 51 43 subnegd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( cosh ` A ) x. ( cosh ` B ) ) - -u ( ( sinh ` A ) x. ( sinh ` B ) ) ) = ( ( ( cosh ` A ) x. ( cosh ` B ) ) + ( ( sinh ` A ) x. ( sinh ` B ) ) ) )
53 20 46 52 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cosh ` ( A + B ) ) = ( ( ( cosh ` A ) x. ( cosh ` B ) ) + ( ( sinh ` A ) x. ( sinh ` B ) ) ) )