Proof of Theorem tanregt0
Step | Hyp | Ref
| Expression |
1 | | ax-1cn 9994 |
. . . . . . 7
|
2 | | recl 13850 |
. . . . . . . . . . 11
|
3 | 2 | adantr 481 |
. . . . . . . . . 10
|
4 | 3 | recnd 10068 |
. . . . . . . . 9
|
5 | 3 | rered 13964 |
. . . . . . . . . . 11
|
6 | | neghalfpire 24217 |
. . . . . . . . . . . . . 14
|
7 | 6 | rexri 10097 |
. . . . . . . . . . . . 13
|
8 | | 0re 10040 |
. . . . . . . . . . . . . 14
|
9 | | pirp 24213 |
. . . . . . . . . . . . . . . 16
|
10 | | rphalfcl 11858 |
. . . . . . . . . . . . . . . 16
|
11 | | rpgt0 11844 |
. . . . . . . . . . . . . . . 16
|
12 | 9, 10, 11 | mp2b 10 |
. . . . . . . . . . . . . . 15
|
13 | | halfpire 24216 |
. . . . . . . . . . . . . . . 16
|
14 | | lt0neg2 10535 |
. . . . . . . . . . . . . . . 16
|
15 | 13, 14 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
16 | 12, 15 | mpbi 220 |
. . . . . . . . . . . . . 14
|
17 | 6, 8, 16 | ltleii 10160 |
. . . . . . . . . . . . 13
|
18 | | iooss1 12210 |
. . . . . . . . . . . . 13
|
19 | 7, 17, 18 | mp2an 708 |
. . . . . . . . . . . 12
|
20 | | simpr 477 |
. . . . . . . . . . . 12
|
21 | 19, 20 | sseldi 3601 |
. . . . . . . . . . 11
|
22 | 5, 21 | eqeltrd 2701 |
. . . . . . . . . 10
|
23 | | cosne0 24276 |
. . . . . . . . . 10
|
24 | 4, 22, 23 | syl2anc 693 |
. . . . . . . . 9
|
25 | 4, 24 | tancld 14862 |
. . . . . . . 8
|
26 | | ax-icn 9995 |
. . . . . . . . . 10
|
27 | | imcl 13851 |
. . . . . . . . . . . 12
|
28 | 27 | adantr 481 |
. . . . . . . . . . 11
|
29 | 28 | recnd 10068 |
. . . . . . . . . 10
|
30 | | mulcl 10020 |
. . . . . . . . . 10
|
31 | 26, 29, 30 | sylancr 695 |
. . . . . . . . 9
|
32 | | rpcoshcl 14887 |
. . . . . . . . . . 11
|
33 | 28, 32 | syl 17 |
. . . . . . . . . 10
|
34 | 33 | rpne0d 11877 |
. . . . . . . . 9
|
35 | 31, 34 | tancld 14862 |
. . . . . . . 8
|
36 | 25, 35 | mulcld 10060 |
. . . . . . 7
|
37 | | subcl 10280 |
. . . . . . 7
|
38 | 1, 36, 37 | sylancr 695 |
. . . . . 6
|
39 | | replim 13856 |
. . . . . . . . . . . 12
|
40 | 39 | adantr 481 |
. . . . . . . . . . 11
|
41 | 40 | fveq2d 6195 |
. . . . . . . . . 10
|
42 | | cosne0 24276 |
. . . . . . . . . . 11
|
43 | 21, 42 | syldan 487 |
. . . . . . . . . 10
|
44 | 41, 43 | eqnetrrd 2862 |
. . . . . . . . 9
|
45 | | tanaddlem 14896 |
. . . . . . . . . 10
|
46 | 4, 31, 24, 34, 45 | syl22anc 1327 |
. . . . . . . . 9
|
47 | 44, 46 | mpbid 222 |
. . . . . . . 8
|
48 | 47 | necomd 2849 |
. . . . . . 7
|
49 | | subeq0 10307 |
. . . . . . . . 9
|
50 | 49 | necon3bid 2838 |
. . . . . . . 8
|
51 | 1, 36, 50 | sylancr 695 |
. . . . . . 7
|
52 | 48, 51 | mpbird 247 |
. . . . . 6
|
53 | 38, 52 | absrpcld 14187 |
. . . . 5
|
54 | | 2z 11409 |
. . . . 5
|
55 | | rpexpcl 12879 |
. . . . 5
|
56 | 53, 54, 55 | sylancl 694 |
. . . 4
|
57 | 56 | rprecred 11883 |
. . 3
|
58 | 38 | cjcld 13936 |
. . . . 5
|
59 | 25, 35 | addcld 10059 |
. . . . 5
|
60 | 58, 59 | mulcld 10060 |
. . . 4
|
61 | 60 | recld 13934 |
. . 3
|
62 | 56 | rpreccld 11882 |
. . . 4
|
63 | 62 | rpgt0d 11875 |
. . 3
|
64 | 3, 24 | retancld 14875 |
. . . . 5
|
65 | | 1re 10039 |
. . . . . 6
|
66 | | retanhcl 14889 |
. . . . . . . 8
|
67 | 28, 66 | syl 17 |
. . . . . . 7
|
68 | 67 | resqcld 13035 |
. . . . . 6
|
69 | | resubcl 10345 |
. . . . . 6
|
70 | 65, 68, 69 | sylancr 695 |
. . . . 5
|
71 | | tanrpcl 24256 |
. . . . . . 7
|
72 | 71 | adantl 482 |
. . . . . 6
|
73 | 72 | rpgt0d 11875 |
. . . . 5
|
74 | | absresq 14042 |
. . . . . . . 8
|
75 | 67, 74 | syl 17 |
. . . . . . 7
|
76 | | tanhbnd 14891 |
. . . . . . . . . . . 12
|
77 | 28, 76 | syl 17 |
. . . . . . . . . . 11
|
78 | | eliooord 12233 |
. . . . . . . . . . 11
|
79 | 77, 78 | syl 17 |
. . . . . . . . . 10
|
80 | | abslt 14054 |
. . . . . . . . . . 11
|
81 | 67, 65, 80 | sylancl 694 |
. . . . . . . . . 10
|
82 | 79, 81 | mpbird 247 |
. . . . . . . . 9
|
83 | 67 | recnd 10068 |
. . . . . . . . . . 11
|
84 | 83 | abscld 14175 |
. . . . . . . . . 10
|
85 | 65 | a1i 11 |
. . . . . . . . . 10
|
86 | 83 | absge0d 14183 |
. . . . . . . . . 10
|
87 | | 0le1 10551 |
. . . . . . . . . . 11
|
88 | 87 | a1i 11 |
. . . . . . . . . 10
|
89 | 84, 85, 86, 88 | lt2sqd 13043 |
. . . . . . . . 9
|
90 | 82, 89 | mpbid 222 |
. . . . . . . 8
|
91 | | sq1 12958 |
. . . . . . . 8
|
92 | 90, 91 | syl6breq 4694 |
. . . . . . 7
|
93 | 75, 92 | eqbrtrrd 4677 |
. . . . . 6
|
94 | | posdif 10521 |
. . . . . . 7
|
95 | 68, 65, 94 | sylancl 694 |
. . . . . 6
|
96 | 93, 95 | mpbid 222 |
. . . . 5
|
97 | 64, 70, 73, 96 | mulgt0d 10192 |
. . . 4
|
98 | 38 | recjd 13944 |
. . . . . . . . 9
|
99 | | resub 13867 |
. . . . . . . . . 10
|
100 | 1, 36, 99 | sylancr 695 |
. . . . . . . . 9
|
101 | | re1 13894 |
. . . . . . . . . . 11
|
102 | 101 | oveq1i 6660 |
. . . . . . . . . 10
|
103 | 64, 35 | remul2d 13967 |
. . . . . . . . . . . . 13
|
104 | | negicn 10282 |
. . . . . . . . . . . . . . . . . 18
|
105 | 104 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
106 | | ine0 10465 |
. . . . . . . . . . . . . . . . . . 19
|
107 | 26, 106 | negne0i 10356 |
. . . . . . . . . . . . . . . . . 18
|
108 | 107 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
109 | 35, 105, 108 | divcld 10801 |
. . . . . . . . . . . . . . . 16
|
110 | | imre 13848 |
. . . . . . . . . . . . . . . 16
|
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . 15
|
112 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
113 | 106 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
114 | 35, 112, 113 | divneg2d 10815 |
. . . . . . . . . . . . . . . . 17
|
115 | 67 | renegcld 10457 |
. . . . . . . . . . . . . . . . 17
|
116 | 114, 115 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . 16
|
117 | 116 | reim0d 13965 |
. . . . . . . . . . . . . . 15
|
118 | 35, 105, 108 | divcan2d 10803 |
. . . . . . . . . . . . . . . 16
|
119 | 118 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
120 | 111, 117,
119 | 3eqtr3rd 2665 |
. . . . . . . . . . . . . 14
|
121 | 120 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
122 | 25 | mul01d 10235 |
. . . . . . . . . . . . 13
|
123 | 103, 121,
122 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
124 | 123 | oveq2d 6666 |
. . . . . . . . . . 11
|
125 | | 1m0e1 11131 |
. . . . . . . . . . 11
|
126 | 124, 125 | syl6eq 2672 |
. . . . . . . . . 10
|
127 | 102, 126 | syl5eq 2668 |
. . . . . . . . 9
|
128 | 98, 100, 127 | 3eqtrd 2660 |
. . . . . . . 8
|
129 | 35, 112, 113 | divcan2d 10803 |
. . . . . . . . . . 11
|
130 | 129 | oveq2d 6666 |
. . . . . . . . . 10
|
131 | 130 | fveq2d 6195 |
. . . . . . . . 9
|
132 | 64, 67 | crred 13971 |
. . . . . . . . 9
|
133 | 131, 132 | eqtr3d 2658 |
. . . . . . . 8
|
134 | 128, 133 | oveq12d 6668 |
. . . . . . 7
|
135 | | mulcom 10022 |
. . . . . . . 8
|
136 | 1, 25, 135 | sylancr 695 |
. . . . . . 7
|
137 | 134, 136 | eqtrd 2656 |
. . . . . 6
|
138 | 25, 83, 83 | mulassd 10063 |
. . . . . . 7
|
139 | 38 | imcjd 13945 |
. . . . . . . . 9
|
140 | | imsub 13875 |
. . . . . . . . . . . 12
|
141 | 1, 36, 140 | sylancr 695 |
. . . . . . . . . . 11
|
142 | | im1 13895 |
. . . . . . . . . . . . . 14
|
143 | 142 | oveq1i 6660 |
. . . . . . . . . . . . 13
|
144 | | df-neg 10269 |
. . . . . . . . . . . . 13
|
145 | 143, 144 | eqtr4i 2647 |
. . . . . . . . . . . 12
|
146 | 64, 35 | immul2d 13968 |
. . . . . . . . . . . . . 14
|
147 | | imval 13847 |
. . . . . . . . . . . . . . . . 17
|
148 | 35, 147 | syl 17 |
. . . . . . . . . . . . . . . 16
|
149 | 67 | rered 13964 |
. . . . . . . . . . . . . . . 16
|
150 | 148, 149 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
151 | 150 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
152 | 146, 151 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
153 | 152 | negeqd 10275 |
. . . . . . . . . . . 12
|
154 | 145, 153 | syl5eq 2668 |
. . . . . . . . . . 11
|
155 | 141, 154 | eqtrd 2656 |
. . . . . . . . . 10
|
156 | 155 | negeqd 10275 |
. . . . . . . . 9
|
157 | 64, 67 | remulcld 10070 |
. . . . . . . . . . 11
|
158 | 157 | recnd 10068 |
. . . . . . . . . 10
|
159 | 158 | negnegd 10383 |
. . . . . . . . 9
|
160 | 139, 156,
159 | 3eqtrd 2660 |
. . . . . . . 8
|
161 | 130 | fveq2d 6195 |
. . . . . . . . 9
|
162 | 64, 67 | crimd 13972 |
. . . . . . . . 9
|
163 | 161, 162 | eqtr3d 2658 |
. . . . . . . 8
|
164 | 160, 163 | oveq12d 6668 |
. . . . . . 7
|
165 | 83 | sqvald 13005 |
. . . . . . . 8
|
166 | 165 | oveq2d 6666 |
. . . . . . 7
|
167 | 138, 164,
166 | 3eqtr4d 2666 |
. . . . . 6
|
168 | 137, 167 | oveq12d 6668 |
. . . . 5
|
169 | 58, 59 | remuld 13958 |
. . . . 5
|
170 | 1 | a1i 11 |
. . . . . 6
|
171 | 83 | sqcld 13006 |
. . . . . 6
|
172 | 25, 170, 171 | subdid 10486 |
. . . . 5
|
173 | 168, 169,
172 | 3eqtr4d 2666 |
. . . 4
|
174 | 97, 173 | breqtrrd 4681 |
. . 3
|
175 | 57, 61, 63, 174 | mulgt0d 10192 |
. 2
|
176 | 40 | fveq2d 6195 |
. . . . . 6
|
177 | | tanadd 14897 |
. . . . . . 7
|
178 | 4, 31, 24, 34, 44, 177 | syl23anc 1333 |
. . . . . 6
|
179 | | recval 14062 |
. . . . . . . . 9
|
180 | 38, 52, 179 | syl2anc 693 |
. . . . . . . 8
|
181 | 180 | oveq1d 6665 |
. . . . . . 7
|
182 | 59, 38, 52 | divrec2d 10805 |
. . . . . . 7
|
183 | 38 | abscld 14175 |
. . . . . . . . . 10
|
184 | 183 | resqcld 13035 |
. . . . . . . . 9
|
185 | 184 | recnd 10068 |
. . . . . . . 8
|
186 | 56 | rpne0d 11877 |
. . . . . . . 8
|
187 | 58, 59, 185, 186 | div23d 10838 |
. . . . . . 7
|
188 | 181, 182,
187 | 3eqtr4d 2666 |
. . . . . 6
|
189 | 176, 178,
188 | 3eqtrd 2660 |
. . . . 5
|
190 | 60, 185, 186 | divrec2d 10805 |
. . . . 5
|
191 | 189, 190 | eqtrd 2656 |
. . . 4
|
192 | 191 | fveq2d 6195 |
. . 3
|
193 | 57, 60 | remul2d 13967 |
. . 3
|
194 | 192, 193 | eqtrd 2656 |
. 2
|
195 | 175, 194 | breqtrrd 4681 |
1
|