This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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