Proof of Theorem tangtx
Step | Hyp | Ref
| Expression |
1 | | elioore 11691 |
. . . . 5
         |
2 | 1 | recoscld 14275 |
. . . . 5
             |
3 | 1, 2 | remulcld 9689 |
. . . 4
       
       |
4 | | 1re 9660 |
. . . . . . 7
 |
5 | | rehalfcl 10862 |
. . . . . . . . . 10
     |
6 | 1, 5 | syl 17 |
. . . . . . . . 9
           |
7 | 6 | resqcld 12480 |
. . . . . . . 8
               |
8 | | 3nn 10791 |
. . . . . . . 8
 |
9 | | nndivre 10667 |
. . . . . . . 8
       
           |
10 | 7, 8, 9 | sylancl 675 |
. . . . . . 7
                 |
11 | | resubcl 9958 |
. . . . . . 7
                       |
12 | 4, 10, 11 | sylancr 676 |
. . . . . 6
                   |
13 | 1, 12 | remulcld 9689 |
. . . . 5
       
             |
14 | | 2re 10701 |
. . . . . . 7
 |
15 | | remulcl 9642 |
. . . . . . 7
                       |
16 | 14, 10, 15 | sylancr 676 |
. . . . . 6
                   |
17 | | resubcl 9958 |
. . . . . 6
                           |
18 | 4, 16, 17 | sylancr 676 |
. . . . 5
                     |
19 | 13, 18 | remulcld 9689 |
. . . 4
                                   |
20 | 1 | resincld 14274 |
. . . 4
             |
21 | 12 | resqcld 12480 |
. . . . . . . . 9
                       |
22 | | remulcl 9642 |
. . . . . . . . 9
                                   |
23 | 14, 21, 22 | sylancr 676 |
. . . . . . . 8
                         |
24 | | resubcl 9958 |
. . . . . . . 8
                 
                     |
25 | 23, 4, 24 | sylancl 675 |
. . . . . . 7
                           |
26 | 12, 18 | remulcld 9689 |
. . . . . . 7
                                 |
27 | 1 | recnd 9687 |
. . . . . . . . . . 11
         |
28 | | 2cn 10702 |
. . . . . . . . . . . 12
 |
29 | 28 | a1i 11 |
. . . . . . . . . . 11
         |
30 | | 2ne0 10724 |
. . . . . . . . . . . 12
 |
31 | 30 | a1i 11 |
. . . . . . . . . . 11
         |
32 | 27, 29, 31 | divcan2d 10407 |
. . . . . . . . . 10
             |
33 | 32 | fveq2d 5883 |
. . . . . . . . 9
                     |
34 | 6 | recnd 9687 |
. . . . . . . . . 10
           |
35 | | cos2t 14309 |
. . . . . . . . . 10
                           |
36 | 34, 35 | syl 17 |
. . . . . . . . 9
                               |
37 | 33, 36 | eqtr3d 2507 |
. . . . . . . 8
                           |
38 | 6 | recoscld 14275 |
. . . . . . . . . . 11
               |
39 | 38 | resqcld 12480 |
. . . . . . . . . 10
                   |
40 | | remulcl 9642 |
. . . . . . . . . 10
                           |
41 | 14, 39, 40 | sylancr 676 |
. . . . . . . . 9
                     |
42 | 4 | a1i 11 |
. . . . . . . . 9
         |
43 | 14 | a1i 11 |
. . . . . . . . . . . . . . 15
         |
44 | | eliooord 11719 |
. . . . . . . . . . . . . . . 16
       
     |
45 | 44 | simpld 466 |
. . . . . . . . . . . . . . 15
         |
46 | | 2pos 10723 |
. . . . . . . . . . . . . . . 16
 |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . 15
         |
48 | 1, 43, 45, 47 | divgt0d 10564 |
. . . . . . . . . . . . . 14
           |
49 | | pire 23492 |
. . . . . . . . . . . . . . . . . . 19
 |
