Metamath Proof Explorer

Theorem coshadd

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

Ref Expression
Assertion coshadd ⊢ A ∈ ℂ ∧ B ∈ ℂ → cosh ⁡ A + B = cosh ⁡ A ⁢ cosh ⁡ B + sinh ⁡ A ⁢ sinh ⁡ B

Proof

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