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 e. CC /\ B e. CC ) -> ( cos ` ( A + B ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) )

Proof

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