50 | | rehalfcl 10862 |
. . . . . . . . . . . . . . . . . . 19
 
   |
51 | 49, 50 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
       
   |
52 | 44 | simprd 470 |
. . . . . . . . . . . . . . . . . 18
           |
53 | | pigt2lt4 23490 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
54 | 53 | simpri 469 |
. . . . . . . . . . . . . . . . . . . . 21
 |
55 | | 2t2e4 10782 |
. . . . . . . . . . . . . . . . . . . . 21
   |
56 | 54, 55 | breqtrri 4421 |
. . . . . . . . . . . . . . . . . . . 20
   |
57 | 14, 46 | pm3.2i 462 |
. . . . . . . . . . . . . . . . . . . . 21
   |
58 | | ltdivmul 10502 |
. . . . . . . . . . . . . . . . . . . . 21
 
     
     |
59 | 49, 14, 57, 58 | mp3an 1390 |
. . . . . . . . . . . . . . . . . . . 20
  
    |
60 | 56, 59 | mpbir 214 |
. . . . . . . . . . . . . . . . . . 19
   |
61 | 60 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
       
   |
62 | 1, 51, 43, 52, 61 | lttrd 9813 |
. . . . . . . . . . . . . . . . 17
         |
63 | 28 | mulid2i 9664 |
. . . . . . . . . . . . . . . . 17
   |
64 | 62, 63 | syl6breqr 4436 |
. . . . . . . . . . . . . . . 16
           |
65 | | ltdivmul2 10504 |
. . . . . . . . . . . . . . . . 17
 
     
     |
66 | 1, 42, 43, 47, 65 | syl112anc 1296 |
. . . . . . . . . . . . . . . 16
         
     |
67 | 64, 66 | mpbird 240 |
. . . . . . . . . . . . . . 15
           |
68 | 6, 42, 67 | ltled 9800 |
. . . . . . . . . . . . . 14
           |
69 | | 0xr 9705 |
. . . . . . . . . . . . . . 15
 |
70 | | elioc2 11722 |
. . . . . . . . . . . . . . 15
        ![(,] (,]](_ioc.gif) 
    
      |
71 | 69, 4, 70 | mp2an 686 |
. . . . . . . . . . . . . 14
     ![(,] (,]](_ioc.gif) 
    
     |
72 | 6, 48, 68, 71 | syl3anbrc 1214 |
. . . . . . . . . . . . 13
           ![(,] (,]](_ioc.gif)    |
73 | | cos01bnd 14317 |
. . . . . . . . . . . . 13
     ![(,] (,]](_ioc.gif)                                        |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . 12
                                             |
75 | 74 | simprd 470 |
. . . . . . . . . . 11
                         |
76 | | cos01gt0 14322 |
. . . . . . . . . . . . . 14
     ![(,] (,]](_ioc.gif)          |
77 | 72, 76 | syl 17 |
. . . . . . . . . . . . 13
               |
78 | | 0re 9661 |
. . . . . . . . . . . . . 14
 |
79 | | ltle 9740 |
. . . . . . . . . . . . . 14
               
         |
80 | 78, 38, 79 | sylancr 676 |
. . . . . . . . . . . . 13
       
               |
81 | 77, 80 | mpd 15 |
. . . . . . . . . . . 12
               |
82 | 78 | a1i 11 |
. . . . . . . . . . . . 13
         |
83 | 82, 38, 12, 77, 75 | lttrd 9813 |
. . . . . . . . . . . . 13
                   |
84 | 82, 12, 83 | ltled 9800 |
. . . . . . . . . . . 12
                   |
85 | 38, 12, 81, 84 | lt2sqd 12488 |
. . . . . . . . . . 11
                       
                           |
86 | 75, 85 | mpbid 215 |
. . . . . . . . . 10
                                 |
87 | | ltmul2 10478 |
. . . . . . . . . . 11
                                                     
                               |
