Metamath Proof Explorer

Theorem coshadd

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

Ref Expression
Assertion coshadd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cosh ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( cosh ‘ 𝐴 ) · ( cosh ‘ 𝐵 ) ) + ( ( sinh ‘ 𝐴 ) · ( sinh ‘ 𝐵 ) ) ) )

Proof

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