Metamath Proof Explorer

Theorem sinadd

Description: Addition formula for sine. Equation 14 of Gleason p. 310. (Contributed by Steve Rodriguez, 10-Nov-2006) (Revised by Mario Carneiro, 30-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 addcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
2 sinval ⊢ ( ( 𝐴 + 𝐵 ) ∈ ℂ → ( sin ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( exp ‘ ( i · ( 𝐴 + 𝐵 ) ) ) − ( exp ‘ ( - i · ( 𝐴 + 𝐵 ) ) ) ) / ( 2 · i ) ) )
3 1 2 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( exp ‘ ( i · ( 𝐴 + 𝐵 ) ) ) − ( exp ‘ ( - i · ( 𝐴 + 𝐵 ) ) ) ) / ( 2 · i ) ) )
4 2cn ⊢ 2 ∈ ℂ
5 4 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 2 ∈ ℂ )
6 ax-icn ⊢ i ∈ ℂ
7 6 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → i ∈ ℂ )
8 coscl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
9 8 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cos ‘ 𝐴 ) ∈ ℂ )
10 sincl ⊢ ( 𝐵 ∈ ℂ → ( sin ‘ 𝐵 ) ∈ ℂ )
11 10 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ 𝐵 ) ∈ ℂ )
12 9 11 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ∈ ℂ )
13 sincl ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
14 13 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ 𝐴 ) ∈ ℂ )
15 coscl ⊢ ( 𝐵 ∈ ℂ → ( cos ‘ 𝐵 ) ∈ ℂ )
16 15 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cos ‘ 𝐵 ) ∈ ℂ )
17 14 16 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ )
18 12 17 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) ∈ ℂ )
19 5 7 18 mulassd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 2 · i ) · ( ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) ) = ( 2 · ( i · ( ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) ) ) )
20 7 12 17 adddid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) ) = ( ( i · ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) + ( i · ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) ) )
21 7 9 11 mul12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) = ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) )
22 14 16 mulcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) = ( ( cos ‘ 𝐵 ) · ( sin ‘ 𝐴 ) ) )
23 22 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) = ( i · ( ( cos ‘ 𝐵 ) · ( sin ‘ 𝐴 ) ) ) )
24 7 16 14 mul12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( ( cos ‘ 𝐵 ) · ( sin ‘ 𝐴 ) ) ) = ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) )
25 23 24 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) = ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) )
26 21 25 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) + ( i · ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) ) = ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) )
27 20 26 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) ) = ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) )
28 27 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( i · ( ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) ) ) = ( 2 · ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
29 19 28 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 2 · i ) · ( ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) ) = ( 2 · ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
30 mulcl ⊢ ( ( i ∈ ℂ ∧ ( sin ‘ 𝐵 ) ∈ ℂ ) → ( i · ( sin ‘ 𝐵 ) ) ∈ ℂ )
31 6 11 30 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( sin ‘ 𝐵 ) ) ∈ ℂ )
32 9 31 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) ∈ ℂ )
33 mulcl ⊢ ( ( i ∈ ℂ ∧ ( sin ‘ 𝐴 ) ∈ ℂ ) → ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ )
34 6 14 33 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( sin ‘ 𝐴 ) ) ∈ ℂ )
35 16 34 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ∈ ℂ )
36 32 35 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ∈ ℂ )
37 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ∈ ℂ ) → ( 2 · ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) ∈ ℂ )
38 4 36 37 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) ∈ ℂ )
39 2mulicn ⊢ ( 2 · i ) ∈ ℂ
40 39 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · i ) ∈ ℂ )
41 2muline0 ⊢ ( 2 · i ) ≠ 0
42 41 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · i ) ≠ 0 )
43 38 40 18 42 divmuld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 2 · ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) / ( 2 · i ) ) = ( ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) ↔ ( ( 2 · i ) · ( ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) ) = ( 2 · ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) ) )
44 29 43 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 2 · ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) / ( 2 · i ) ) = ( ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) )
45 9 16 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ )
46 31 34 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ∈ ℂ )
47 45 46 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ∈ ℂ )
48 47 36 36 pnncand ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( ( 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 ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) + ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
49 adddi ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( 𝐴 + 𝐵 ) ) = ( ( i · 𝐴 ) + ( i · 𝐵 ) ) )
50 6 49 mp3an1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · ( 𝐴 + 𝐵 ) ) = ( ( i · 𝐴 ) + ( i · 𝐵 ) ) )
51 50 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( i · ( 𝐴 + 𝐵 ) ) ) = ( exp ‘ ( ( i · 𝐴 ) + ( i · 𝐵 ) ) ) )
52 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
53 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
54 6 52 53 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
55 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
56 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · 𝐵 ) ∈ ℂ )
57 6 55 56 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · 𝐵 ) ∈ ℂ )
58 efadd ⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ ( i · 𝐵 ) ∈ ℂ ) → ( exp ‘ ( ( i · 𝐴 ) + ( i · 𝐵 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐵 ) ) ) )
59 54 57 58 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( ( i · 𝐴 ) + ( i · 𝐵 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐵 ) ) ) )
60 efival ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) )
61 efival ⊢ ( 𝐵 ∈ ℂ → ( exp ‘ ( i · 𝐵 ) ) = ( ( cos ‘ 𝐵 ) + ( i · ( sin ‘ 𝐵 ) ) ) )
62 60 61 oveqan12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐵 ) ) ) = ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) · ( ( cos ‘ 𝐵 ) + ( i · ( sin ‘ 𝐵 ) ) ) ) )
63 9 34 16 31 muladdd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( cos ‘ 𝐴 ) + ( i · ( sin ‘ 𝐴 ) ) ) · ( ( cos ‘ 𝐵 ) + ( i · ( sin ‘ 𝐵 ) ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) + ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
64 62 63 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐵 ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) + ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
65 51 59 64 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( i · ( 𝐴 + 𝐵 ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) + ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
66 negicn ⊢ - i ∈ ℂ
67 adddi ⊢ ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - i · ( 𝐴 + 𝐵 ) ) = ( ( - i · 𝐴 ) + ( - i · 𝐵 ) ) )
68 66 67 mp3an1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - i · ( 𝐴 + 𝐵 ) ) = ( ( - i · 𝐴 ) + ( - i · 𝐵 ) ) )
69 68 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( - i · ( 𝐴 + 𝐵 ) ) ) = ( exp ‘ ( ( - i · 𝐴 ) + ( - i · 𝐵 ) ) ) )
70 mulcl ⊢ ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) ∈ ℂ )
71 66 52 70 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - i · 𝐴 ) ∈ ℂ )
72 mulcl ⊢ ( ( - i ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - i · 𝐵 ) ∈ ℂ )
73 66 55 72 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - i · 𝐵 ) ∈ ℂ )
74 efadd ⊢ ( ( ( - i · 𝐴 ) ∈ ℂ ∧ ( - i · 𝐵 ) ∈ ℂ ) → ( exp ‘ ( ( - i · 𝐴 ) + ( - i · 𝐵 ) ) ) = ( ( exp ‘ ( - i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐵 ) ) ) )
75 71 73 74 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( ( - i · 𝐴 ) + ( - i · 𝐵 ) ) ) = ( ( exp ‘ ( - i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐵 ) ) ) )
76 efmival ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) = ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) )
77 efmival ⊢ ( 𝐵 ∈ ℂ → ( exp ‘ ( - i · 𝐵 ) ) = ( ( cos ‘ 𝐵 ) − ( i · ( sin ‘ 𝐵 ) ) ) )
78 76 77 oveqan12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( exp ‘ ( - i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐵 ) ) ) = ( ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) · ( ( cos ‘ 𝐵 ) − ( i · ( sin ‘ 𝐵 ) ) ) ) )
79 9 34 16 31 mulsubd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( cos ‘ 𝐴 ) − ( i · ( sin ‘ 𝐴 ) ) ) · ( ( cos ‘ 𝐵 ) − ( i · ( sin ‘ 𝐵 ) ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) − ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
80 78 79 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( exp ‘ ( - i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐵 ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) − ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
81 69 75 80 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( - i · ( 𝐴 + 𝐵 ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( i · ( sin ‘ 𝐵 ) ) · ( i · ( sin ‘ 𝐴 ) ) ) ) − ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
82 65 81 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 ‘ 𝐴 ) ) ) ) ) ) )
83 36 2timesd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) + ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
84 48 82 83 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( exp ‘ ( i · ( 𝐴 + 𝐵 ) ) ) − ( exp ‘ ( - i · ( 𝐴 + 𝐵 ) ) ) ) = ( 2 · ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) )
85 84 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( exp ‘ ( i · ( 𝐴 + 𝐵 ) ) ) − ( exp ‘ ( - i · ( 𝐴 + 𝐵 ) ) ) ) / ( 2 · i ) ) = ( ( 2 · ( ( ( cos ‘ 𝐴 ) · ( i · ( sin ‘ 𝐵 ) ) ) + ( ( cos ‘ 𝐵 ) · ( i · ( sin ‘ 𝐴 ) ) ) ) ) / ( 2 · i ) ) )
86 17 12 addcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) = ( ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) )
87 44 85 86 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( exp ‘ ( i · ( 𝐴 + 𝐵 ) ) ) − ( exp ‘ ( - i · ( 𝐴 + 𝐵 ) ) ) ) / ( 2 · i ) ) = ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
88 3 87 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )