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 ⊢A∈ℂ∧B∈ℂ→cos⁡A+B=cos⁡A⁢cos⁡B−sin⁡A⁢sin⁡B

Proof

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