Proof of Theorem tangtx
Step | Hyp | Ref
| Expression |
1 | | elioore 12205 |
. . . . 5
|
2 | 1 | recoscld 14874 |
. . . . 5
|
3 | 1, 2 | remulcld 10070 |
. . . 4
|
4 | | 1re 10039 |
. . . . . . 7
|
5 | | rehalfcl 11258 |
. . . . . . . . . 10
|
6 | 1, 5 | syl 17 |
. . . . . . . . 9
|
7 | 6 | resqcld 13035 |
. . . . . . . 8
|
8 | | 3nn 11186 |
. . . . . . . 8
|
9 | | nndivre 11056 |
. . . . . . . 8
|
10 | 7, 8, 9 | sylancl 694 |
. . . . . . 7
|
11 | | resubcl 10345 |
. . . . . . 7
|
12 | 4, 10, 11 | sylancr 695 |
. . . . . 6
|
13 | 1, 12 | remulcld 10070 |
. . . . 5
|
14 | | 2re 11090 |
. . . . . . 7
|
15 | | remulcl 10021 |
. . . . . . 7
|
16 | 14, 10, 15 | sylancr 695 |
. . . . . 6
|
17 | | resubcl 10345 |
. . . . . 6
|
18 | 4, 16, 17 | sylancr 695 |
. . . . 5
|
19 | 13, 18 | remulcld 10070 |
. . . 4
|
20 | 1 | resincld 14873 |
. . . 4
|
21 | 12 | resqcld 13035 |
. . . . . . . . 9
|
22 | | remulcl 10021 |
. . . . . . . . 9
|
23 | 14, 21, 22 | sylancr 695 |
. . . . . . . 8
|
24 | | resubcl 10345 |
. . . . . . . 8
|
25 | 23, 4, 24 | sylancl 694 |
. . . . . . 7
|
26 | 12, 18 | remulcld 10070 |
. . . . . . 7
|
27 | 1 | recnd 10068 |
. . . . . . . . . . 11
|
28 | | 2cn 11091 |
. . . . . . . . . . . 12
|
29 | 28 | a1i 11 |
. . . . . . . . . . 11
|
30 | | 2ne0 11113 |
. . . . . . . . . . . 12
|
31 | 30 | a1i 11 |
. . . . . . . . . . 11
|
32 | 27, 29, 31 | divcan2d 10803 |
. . . . . . . . . 10
|
33 | 32 | fveq2d 6195 |
. . . . . . . . 9
|
34 | 6 | recnd 10068 |
. . . . . . . . . 10
|
35 | | cos2t 14908 |
. . . . . . . . . 10
|
36 | 34, 35 | syl 17 |
. . . . . . . . 9
|
37 | 33, 36 | eqtr3d 2658 |
. . . . . . . 8
|
38 | 6 | recoscld 14874 |
. . . . . . . . . . 11
|
39 | 38 | resqcld 13035 |
. . . . . . . . . 10
|
40 | | remulcl 10021 |
. . . . . . . . . 10
|
41 | 14, 39, 40 | sylancr 695 |
. . . . . . . . 9
|
42 | 4 | a1i 11 |
. . . . . . . . 9
|
43 | 14 | a1i 11 |
. . . . . . . . . . . . . . 15
|
44 | | eliooord 12233 |
. . . . . . . . . . . . . . . 16
|
45 | 44 | simpld 475 |
. . . . . . . . . . . . . . 15
|
46 | | 2pos 11112 |
. . . . . . . . . . . . . . . 16
|
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . 15
|
48 | 1, 43, 45, 47 | divgt0d 10959 |
. . . . . . . . . . . . . 14
|
49 | | pire 24210 |
. . . . . . . . . . . . . . . . . . 19
|
50 | | rehalfcl 11258 |
. . . . . . . . . . . . . . . . . . 19
|
51 | 49, 50 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
|
52 | 44 | simprd 479 |
. . . . . . . . . . . . . . . . . 18
|
53 | | pigt2lt4 24208 |
. . . . . . . . . . . . . . . . . . . . . 22
|
54 | 53 | simpri 478 |
. . . . . . . . . . . . . . . . . . . . 21
|
55 | | 2t2e4 11177 |
. . . . . . . . . . . . . . . . . . . . 21
|
56 | 54, 55 | breqtrri 4680 |
. . . . . . . . . . . . . . . . . . . 20
|
57 | 14, 46 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . 21
|
58 | | ltdivmul 10898 |
. . . . . . . . . . . . . . . . . . . . 21
|
59 | 49, 14, 57, 58 | mp3an 1424 |
. . . . . . . . . . . . . . . . . . . 20
|
60 | 56, 59 | mpbir 221 |
. . . . . . . . . . . . . . . . . . 19
|
61 | 60 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
62 | 1, 51, 43, 52, 61 | lttrd 10198 |
. . . . . . . . . . . . . . . . 17
|
63 | 28 | mulid2i 10043 |
. . . . . . . . . . . . . . . . 17
|
64 | 62, 63 | syl6breqr 4695 |
. . . . . . . . . . . . . . . 16
|
65 | | ltdivmul2 10900 |
. . . . . . . . . . . . . . . . 17
|
66 | 1, 42, 43, 47, 65 | syl112anc 1330 |
. . . . . . . . . . . . . . . 16
|
67 | 64, 66 | mpbird 247 |
. . . . . . . . . . . . . . 15
|
68 | 6, 42, 67 | ltled 10185 |
. . . . . . . . . . . . . 14
|
69 | | 0xr 10086 |
. . . . . . . . . . . . . . 15
|
70 | | elioc2 12236 |
. . . . . . . . . . . . . . 15
|
71 | 69, 4, 70 | mp2an 708 |
. . . . . . . . . . . . . 14
|
72 | 6, 48, 68, 71 | syl3anbrc 1246 |
. . . . . . . . . . . . 13
|
73 | | cos01bnd 14916 |
. . . . . . . . . . . . 13
|
74 | 72, 73 | syl 17 |
. . . . . . . . . . . 12
|
75 | 74 | simprd 479 |
. . . . . . . . . . 11
|
76 | | cos01gt0 14921 |
. . . . . . . . . . . . . 14
|
77 | 72, 76 | syl 17 |
. . . . . . . . . . . . 13
|
78 | | 0re 10040 |
. . . . . . . . . . . . . 14
|
79 | | ltle 10126 |
. . . . . . . . . . . . . 14
|
80 | 78, 38, 79 | sylancr 695 |
. . . . . . . . . . . . 13
|
81 | 77, 80 | mpd 15 |
. . . . . . . . . . . 12
|
82 | 78 | a1i 11 |
. . . . . . . . . . . . 13
|
83 | 82, 38, 12, 77, 75 | lttrd 10198 |
. . . . . . . . . . . . 13
|
84 | 82, 12, 83 | ltled 10185 |
. . . . . . . . . . . 12
|
85 | 38, 12, 81, 84 | lt2sqd 13043 |
. . . . . . . . . . 11
|
86 | 75, 85 | mpbid 222 |
. . . . . . . . . 10
|
87 | | ltmul2 10874 |
. . . . . . . . . . 11
|
88 | 39, 21, 43, 47, 87 | syl112anc 1330 |
. . . . . . . . . 10
|
89 | 86, 88 | mpbid 222 |
. . . . . . . . 9
|
90 | 41, 23, 42, 89 | ltsub1dd 10639 |
. . . . . . . 8
|
91 | 37, 90 | eqbrtrd 4675 |
. . . . . . 7
|
92 | | 3re 11094 |
. . . . . . . . . 10
|
93 | | remulcl 10021 |
. . . . . . . . . 10
|
94 | 92, 10, 93 | sylancr 695 |
. . . . . . . . 9
|
95 | | 4re 11097 |
. . . . . . . . . 10
|
96 | | remulcl 10021 |
. . . . . . . . . 10
|
97 | 95, 10, 96 | sylancr 695 |
. . . . . . . . 9
|
98 | 10 | resqcld 13035 |
. . . . . . . . . . 11
|
99 | | remulcl 10021 |
. . . . . . . . . . 11
|
100 | 14, 98, 99 | sylancr 695 |
. . . . . . . . . 10
|
101 | | readdcl 10019 |
. . . . . . . . . 10
|
102 | 4, 100, 101 | sylancr 695 |
. . . . . . . . 9
|
103 | | 3lt4 11197 |
. . . . . . . . . 10
|
104 | 92 | a1i 11 |
. . . . . . . . . . 11
|
105 | 95 | a1i 11 |
. . . . . . . . . . 11
|
106 | 48 | gt0ne0d 10592 |
. . . . . . . . . . . . 13
|
107 | 6, 106 | sqgt0d 13037 |
. . . . . . . . . . . 12
|
108 | | 3pos 11114 |
. . . . . . . . . . . . 13
|
109 | 108 | a1i 11 |
. . . . . . . . . . . 12
|
110 | 7, 104, 107, 109 | divgt0d 10959 |
. . . . . . . . . . 11
|
111 | | ltmul1 10873 |
. . . . . . . . . . 11
|
112 | 104, 105,
10, 110, 111 | syl112anc 1330 |
. . . . . . . . . 10
|
113 | 103, 112 | mpbii 223 |
. . . . . . . . 9
|
114 | 94, 97, 102, 113 | ltsub2dd 10640 |
. . . . . . . 8
|
115 | | sq1 12958 |
. . . . . . . . . . . . . . . 16
|
116 | 115 | a1i 11 |
. . . . . . . . . . . . . . 15
|
117 | 10 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
|
118 | 117 | mulid2d 10058 |
. . . . . . . . . . . . . . . 16
|
119 | 118 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
120 | 116, 119 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
121 | 120 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
122 | | ax-1cn 9994 |
. . . . . . . . . . . . . 14
|
123 | | binom2sub 12981 |
. . . . . . . . . . . . . 14
|
124 | 122, 117,
123 | sylancr 695 |
. . . . . . . . . . . . 13
|
125 | 42 | recnd 10068 |
. . . . . . . . . . . . . 14
|
126 | 98 | recnd 10068 |
. . . . . . . . . . . . . 14
|
127 | 16 | recnd 10068 |
. . . . . . . . . . . . . 14
|
128 | 125, 126,
127 | addsubd 10413 |
. . . . . . . . . . . . 13
|
129 | 121, 124,
128 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
|
130 | 129 | oveq2d 6666 |
. . . . . . . . . . 11
|
131 | | addcl 10018 |
. . . . . . . . . . . . 13
|
132 | 122, 126,
131 | sylancr 695 |
. . . . . . . . . . . 12
|
133 | 29, 132, 127 | subdid 10486 |
. . . . . . . . . . 11
|
134 | 29, 125, 126 | adddid 10064 |
. . . . . . . . . . . . . 14
|
135 | 122 | 2timesi 11147 |
. . . . . . . . . . . . . . . 16
|
136 | 135 | oveq1i 6660 |
. . . . . . . . . . . . . . 15
|
137 | 100 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
138 | 125, 125,
137 | addassd 10062 |
. . . . . . . . . . . . . . 15
|
139 | 136, 138 | syl5eq 2668 |
. . . . . . . . . . . . . 14
|
140 | 134, 139 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
141 | 55 | oveq1i 6660 |
. . . . . . . . . . . . . 14
|
142 | 29, 29, 117 | mulassd 10063 |
. . . . . . . . . . . . . 14
|
143 | 141, 142 | syl5reqr 2671 |
. . . . . . . . . . . . 13
|
144 | 140, 143 | oveq12d 6668 |
. . . . . . . . . . . 12
|
145 | | addcl 10018 |
. . . . . . . . . . . . . 14
|
146 | 122, 137,
145 | sylancr 695 |
. . . . . . . . . . . . 13
|
147 | 97 | recnd 10068 |
. . . . . . . . . . . . 13
|
148 | 125, 146,
147 | addsubassd 10412 |
. . . . . . . . . . . 12
|
149 | 144, 148 | eqtrd 2656 |
. . . . . . . . . . 11
|
150 | 130, 133,
149 | 3eqtrd 2660 |
. . . . . . . . . 10
|
151 | 150 | oveq1d 6665 |
. . . . . . . . 9
|
152 | 146, 147 | subcld 10392 |
. . . . . . . . . 10
|
153 | | pncan2 10288 |
. . . . . . . . . 10
|
154 | 122, 152,
153 | sylancr 695 |
. . . . . . . . 9
|
155 | 151, 154 | eqtrd 2656 |
. . . . . . . 8
|
156 | | subcl 10280 |
. . . . . . . . . . 11
|
157 | 122, 117,
156 | sylancr 695 |
. . . . . . . . . 10
|
158 | 157, 125,
127 | subdid 10486 |
. . . . . . . . 9
|
159 | 157 | mulid1d 10057 |
. . . . . . . . . 10
|
160 | 125, 117,
127 | subdird 10487 |
. . . . . . . . . . 11
|
161 | 127 | mulid2d 10058 |
. . . . . . . . . . . 12
|
162 | 117, 29, 117 | mul12d 10245 |
. . . . . . . . . . . . 13
|
163 | 117 | sqvald 13005 |
. . . . . . . . . . . . . 14
|
164 | 163 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
165 | 162, 164 | eqtr4d 2659 |
. . . . . . . . . . . 12
|
166 | 161, 165 | oveq12d 6668 |
. . . . . . . . . . 11
|
167 | 160, 166 | eqtrd 2656 |
. . . . . . . . . 10
|
168 | 159, 167 | oveq12d 6668 |
. . . . . . . . 9
|
169 | 125, 117,
127, 137 | subadd4d 10440 |
. . . . . . . . . 10
|
170 | | df-3 11080 |
. . . . . . . . . . . . . 14
|
171 | 28, 122 | addcomi 10227 |
. . . . . . . . . . . . . 14
|
172 | 170, 171 | eqtri 2644 |
. . . . . . . . . . . . 13
|
173 | 172 | oveq1i 6660 |
. . . . . . . . . . . 12
|
174 | 125, 29, 117 | adddird 10065 |
. . . . . . . . . . . . 13
|
175 | 118 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
176 | 174, 175 | eqtrd 2656 |
. . . . . . . . . . . 12
|
177 | 173, 176 | syl5eq 2668 |
. . . . . . . . . . 11
|
178 | 177 | oveq2d 6666 |
. . . . . . . . . 10
|
179 | 169, 178 | eqtr4d 2659 |
. . . . . . . . 9
|
180 | 158, 168,
179 | 3eqtrd 2660 |
. . . . . . . 8
|
181 | 114, 155,
180 | 3brtr4d 4685 |
. . . . . . 7
|
182 | 2, 25, 26, 91, 181 | lttrd 10198 |
. . . . . 6
|
183 | | ltmul2 10874 |
. . . . . . 7
|
184 | 2, 26, 1, 45, 183 | syl112anc 1330 |
. . . . . 6
|
185 | 182, 184 | mpbid 222 |
. . . . 5
|
186 | 18 | recnd 10068 |
. . . . . 6
|
187 | 27, 157, 186 | mulassd 10063 |
. . . . 5
|
188 | 185, 187 | breqtrrd 4681 |
. . . 4
|
189 | 13, 38 | remulcld 10070 |
. . . . 5
|
190 | 74 | simpld 475 |
. . . . . 6
|
191 | 1, 12, 45, 83 | mulgt0d 10192 |
. . . . . . 7
|
192 | | ltmul2 10874 |
. . . . . . 7
|
193 | 18, 38, 13, 191, 192 | syl112anc 1330 |
. . . . . 6
|
194 | 190, 193 | mpbid 222 |
. . . . 5
|
195 | 29, 34, 157 | mulassd 10063 |
. . . . . . . . 9
|
196 | 32 | oveq1d 6665 |
. . . . . . . . 9
|
197 | 34, 125, 117 | subdid 10486 |
. . . . . . . . . . 11
|
198 | 34 | mulid1d 10057 |
. . . . . . . . . . . 12
|
199 | 170 | oveq2i 6661 |
. . . . . . . . . . . . . . . 16
|
200 | | 2nn0 11309 |
. . . . . . . . . . . . . . . . 17
|
201 | | expp1 12867 |
. . . . . . . . . . . . . . . . 17
|
202 | 34, 200, 201 | sylancl 694 |
. . . . . . . . . . . . . . . 16
|
203 | 199, 202 | syl5eq 2668 |
. . . . . . . . . . . . . . 15
|
204 | 7 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
205 | 204, 34 | mulcomd 10061 |
. . . . . . . . . . . . . . 15
|
206 | 203, 205 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
207 | 206 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
208 | | 3cn 11095 |
. . . . . . . . . . . . . . 15
|
209 | 208 | a1i 11 |
. . . . . . . . . . . . . 14
|
210 | | 3ne0 11115 |
. . . . . . . . . . . . . . 15
|
211 | 210 | a1i 11 |
. . . . . . . . . . . . . 14
|
212 | 34, 204, 209, 211 | divassd 10836 |
. . . . . . . . . . . . 13
|
213 | 207, 212 | eqtr2d 2657 |
. . . . . . . . . . . 12
|
214 | 198, 213 | oveq12d 6668 |
. . . . . . . . . . 11
|
215 | 197, 214 | eqtrd 2656 |
. . . . . . . . . 10
|
216 | 215 | oveq2d 6666 |
. . . . . . . . 9
|
217 | 195, 196,
216 | 3eqtr3d 2664 |
. . . . . . . 8
|
218 | | sin01bnd 14915 |
. . . . . . . . . . 11
|
219 | 72, 218 | syl 17 |
. . . . . . . . . 10
|
220 | 219 | simpld 475 |
. . . . . . . . 9
|
221 | | 3nn0 11310 |
. . . . . . . . . . . . 13
|
222 | | reexpcl 12877 |
. . . . . . . . . . . . 13
|
223 | 6, 221, 222 | sylancl 694 |
. . . . . . . . . . . 12
|
224 | | nndivre 11056 |
. . . . . . . . . . . 12
|
225 | 223, 8, 224 | sylancl 694 |
. . . . . . . . . . 11
|
226 | 6, 225 | resubcld 10458 |
. . . . . . . . . 10
|
227 | 6 | resincld 14873 |
. . . . . . . . . 10
|
228 | | ltmul2 10874 |
. . . . . . . . . 10
|
229 | 226, 227,
43, 47, 228 | syl112anc 1330 |
. . . . . . . . 9
|
230 | 220, 229 | mpbid 222 |
. . . . . . . 8
|
231 | 217, 230 | eqbrtrd 4675 |
. . . . . . 7
|
232 | | remulcl 10021 |
. . . . . . . . 9
|
233 | 14, 227, 232 | sylancr 695 |
. . . . . . . 8
|
234 | | ltmul1 10873 |
. . . . . . . 8
|
235 | 13, 233, 38, 77, 234 | syl112anc 1330 |
. . . . . . 7
|
236 | 231, 235 | mpbid 222 |
. . . . . 6
|
237 | 227 | recnd 10068 |
. . . . . . . 8
|
238 | 38 | recnd 10068 |
. . . . . . . 8
|
239 | 29, 237, 238 | mulassd 10063 |
. . . . . . 7
|
240 | | sin2t 14907 |
. . . . . . . 8
|
241 | 34, 240 | syl 17 |
. . . . . . 7
|
242 | 32 | fveq2d 6195 |
. . . . . . 7
|
243 | 239, 241,
242 | 3eqtr2rd 2663 |
. . . . . 6
|
244 | 236, 243 | breqtrrd 4681 |
. . . . 5
|
245 | 19, 189, 20, 194, 244 | lttrd 10198 |
. . . 4
|
246 | 3, 19, 20, 188, 245 | lttrd 10198 |
. . 3
|
247 | | sincosq1sgn 24250 |
. . . . 5
|
248 | 247 | simprd 479 |
. . . 4
|
249 | | ltmuldiv 10896 |
. . . 4
|
250 | 1, 20, 2, 248, 249 | syl112anc 1330 |
. . 3
|
251 | 246, 250 | mpbid 222 |
. 2
|
252 | 248 | gt0ne0d 10592 |
. . 3
|
253 | | tanval 14858 |
. . 3
|
254 | 27, 252, 253 | syl2anc 693 |
. 2
|
255 | 251, 254 | breqtrrd 4681 |
1
|