88 | 39, 21, 43, 47, 87 | syl112anc 1296 |
. . . . . . . . . 10
                                                               |
89 | 86, 88 | mpbid 215 |
. . . . . . . . 9
                                     |
90 | 41, 23, 42, 89 | ltsub1dd 10246 |
. . . . . . . 8
                                         |
91 | 37, 90 | eqbrtrd 4416 |
. . . . . . 7
                               |
92 | | 3re 10705 |
. . . . . . . . . 10
 |
93 | | remulcl 9642 |
. . . . . . . . . 10
                       |
94 | 92, 10, 93 | sylancr 676 |
. . . . . . . . 9
                   |
95 | | 4re 10708 |
. . . . . . . . . 10
 |
96 | | remulcl 9642 |
. . . . . . . . . 10
                       |
97 | 95, 10, 96 | sylancr 676 |
. . . . . . . . 9
                   |
98 | 10 | resqcld 12480 |
. . . . . . . . . . 11
                     |
99 | | remulcl 9642 |
. . . . . . . . . . 11
                               |
100 | 14, 98, 99 | sylancr 676 |
. . . . . . . . . 10
                       |
101 | | readdcl 9640 |
. . . . . . . . . 10
                                   |
102 | 4, 100, 101 | sylancr 676 |
. . . . . . . . 9
                         |
103 | | 3lt4 10802 |
. . . . . . . . . 10
 |
104 | 92 | a1i 11 |
. . . . . . . . . . 11
         |
105 | 95 | a1i 11 |
. . . . . . . . . . 11
         |
106 | 48 | gt0ne0d 10199 |
. . . . . . . . . . . . 13
           |
107 | 6, 106 | sqgt0d 12482 |
. . . . . . . . . . . 12
               |
108 | | 3pos 10725 |
. . . . . . . . . . . . 13
 |
109 | 108 | a1i 11 |
. . . . . . . . . . . 12
         |
110 | 7, 104, 107, 109 | divgt0d 10564 |
. . . . . . . . . . 11
                 |
111 | | ltmul1 10477 |
. . . . . . . . . . 11
 
                                           |
112 | 104, 105,
10, 110, 111 | syl112anc 1296 |
. . . . . . . . . 10
       
                       |
113 | 103, 112 | mpbii 216 |
. . . . . . . . 9
                             |
114 | 94, 97, 102, 113 | ltsub2dd 10247 |
. . . . . . . 8
                                                                 |
115 | | sq1 12407 |
. . . . . . . . . . . . . . . 16
     |
116 | 115 | a1i 11 |
. . . . . . . . . . . . . . 15
             |
117 | 10 | recnd 9687 |
. . . . . . . . . . . . . . . . 17
                 |
118 | 117 | mulid2d 9679 |
. . . . . . . . . . . . . . . 16
                           |
119 | 118 | oveq2d 6324 |
. . . . . . . . . . . . . . 15
                               |
120 | 116, 119 | oveq12d 6326 |
. . . . . . . . . . . . . 14
                                       |
121 | 120 | oveq1d 6323 |
. . . . . . . . . . . . 13
                                                                   |
122 | | ax-1cn 9615 |
. . . . . . . . . . . . . 14
 |
123 | | binom2sub 12429 |
. . . . . . . . . . . . . 14
                                                           |
124 | 122, 117,
123 | sylancr 676 |
. . . . . . . . . . . . 13
                                                       |
125 | 42 | recnd 9687 |
. . . . . . . . . . . . . 14
         |
126 | 98 | recnd 9687 |
. . . . . . . . . . . . . 14
                     |
127 | 16 | recnd 9687 |
. . . . . . . . . . . . . 14
                   |
128 | 125, 126,
127 | addsubd 10026 |
. . . . . . . . . . . . 13
                                                             |
129 | 121, 124,
128 | 3eqtr4d 2515 |
. . . . . . . . . . . 12
                                                 |
