Metamath Proof Explorer

Theorem cosadd

Description: Addition formula for cosine. Equation 15 of Gleason p. 310. (Contributed by NM, 15-Jan-2006) (Revised by Mario Carneiro, 30-Apr-2014)

Ref Expression
Assertion cosadd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cos ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 addcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
2 cosval ⊢ ( ( 𝐴 + 𝐵 ) ∈ ℂ → ( cos ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( exp ‘ ( i · ( 𝐴 + 𝐵 ) ) ) + ( exp ‘ ( - i · ( 𝐴 + 𝐵 ) ) ) ) / 2 ) )
3 1 2 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cos ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( exp ‘ ( i · ( 𝐴 + 𝐵 ) ) ) + ( exp ‘ ( - i · ( 𝐴 + 𝐵 ) ) ) ) / 2 ) )
4 coscl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
5 4 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cos ‘ 𝐴 ) ∈ ℂ )
6 coscl ⊢ ( 𝐵 ∈ ℂ → ( cos ‘ 𝐵 ) ∈ ℂ )
7 6 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cos ‘ 𝐵 ) ∈ ℂ )
8 5 7 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ )
9 ax-icn ⊢ i ∈ ℂ
10 sincl ⊢ ( 𝐵 ∈ ℂ → ( sin ‘ 𝐵 ) ∈ ℂ )
11 10 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ 𝐵 ) ∈ ℂ )
12 mulcl ⊢ ( ( i ∈ ℂ ∧ ( sin ‘ 𝐵 ) ∈ ℂ ) → ( i · ( sin ‘ 𝐵 ) ) ∈ ℂ )
13 9 11 12 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( sin ‘ 𝐵 ) ) ∈ ℂ )
14 sincl ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
15 14 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ 𝐴 ) ∈ ℂ )
16 mulcl ⊢ ( ( i ∈ ℂ ∧ ( sin ‘ 𝐴 ) ∈ ℂ ) → ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ )
17 9 15 16 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ )
18 13 17 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ∈ ℂ )
19 8 18 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ∈ ℂ )
20 5 13 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) ∈ ℂ )
21 7 17 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ∈ ℂ )
22 20 21 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ∈ ℂ )
23 19 22 19 ppncand ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) + ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) + ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) − ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) + ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
24 adddi ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( 𝐴 + 𝐵 ) ) = ( ( i · 𝐴 ) + ( i · 𝐵 ) ) )
25 9 24 mp3an1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( 𝐴 + 𝐵 ) ) = ( ( i · 𝐴 ) + ( i · 𝐵 ) ) )
26 25 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( i · ( 𝐴 + 𝐵 ) ) ) = ( exp ‘ ( ( i · 𝐴 ) + ( i · 𝐵 ) ) ) )
27 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
28 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
29 9 27 28 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
30 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
31 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · 𝐵 ) ∈ ℂ )
32 9 30 31 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · 𝐵 ) ∈ ℂ )
33 efadd ⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ ( i · 𝐵 ) ∈ ℂ ) → ( exp ‘ ( ( i · 𝐴 ) + ( i · 𝐵 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐵 ) ) ) )
34 29 32 33 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( ( i · 𝐴 ) + ( i · 𝐵 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐵 ) ) ) )
35 efival ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) )
36 efival ⊢ ( 𝐵 ∈ ℂ → ( exp ‘ ( i · 𝐵 ) ) = ( ( cos ‘ 𝐵 ) + ( i · ( sin ‘ 𝐵 ) ) ) )
37 35 36 oveqan12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐵 ) ) ) = ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) · ( ( cos ‘ 𝐵 ) + ( i · ( sin ‘ 𝐵 ) ) ) ) )
38 5 17 7 13 muladdd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) · ( ( cos ‘ 𝐵 ) + ( i · ( sin ‘ 𝐵 ) ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) + ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
39 37 38 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐵 ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) + ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
40 26 34 39 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( i · ( 𝐴 + 𝐵 ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) + ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
41 negicn ⊢ - i ∈ ℂ
42 adddi ⊢ ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - i · ( 𝐴 + 𝐵 ) ) = ( ( - i · 𝐴 ) + ( - i · 𝐵 ) ) )
43 41 42 mp3an1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - i · ( 𝐴 + 𝐵 ) ) = ( ( - i · 𝐴 ) + ( - i · 𝐵 ) ) )
44 43 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( - i · ( 𝐴 + 𝐵 ) ) ) = ( exp ‘ ( ( - i · 𝐴 ) + ( - i · 𝐵 ) ) ) )
45 mulcl ⊢ ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) ∈ ℂ )
46 41 27 45 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - i · 𝐴 ) ∈ ℂ )
47 mulcl ⊢ ( ( - i ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - i · 𝐵 ) ∈ ℂ )
48 41 30 47 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - i · 𝐵 ) ∈ ℂ )
49 efadd ⊢ ( ( ( - i · 𝐴 ) ∈ ℂ ∧ ( - i · 𝐵 ) ∈ ℂ ) → ( exp ‘ ( ( - i · 𝐴 ) + ( - i · 𝐵 ) ) ) = ( ( exp ‘ ( - i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐵 ) ) ) )
50 46 48 49 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( ( - i · 𝐴 ) + ( - i · 𝐵 ) ) ) = ( ( exp ‘ ( - i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐵 ) ) ) )
51 efmival ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) )
52 efmival ⊢ ( 𝐵 ∈ ℂ → ( exp ‘ ( - i · 𝐵 ) ) = ( ( cos ‘ 𝐵 ) − ( i · ( sin ‘ 𝐵 ) ) ) )
53 51 52 oveqan12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( exp ‘ ( - i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐵 ) ) ) = ( ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) · ( ( cos ‘ 𝐵 ) − ( i · ( sin ‘ 𝐵 ) ) ) ) )
54 5 17 7 13 mulsubd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) · ( ( cos ‘ 𝐵 ) − ( i · ( sin ‘ 𝐵 ) ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) − ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
55 53 54 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( exp ‘ ( - i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐵 ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) − ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
56 44 50 55 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( - i · ( 𝐴 + 𝐵 ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) − ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
57 40 56 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( exp ‘ ( i · ( 𝐴 + 𝐵 ) ) ) + ( exp ‘ ( - i · ( 𝐴 + 𝐵 ) ) ) ) = ( ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) + ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) + ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) − ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) ) )
58 19 2timesd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) + ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
59 23 57 58 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( exp ‘ ( i · ( 𝐴 + 𝐵 ) ) ) + ( exp ‘ ( - i · ( 𝐴 + 𝐵 ) ) ) ) = ( 2 · ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
60 59 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( exp ‘ ( i · ( 𝐴 + 𝐵 ) ) ) + ( exp ‘ ( - i · ( 𝐴 + 𝐵 ) ) ) ) / 2 ) = ( ( 2 · ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) / 2 ) )
61 2cn ⊢ 2 ∈ ℂ
62 2ne0 ⊢ 2 ≠ 0
63 divcan3 ⊢ ( ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) / 2 ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) )
64 61 62 63 mp3an23 ⊢ ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ∈ ℂ → ( ( 2 · ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) / 2 ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) )
65 19 64 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 2 · ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) / 2 ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) )
66 9 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → i ∈ ℂ )
67 66 11 66 15 mul4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) = ( ( i · i ) · ( ( sin ‘ 𝐵 ) · ( sin ‘ 𝐴 ) ) ) )
68 ixi ⊢ ( i · i ) = - 1
69 68 oveq1i ⊢ ( ( i · i ) · ( ( sin ‘ 𝐵 ) · ( sin ‘ 𝐴 ) ) ) = ( - 1 · ( ( sin ‘ 𝐵 ) · ( sin ‘ 𝐴 ) ) )
70 11 15 mulcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ 𝐵 ) · ( sin ‘ 𝐴 ) ) = ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) )
71 70 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 1 · ( ( sin ‘ 𝐵 ) · ( sin ‘ 𝐴 ) ) ) = ( - 1 · ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
72 69 71 syl5eq ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · i ) · ( ( sin ‘ 𝐵 ) · ( sin ‘ 𝐴 ) ) ) = ( - 1 · ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
73 15 11 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ∈ ℂ )
74 73 mulm1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 1 · ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) = - ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) )
75 67 72 74 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) = - ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) )
76 75 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + - ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
77 8 73 negsubd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + - ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
78 65 76 77 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 2 · ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) / 2 ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
79 3 60 78 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cos ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )