Step Hyp Ref
Expression 1 oveq2 6304 . . . . 5
2 oveq1 6303 . . . . . . 7
3 2 fveq2d 5875 . . . . . 6
4 2 fveq2d 5875 . . . . . . 7
5 4 oveq2d 6312 . . . . . 6
6 3 , 5 oveq12d 6314 . . . . 5
7 1 , 6 eqeq12d 2479 . . . 4
8 7 imbi2d 316 . . 3
9 oveq2 6304 . . . . 5
10 oveq1 6303 . . . . . . 7
11 10 fveq2d 5875 . . . . . 6
12 10 fveq2d 5875 . . . . . . 7
13 12 oveq2d 6312 . . . . . 6
14 11 , 13 oveq12d 6314 . . . . 5
15 9 , 14 eqeq12d 2479 . . . 4
16 15 imbi2d 316 . . 3
17 oveq2 6304 . . . . 5
18 oveq1 6303 . . . . . . 7
19 18 fveq2d 5875 . . . . . 6
20 18 fveq2d 5875 . . . . . . 7
21 20 oveq2d 6312 . . . . . 6
22 19 , 21 oveq12d 6314 . . . . 5
23 17 , 22 eqeq12d 2479 . . . 4
24 23 imbi2d 316 . . 3
25 oveq2 6304 . . . . 5
26 oveq1 6303 . . . . . . 7
27 26 fveq2d 5875 . . . . . 6
28 26 fveq2d 5875 . . . . . . 7
29 28 oveq2d 6312 . . . . . 6
30 27 , 29 oveq12d 6314 . . . . 5
31 25 , 30 eqeq12d 2479 . . . 4
32 31 imbi2d 316 . . 3
33 coscl 13862 . . . . . 6
34 ax-icn 9572 . . . . . . 7
35 sincl 13861 . . . . . . 7
36 mulcl 9597 . . . . . . 7
37 34 , 35 , 36 sylancr 663 . . . . . 6
38 addcl 9595 . . . . . 6
39 33 , 37 , 38 syl2anc 661 . . . . 5
40 exp0 12170 . . . . 5
41 39 , 40 syl 16 . . . 4
42 mul02 9779 . . . . . . . 8
43 42 fveq2d 5875 . . . . . . 7
44 cos0 13885 . . . . . . 7
45 43 , 44 syl6eq 2514 . . . . . 6
46 42 fveq2d 5875 . . . . . . . . 9
47 sin0 13884 . . . . . . . . 9
48 46 , 47 syl6eq 2514 . . . . . . . 8
49 48 oveq2d 6312 . . . . . . 7
50 34 mul01i 9791 . . . . . . 7
51 49 , 50 syl6eq 2514 . . . . . 6
52 45 , 51 oveq12d 6314 . . . . 5
53 ax-1cn 9571 . . . . . 6
54 53 addid1i 9788 . . . . 5
55 52 , 54 syl6eq 2514 . . . 4
56 41 , 55 eqtr4d 2501 . . 3
57 expp1 12173 . . . . . . . . 9
58 39 , 57 sylan 471 . . . . . . . 8
59 58 ancoms 453 . . . . . . 7
60 59 adantr 465 . . . . . 6
61 oveq1 6303 . . . . . . 7
62 61 adantl 466 . . . . . 6
63 nn0cn 10830 . . . . . . . . . . . . 13
64 mulcl 9597 . . . . . . . . . . . . 13
65 63 , 64 sylan 471 . . . . . . . . . . . 12
66 sinadd 13899 . . . . . . . . . . . 12
67 65 , 66 sylancom 667 . . . . . . . . . . 11
68 33 adantl 466 . . . . . . . . . . . . 13
69 sincl 13861 . . . . . . . . . . . . . 14
70 65 , 69 syl 16 . . . . . . . . . . . . 13
71 mulcom 9599 . . . . . . . . . . . . 13
72 68 , 70 , 71 syl2anc 661 . . . . . . . . . . . 12
73 72 oveq1d 6311 . . . . . . . . . . 11
74 mulcl 9597 . . . . . . . . . . . . 13
75 68 , 70 , 74 syl2anc 661 . . . . . . . . . . . 12
76 coscl 13862 . . . . . . . . . . . . . 14
77 65 , 76 syl 16 . . . . . . . . . . . . 13
78 35 adantl 466 . . . . . . . . . . . . 13
79 mulcl 9597 . . . . . . . . . . . . 13
80 77 , 78 , 79 syl2anc 661 . . . . . . . . . . . 12
81 addcom 9787 . . . . . . . . . . . 12
82 75 , 80 , 81 syl2anc 661 . . . . . . . . . . 11
83 67 , 73 , 82 3eqtr2d 2504 . . . . . . . . . 10
84 83 oveq2d 6312 . . . . . . . . 9
85 84 oveq2d 6312 . . . . . . . 8
86 adddir 9608 . . . . . . . . . . . . 13
87 mulid2 9615 . . . . . . . . . . . . . . 15
88 87 oveq2d 6312 . . . . . . . . . . . . . 14
89 88 3ad2ant3 1019 . . . . . . . . . . . . 13
90 86 , 89 eqtrd 2498 . . . . . . . . . . . 12
91 63 , 90 syl3an1 1261 . . . . . . . . . . 11
92 53 , 91 mp3an2 1312 . . . . . . . . . 10
93 92 fveq2d 5875 . . . . . . . . 9
94 92 fveq2d 5875 . . . . . . . . . 10
95 94 oveq2d 6312 . . . . . . . . 9
96 93 , 95 oveq12d 6314 . . . . . . . 8
97 mulcl 9597 . . . . . . . . . . . . . 14
98 34 , 97 mpan 670 . . . . . . . . . . . . 13
99 65 , 69 , 98 3syl 20 . . . . . . . . . . . 12
100 33 , 37 jca 532 . . . . . . . . . . . . 13
101 100 adantl 466 . . . . . . . . . . . 12
102 muladd 10014 . . . . . . . . . . . 12
103 77 , 99 , 101 , 102 syl21anc 1227 . . . . . . . . . . 11
104 78 , 34 jctil 537 . . . . . . . . . . . . . 14
105 70 , 34 jctil 537 . . . . . . . . . . . . . 14
106 mul4 9770 . . . . . . . . . . . . . . 15
107 ixi 10203 . . . . . . . . . . . . . . . 16
108 107 oveq1i 6306 . . . . . . . . . . . . . . 15
109 106 , 108 syl6eq 2514 . . . . . . . . . . . . . 14
110 104 , 105 ,
109 syl2anc 661 . . . . . . . . . . . . 13
111 110 oveq2d 6312 . . . . . . . . . . . 12
112 111 oveq1d 6311 . . . . . . . . . . 11
113 mul12 9767 . . . . . . . . . . . . . . . 16
114 34 , 113 mp3an2 1312 . . . . . . . . . . . . . . 15
115 77 , 78 , 114 syl2anc 661 . . . . . . . . . . . . . 14
116 mul12 9767 . . . . . . . . . . . . . . . 16
117 34 , 116 mp3an2 1312 . . . . . . . . . . . . . . 15
118 68 , 70 , 117 syl2anc 661 . . . . . . . . . . . . . 14
119 115 , 118 oveq12d 6314 . . . . . . . . . . . . 13
120 adddi 9602 . . . . . . . . . . . . . . 15
121 34 , 120 mp3an1 1311 . . . . . . . . . . . . . 14
122 80 , 75 , 121 syl2anc 661 . . . . . . . . . . . . 13
123 119 , 122 eqtr4d 2501 . . . . . . . . . . . 12
124 123 oveq2d 6312 . . . . . . . . . . 11
125 103 , 112 ,
124 3eqtrd 2502 . . . . . . . . . 10
126 mulcl 9597 . . . . . . . . . . . . . 14
127 78 , 70 , 126 syl2anc 661 . . . . . . . . . . . . 13
128 mulm1 10023 . . . . . . . . . . . . 13
129 127 , 128 syl 16 . . . . . . . . . . . 12
130 129 oveq2d 6312 . . . . . . . . . . 11
131 130 oveq1d 6311 . . . . . . . . . 10
132 mulcl 9597 . . . . . . . . . . . . 13
133 77 , 68 , 132 syl2anc 661 . . . . . . . . . . . 12
134 negsub 9890 . . . . . . . . . . . 12
135 133 , 127 ,
134 syl2anc 661 . . . . . . . . . . 11
136 135 oveq1d 6311 . . . . . . . . . 10
137 125 , 131 ,
136 3eqtrd 2502 . . . . . . . . 9
138 cosadd 13900 . . . . . . . . . . . 12
139 65 , 138 sylancom 667 . . . . . . . . . . 11
140 mulcom 9599 . . . . . . . . . . . . 13
141 70 , 78 , 140 syl2anc 661 . . . . . . . . . . . 12
142 141 oveq2d 6312 . . . . . . . . . . 11
143 139 , 142 eqtrd 2498 . . . . . . . . . 10
144 143 oveq1d 6311 . . . . . . . . 9
145 137 , 144 eqtr4d 2501 . . . . . . . 8
146 85 , 96 , 145 3eqtr4rd 2509 . . . . . . 7
147 146 adantr 465 . . . . . 6
148 60 , 62 , 147 3eqtrd 2502 . . . . 5
149 148 exp31 604 . . . 4
150 149 a2d 26 . . 3
151 8 , 16 , 24 , 32 , 56 , 150 nn0ind 10984 . 2
152 151 impcom 430 1