130 | 129 | oveq2d 6324 |
. . . . . . . . . . 11
                                                     |
131 | | addcl 9639 |
. . . . . . . . . . . . 13
                               |
132 | 122, 126,
131 | sylancr 676 |
. . . . . . . . . . . 12
                       |
133 | 29, 132, 127 | subdid 10095 |
. . . . . . . . . . 11
                                                                   |
134 | 29, 125, 126 | adddid 9685 |
. . . . . . . . . . . . . 14
                                           |
135 | 122 | 2timesi 10753 |
. . . . . . . . . . . . . . . 16
     |
136 | 135 | oveq1i 6318 |
. . . . . . . . . . . . . . 15
                                     |
137 | 100 | recnd 9687 |
. . . . . . . . . . . . . . . 16
                       |
138 | 125, 125,
137 | addassd 9683 |
. . . . . . . . . . . . . . 15
                                             |
139 | 136, 138 | syl5eq 2517 |
. . . . . . . . . . . . . 14
                                             |
140 | 134, 139 | eqtrd 2505 |
. . . . . . . . . . . . 13
                                           |
141 | 55 | oveq1i 6318 |
. . . . . . . . . . . . . 14
                       |
142 | 29, 29, 117 | mulassd 9684 |
. . . . . . . . . . . . . 14
                                 |
143 | 141, 142 | syl5reqr 2520 |
. . . . . . . . . . . . 13
                               |
144 | 140, 143 | oveq12d 6326 |
. . . . . . . . . . . 12
                                                                     |
145 | | addcl 9639 |
. . . . . . . . . . . . . 14
                                   |
146 | 122, 137,
145 | sylancr 676 |
. . . . . . . . . . . . 13
                         |
147 | 97 | recnd 9687 |
. . . . . . . . . . . . 13
                   |
148 | 125, 146,
147 | addsubassd 10025 |
. . . . . . . . . . . 12
                                                                     |
149 | 144, 148 | eqtrd 2505 |
. . . . . . . . . . 11
                                                                     |
150 | 130, 133,
149 | 3eqtrd 2509 |
. . . . . . . . . 10
                                                       |
151 | 150 | oveq1d 6323 |
. . . . . . . . 9
                                                           |
152 | 146, 147 | subcld 10005 |
. . . . . . . . . 10
                                     |
153 | | pncan2 9902 |
. . . . . . . . . 10
                                                                                             |
154 | 122, 152,
153 | sylancr 676 |
. . . . . . . . 9
                                                                     |
155 | 151, 154 | eqtrd 2505 |
. . . . . . . 8
                                                       |
156 | | subcl 9894 |
. . . . . . . . . . 11
                       |
157 | 122, 117,
156 | sylancr 676 |
. . . . . . . . . 10
                   |
158 | 157, 125,
127 | subdid 10095 |
. . . . . . . . 9
                                                                     |
159 | 157 | mulid1d 9678 |
. . . . . . . . . 10
                               |
160 | 125, 117,
127 | subdird 10096 |
. . . . . . . . . . 11
                                                                 |
161 | 127 | mulid2d 9679 |
. . . . . . . . . . . 12
                               |
162 | 117, 29, 117 | mul12d 9860 |
. . . . . . . . . . . . 13
                                                 |
163 | 117 | sqvald 12451 |
. . . . . . . . . . . . . 14
                                       |
164 | 163 | oveq2d 6324 |
. . . . . . . . . . . . 13
                                           |
165 | 162, 164 | eqtr4d 2508 |
. . . . . . . . . . . 12
                                           |
166 | 161, 165 | oveq12d 6326 |
. . . . . . . . . . 11
                                                                     |
167 | 160, 166 | eqtrd 2505 |
. . . . . . . . . 10
                                                         |
168 | 159, 167 | oveq12d 6326 |
. . . . . . . . 9
                                                                                   |
169 | 125, 117,
127, 137 | subadd4d 10053 |
. . . . . . . . . 10
                                                                                     |
