# Metamath Proof Explorer

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 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \mathrm{cos}\left({A}+{B}\right)=\mathrm{cos}{A}\mathrm{cos}{B}-\mathrm{sin}{A}\mathrm{sin}{B}$

### Proof

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