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 syl5eq 
 |-  ( ( 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 ) ) ) )