170 | | df-3 10691 |
. . . . . . . . . . . . . 14
   |
171 | 28, 122 | addcomi 9842 |
. . . . . . . . . . . . . 14
     |
172 | 170, 171 | eqtri 2493 |
. . . . . . . . . . . . 13
   |
173 | 172 | oveq1i 6318 |
. . . . . . . . . . . 12
                       |
174 | 125, 29, 117 | adddird 9686 |
. . . . . . . . . . . . 13
                                           |
175 | 118 | oveq1d 6323 |
. . . . . . . . . . . . 13
                                                   |
176 | 174, 175 | eqtrd 2505 |
. . . . . . . . . . . 12
                                         |
177 | 173, 176 | syl5eq 2517 |
. . . . . . . . . . 11
                                       |
178 | 177 | oveq2d 6324 |
. . . . . . . . . 10
                                                                           |
179 | 169, 178 | eqtr4d 2508 |
. . . . . . . . 9
                                                                           |
180 | 158, 168,
179 | 3eqtrd 2509 |
. . . . . . . 8
                                                             |
181 | 114, 155,
180 | 3brtr4d 4426 |
. . . . . . 7
                                                   |
182 | 2, 25, 26, 91, 181 | lttrd 9813 |
. . . . . 6
                                     |
183 | | ltmul2 10478 |
. . . . . . 7
                              
 
                                                                |
184 | 2, 26, 1, 45, 183 | syl112anc 1296 |
. . . . . 6
           
                       
      
                            |
185 | 182, 184 | mpbid 215 |
. . . . 5
       
                                 |
186 | 18 | recnd 9687 |
. . . . . 6
                     |
187 | 27, 157, 186 | mulassd 9684 |
. . . . 5
                                                             |
188 | 185, 187 | breqtrrd 4422 |
. . . 4
       
                                 |
189 | 13, 38 | remulcld 9689 |
. . . . 5
                             |
190 | 74 | simpld 466 |
. . . . . 6
                           |
191 | 1, 12, 45, 83 | mulgt0d 9807 |
. . . . . . 7
                     |
192 | | ltmul2 10478 |
. . . . . . 7
                                                                                                                   |
193 | 18, 38, 13, 191, 192 | syl112anc 1296 |
. . . . . 6
                         
 
                                               |
194 | 190, 193 | mpbid 215 |
. . . . 5
                                                       |
195 | 29, 34, 157 | mulassd 9684 |
. . . . . . . . 9
                                         |
196 | 32 | oveq1d 6323 |
. . . . . . . . 9
                                     |
197 | 34, 125, 117 | subdid 10095 |
. . . . . . . . . . 11
                                         |
198 | 34 | mulid1d 9678 |
. . . . . . . . . . . 12
               |
199 | 170 | oveq2i 6319 |
. . . . . . . . . . . . . . . 16
               |
200 | | 2nn0 10910 |
. . . . . . . . . . . . . . . . 17
 |
201 | | expp1 12317 |
. . . . . . . . . . . . . . . . 17
   
                     |
202 | 34, 200, 201 | sylancl 675 |
. . . . . . . . . . . . . . . 16
                           |
203 | 199, 202 | syl5eq 2517 |
. . . . . . . . . . . . . . 15
                         |
204 | 7 | recnd 9687 |
. . . . . . . . . . . . . . . 16
               |
205 | 204, 34 | mulcomd 9682 |
. . . . . . . . . . . . . . 15
                             |
206 | 203, 205 | eqtrd 2505 |
. . . . . . . . . . . . . 14
                         |
207 | 206 | oveq1d 6323 |
. . . . . . . . . . . . 13
                             |
208 | | 3cn 10706 |
. . . . . . . . . . . . . . 15
 |
209 | 208 | a1i 11 |
. . . . . . . . . . . . . 14
         |
210 | | 3ne0 10726 |
. . . . . . . . . . . . . . 15
 |
211 | 210 | a1i 11 |
. . . . . . . . . . . . . 14
         |
212 | 34, 204, 209, 211 | divassd 10440 |
. . . . . . . . . . . . 13
                                 |
213 | 207, 212 | eqtr2d 2506 |
. . . . . . . . . . . 12
                             |
214 | 198, 213 | oveq12d 6326 |
. . . . . . . . . . 11
                                       |
215 | 197, 214 | eqtrd 2505 |
. . . . . . . . . 10
                                   |
216 | 215 | oveq2d 6324 |
. . . . . . . . 9
                                       |
217 | 195, 196,
216 | 3eqtr3d 2513 |
. . . . . . . 8
       
                           |
218 | | sin01bnd 14316 |
. . . . . . . . . . 11
     ![(,] (,]](_ioc.gif)                                |
219 | 72, 218 | syl 17 |
. . . . . . . . . 10
                                     |
220 | 219 | simpld 466 |
. . . . . . . . 9
                           |
221 | | 3nn0 10911 |
. . . . . . . . . . . . 13
 |
222 | | reexpcl 12327 |
. . . . . . . . . . . . 13
   
         |
223 | 6, 221, 222 | sylancl 675 |
. . . . . . . . . . . 12
               |
224 | | nndivre 10667 |
. . . . . . . . . . . 12
       
           |
225 | 223, 8, 224 | sylancl 675 |
. . . . . . . . . . 11
                 |
226 | 6, 225 | resubcld 10068 |
. . . . . . . . . 10
                     |
227 | 6 | resincld 14274 |
. . . . . . . . . 10
               |
228 | | ltmul2 10478 |
. . . . . . . . . 10
                                                                   |
229 | 226, 227,
43, 47, 228 | syl112anc 1296 |
. . . . . . . . 9
                         
                         |
230 | 220, 229 | mpbid 215 |
. . . . . . . 8
                               |
231 | 217, 230 | eqbrtrd 4416 |
. . . . . . 7
       
                     |
232 | | remulcl 9642 |
. . . . . . . . 9
                   |
233 | 14, 227, 232 | sylancr 676 |
. . . . . . . 8
                 |
234 | | ltmul1 10477 |
. . . . . . . 8
                                                                                                 |
235 | 13, 233, 38, 77, 234 | syl112anc 1296 |
. . . . . . 7
                                                                   |
236 | 231, 235 | mpbid 215 |
. . . . . 6
                                             |
237 | 227 | recnd 9687 |
. . . . . . . 8
               |
238 | 38 | recnd 9687 |
. . . . . . . 8
               |
239 | 29, 237, 238 | mulassd 9684 |
. . . . . . 7
                                         |
240 | | sin2t 14308 |
. . . . . . . 8
                             |
241 | 34, 240 | syl 17 |
. . . . . . 7
                                 |
242 | 32 | fveq2d 5883 |
. . . . . . 7
                     |
243 | 239, 241,
242 | 3eqtr2rd 2512 |
. . . . . 6
                             |
244 | 236, 243 | breqtrrd 4422 |
. . . . 5
                                 |
245 | 19, 189, 20, 194, 244 | lttrd 9813 |
. . . 4
                                       |
246 | 3, 19, 20, 188, 245 | lttrd 9813 |
. . 3
       
           |
247 | | sincosq1sgn 23532 |
. . . . 5
       
           |
248 | 247 | simprd 470 |
. . . 4
             |
249 | | ltmuldiv 10500 |
. . . 4
                           
             |
250 | 1, 20, 2, 248, 249 | syl112anc 1296 |
. . 3
                 
             |
251 | 246, 250 | mpbid 215 |
. 2
                   |
252 | 248 | gt0ne0d 10199 |
. . 3
             |
253 | | tanval 14259 |
. . 3
                       |
254 | 27, 252, 253 | syl2anc 673 |
. 2
                       |
255 | 251, 254 | breqtrrd 4422 |
1
             |