Step | Hyp | Ref
| Expression |
1 | | uzssz 11707 |
. . . . . 6
|
2 | | zssre 11384 |
. . . . . 6
|
3 | 1, 2 | sstri 3612 |
. . . . 5
|
4 | 3 | a1i 11 |
. . . 4
|
5 | | ioodvbdlimc2lem.m |
. . . . . . 7
|
6 | | ioodvbdlimc2lem.b |
. . . . . . . . . . 11
|
7 | | ioodvbdlimc2lem.a |
. . . . . . . . . . 11
|
8 | 6, 7 | resubcld 10458 |
. . . . . . . . . 10
|
9 | | ioodvbdlimc2lem.altb |
. . . . . . . . . . . 12
|
10 | 7, 6 | posdifd 10614 |
. . . . . . . . . . . 12
|
11 | 9, 10 | mpbid 222 |
. . . . . . . . . . 11
|
12 | 11 | gt0ne0d 10592 |
. . . . . . . . . 10
|
13 | 8, 12 | rereccld 10852 |
. . . . . . . . 9
|
14 | | 0red 10041 |
. . . . . . . . . 10
|
15 | 8, 11 | recgt0d 10958 |
. . . . . . . . . 10
|
16 | 14, 13, 15 | ltled 10185 |
. . . . . . . . 9
|
17 | | flge0nn0 12621 |
. . . . . . . . 9
|
18 | 13, 16, 17 | syl2anc 693 |
. . . . . . . 8
|
19 | | peano2nn0 11333 |
. . . . . . . 8
|
20 | 18, 19 | syl 17 |
. . . . . . 7
|
21 | 5, 20 | syl5eqel 2705 |
. . . . . 6
|
22 | 21 | nn0zd 11480 |
. . . . 5
|
23 | | eqid 2622 |
. . . . . 6
|
24 | 23 | uzsup 12662 |
. . . . 5
|
25 | 22, 24 | syl 17 |
. . . 4
|
26 | | ioodvbdlimc2lem.f |
. . . . . . 7
|
27 | 26 | adantr 481 |
. . . . . 6
|
28 | 7 | rexrd 10089 |
. . . . . . . 8
|
29 | 28 | adantr 481 |
. . . . . . 7
|
30 | 6 | rexrd 10089 |
. . . . . . . 8
|
31 | 30 | adantr 481 |
. . . . . . 7
|
32 | 6 | adantr 481 |
. . . . . . . 8
|
33 | | eluzelre 11698 |
. . . . . . . . . 10
|
34 | 33 | adantl 482 |
. . . . . . . . 9
|
35 | | 0red 10041 |
. . . . . . . . . . 11
|
36 | | 0red 10041 |
. . . . . . . . . . . . 13
|
37 | | 1red 10055 |
. . . . . . . . . . . . 13
|
38 | 36, 37 | readdcld 10069 |
. . . . . . . . . . . 12
|
39 | 38 | adantl 482 |
. . . . . . . . . . 11
|
40 | 36 | ltp1d 10954 |
. . . . . . . . . . . 12
|
41 | 40 | adantl 482 |
. . . . . . . . . . 11
|
42 | | eluzel2 11692 |
. . . . . . . . . . . . . 14
|
43 | 42 | zred 11482 |
. . . . . . . . . . . . 13
|
44 | 43 | adantl 482 |
. . . . . . . . . . . 12
|
45 | 13 | flcld 12599 |
. . . . . . . . . . . . . . . 16
|
46 | 45 | zred 11482 |
. . . . . . . . . . . . . . 15
|
47 | | 1red 10055 |
. . . . . . . . . . . . . . 15
|
48 | 18 | nn0ge0d 11354 |
. . . . . . . . . . . . . . 15
|
49 | 14, 46, 47, 48 | leadd1dd 10641 |
. . . . . . . . . . . . . 14
|
50 | 49, 5 | syl6breqr 4695 |
. . . . . . . . . . . . 13
|
51 | 50 | adantr 481 |
. . . . . . . . . . . 12
|
52 | | eluzle 11700 |
. . . . . . . . . . . . 13
|
53 | 52 | adantl 482 |
. . . . . . . . . . . 12
|
54 | 39, 44, 34, 51, 53 | letrd 10194 |
. . . . . . . . . . 11
|
55 | 35, 39, 34, 41, 54 | ltletrd 10197 |
. . . . . . . . . 10
|
56 | 55 | gt0ne0d 10592 |
. . . . . . . . 9
|
57 | 34, 56 | rereccld 10852 |
. . . . . . . 8
|
58 | 32, 57 | resubcld 10458 |
. . . . . . 7
|
59 | 7 | adantr 481 |
. . . . . . . 8
|
60 | 21 | nn0red 11352 |
. . . . . . . . . . 11
|
61 | 14, 47 | readdcld 10069 |
. . . . . . . . . . . . . 14
|
62 | 46, 47 | readdcld 10069 |
. . . . . . . . . . . . . 14
|
63 | 14 | ltp1d 10954 |
. . . . . . . . . . . . . 14
|
64 | 14, 61, 62, 63, 49 | ltletrd 10197 |
. . . . . . . . . . . . 13
|
65 | 64, 5 | syl6breqr 4695 |
. . . . . . . . . . . 12
|
66 | 65 | gt0ne0d 10592 |
. . . . . . . . . . 11
|
67 | 60, 66 | rereccld 10852 |
. . . . . . . . . 10
|
68 | 67 | adantr 481 |
. . . . . . . . 9
|
69 | 32, 68 | resubcld 10458 |
. . . . . . . 8
|
70 | 5 | eqcomi 2631 |
. . . . . . . . . . . . 13
|
71 | 70 | oveq2i 6661 |
. . . . . . . . . . . 12
|
72 | 71, 67 | syl5eqel 2705 |
. . . . . . . . . . 11
|
73 | 13, 15 | elrpd 11869 |
. . . . . . . . . . . . 13
|
74 | 62, 64 | elrpd 11869 |
. . . . . . . . . . . . 13
|
75 | | 1rp 11836 |
. . . . . . . . . . . . . 14
|
76 | 75 | a1i 11 |
. . . . . . . . . . . . 13
|
77 | | fllelt 12598 |
. . . . . . . . . . . . . . 15
|
78 | 13, 77 | syl 17 |
. . . . . . . . . . . . . 14
|
79 | 78 | simprd 479 |
. . . . . . . . . . . . 13
|
80 | 73, 74, 76, 79 | ltdiv2dd 39507 |
. . . . . . . . . . . 12
|
81 | 8 | recnd 10068 |
. . . . . . . . . . . . 13
|
82 | 81, 12 | recrecd 10798 |
. . . . . . . . . . . 12
|
83 | 80, 82 | breqtrd 4679 |
. . . . . . . . . . 11
|
84 | 72, 8, 6, 83 | ltsub2dd 10640 |
. . . . . . . . . 10
|
85 | 6 | recnd 10068 |
. . . . . . . . . . 11
|
86 | 7 | recnd 10068 |
. . . . . . . . . . 11
|
87 | 85, 86 | nncand 10397 |
. . . . . . . . . 10
|
88 | 71 | oveq2i 6661 |
. . . . . . . . . . 11
|
89 | 88 | a1i 11 |
. . . . . . . . . 10
|
90 | 84, 87, 89 | 3brtr3d 4684 |
. . . . . . . . 9
|
91 | 90 | adantr 481 |
. . . . . . . 8
|
92 | 60, 65 | elrpd 11869 |
. . . . . . . . . . 11
|
93 | 92 | adantr 481 |
. . . . . . . . . 10
|
94 | 34, 55 | elrpd 11869 |
. . . . . . . . . 10
|
95 | | 1red 10055 |
. . . . . . . . . 10
|
96 | | 0le1 10551 |
. . . . . . . . . . 11
|
97 | 96 | a1i 11 |
. . . . . . . . . 10
|
98 | 93, 94, 95, 97, 53 | lediv2ad 11894 |
. . . . . . . . 9
|
99 | 57, 68, 32, 98 | lesub2dd 10644 |
. . . . . . . 8
|
100 | 59, 69, 58, 91, 99 | ltletrd 10197 |
. . . . . . 7
|
101 | 94 | rpreccld 11882 |
. . . . . . . 8
|
102 | 32, 101 | ltsubrpd 11904 |
. . . . . . 7
|
103 | 29, 31, 58, 100, 102 | eliood 39720 |
. . . . . 6
|
104 | 27, 103 | ffvelrnd 6360 |
. . . . 5
|
105 | | ioodvbdlimc2lem.s |
. . . . 5
|
106 | 104, 105 | fmptd 6385 |
. . . 4
|
107 | | ioodvbdlimc2lem.dmdv |
. . . . . 6
|
108 | | ioodvbdlimc2lem.dvbd |
. . . . . 6
|
109 | 7, 6, 9, 26, 107, 108 | dvbdfbdioo 40145 |
. . . . 5
|
110 | 60 | adantr 481 |
. . . . . . . 8
|
111 | | simpr 477 |
. . . . . . . . . . . . . 14
|
112 | 105 | fvmpt2 6291 |
. . . . . . . . . . . . . 14
|
113 | 111, 104,
112 | syl2anc 693 |
. . . . . . . . . . . . 13
|
114 | 113 | fveq2d 6195 |
. . . . . . . . . . . 12
|
115 | 114 | adantlr 751 |
. . . . . . . . . . 11
|
116 | | simplr 792 |
. . . . . . . . . . . 12
|
117 | 103 | adantlr 751 |
. . . . . . . . . . . 12
|
118 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
119 | 118 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
120 | 119 | breq1d 4663 |
. . . . . . . . . . . . 13
|
121 | 120 | rspccva 3308 |
. . . . . . . . . . . 12
|
122 | 116, 117,
121 | syl2anc 693 |
. . . . . . . . . . 11
|
123 | 115, 122 | eqbrtrd 4675 |
. . . . . . . . . 10
|
124 | 123 | a1d 25 |
. . . . . . . . 9
|
125 | 124 | ralrimiva 2966 |
. . . . . . . 8
|
126 | | breq1 4656 |
. . . . . . . . . . 11
|
127 | 126 | imbi1d 331 |
. . . . . . . . . 10
|
128 | 127 | ralbidv 2986 |
. . . . . . . . 9
|
129 | 128 | rspcev 3309 |
. . . . . . . 8
|
130 | 110, 125,
129 | syl2anc 693 |
. . . . . . 7
|
131 | 130 | ex 450 |
. . . . . 6
|
132 | 131 | reximdv 3016 |
. . . . 5
|
133 | 109, 132 | mpd 15 |
. . . 4
|
134 | 4, 25, 106, 133 | limsupre 39873 |
. . 3
|
135 | 134 | recnd 10068 |
. 2
|
136 | | eluzelre 11698 |
. . . . . . . . 9
|
137 | 136 | adantl 482 |
. . . . . . . 8
|
138 | | 0red 10041 |
. . . . . . . . . 10
|
139 | 45 | peano2zd 11485 |
. . . . . . . . . . . . . 14
|
140 | 5, 139 | syl5eqel 2705 |
. . . . . . . . . . . . 13
|
141 | 140 | adantr 481 |
. . . . . . . . . . . 12
|
142 | 141 | zred 11482 |
. . . . . . . . . . 11
|
143 | 142 | adantr 481 |
. . . . . . . . . 10
|
144 | 65 | ad2antrr 762 |
. . . . . . . . . 10
|
145 | | ioodvbdlimc2lem.n |
. . . . . . . . . . . . . 14
|
146 | | ioodvbdlimc2lem.y |
. . . . . . . . . . . . . . . . . . . 20
|
147 | | ioomidp 39740 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
148 | 7, 6, 9, 147 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
149 | | ne0i 3921 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
150 | 148, 149 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
151 | | ioossre 12235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
152 | 151 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
153 | | dvfre 23714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
154 | 26, 152, 153 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
155 | 107 | feq2d 6031 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
156 | 154, 155 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
157 | 156 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
158 | 157 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
159 | 158 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . . 22
|
160 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
|
161 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
|
162 | 150, 159,
108, 160, 161 | suprnmpt 39355 |
. . . . . . . . . . . . . . . . . . . . 21
|
163 | 162 | simpld 475 |
. . . . . . . . . . . . . . . . . . . 20
|
164 | 146, 163 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . . 19
|
165 | 164 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
166 | | rpre 11839 |
. . . . . . . . . . . . . . . . . . . 20
|
167 | 166 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . . . 19
|
168 | 167 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
169 | 166 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
|
170 | 169 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
171 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . 19
|
172 | | rpne0 11848 |
. . . . . . . . . . . . . . . . . . . 20
|
173 | 172 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
174 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . . . . 20
|
175 | 174 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
176 | 170, 171,
173, 175 | divne0d 10817 |
. . . . . . . . . . . . . . . . . 18
|
177 | 165, 168,
176 | redivcld 10853 |
. . . . . . . . . . . . . . . . 17
|
178 | 177 | flcld 12599 |
. . . . . . . . . . . . . . . 16
|
179 | 178 | peano2zd 11485 |
. . . . . . . . . . . . . . 15
|
180 | 179, 141 | ifcld 4131 |
. . . . . . . . . . . . . 14
|
181 | 145, 180 | syl5eqel 2705 |
. . . . . . . . . . . . 13
|
182 | 181 | zred 11482 |
. . . . . . . . . . . 12
|
183 | 182 | adantr 481 |
. . . . . . . . . . 11
|
184 | 179 | zred 11482 |
. . . . . . . . . . . . . 14
|
185 | | max1 12016 |
. . . . . . . . . . . . . 14
|
186 | 142, 184,
185 | syl2anc 693 |
. . . . . . . . . . . . 13
|
187 | 186, 145 | syl6breqr 4695 |
. . . . . . . . . . . 12
|
188 | 187 | adantr 481 |
. . . . . . . . . . 11
|
189 | | eluzle 11700 |
. . . . . . . . . . . 12
|
190 | 189 | adantl 482 |
. . . . . . . . . . 11
|
191 | 143, 183,
137, 188, 190 | letrd 10194 |
. . . . . . . . . 10
|
192 | 138, 143,
137, 144, 191 | ltletrd 10197 |
. . . . . . . . 9
|
193 | 192 | gt0ne0d 10592 |
. . . . . . . 8
|
194 | 137, 193 | rereccld 10852 |
. . . . . . 7
|
195 | 137, 192 | recgt0d 10958 |
. . . . . . 7
|
196 | 194, 195 | elrpd 11869 |
. . . . . 6
|
197 | 196 | adantr 481 |
. . . . 5
|
198 | | ioodvbdlimc2lem.ch |
. . . . . . . . 9
|
199 | 198 | biimpi 206 |
. . . . . . . . . . . . . . . . 17
|
200 | | simp-5l 808 |
. . . . . . . . . . . . . . . . 17
|
201 | 199, 200 | syl 17 |
. . . . . . . . . . . . . . . 16
|
202 | 201, 26 | syl 17 |
. . . . . . . . . . . . . . 15
|
203 | 199 | simplrd 793 |
. . . . . . . . . . . . . . 15
|
204 | 202, 203 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
|
205 | 204 | recnd 10068 |
. . . . . . . . . . . . 13
|
206 | 201, 106 | syl 17 |
. . . . . . . . . . . . . . 15
|
207 | | simp-5r 809 |
. . . . . . . . . . . . . . . . . . 19
|
208 | 199, 207 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
209 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . 19
|
210 | 141, 181,
187, 209 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . 18
|
211 | 201, 208,
210 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
212 | | uzss 11708 |
. . . . . . . . . . . . . . . . 17
|
213 | 211, 212 | syl 17 |
. . . . . . . . . . . . . . . 16
|
214 | | simp-4r 807 |
. . . . . . . . . . . . . . . . 17
|
215 | 199, 214 | syl 17 |
. . . . . . . . . . . . . . . 16
|
216 | 213, 215 | sseldd 3604 |
. . . . . . . . . . . . . . 15
|
217 | 206, 216 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
|
218 | 217 | recnd 10068 |
. . . . . . . . . . . . 13
|
219 | 201, 135 | syl 17 |
. . . . . . . . . . . . 13
|
220 | 205, 218,
219 | npncand 10416 |
. . . . . . . . . . . 12
|
221 | 220 | eqcomd 2628 |
. . . . . . . . . . 11
|
222 | 221 | fveq2d 6195 |
. . . . . . . . . 10
|
223 | 204, 217 | resubcld 10458 |
. . . . . . . . . . . . . 14
|
224 | 201, 134 | syl 17 |
. . . . . . . . . . . . . . 15
|
225 | 217, 224 | resubcld 10458 |
. . . . . . . . . . . . . 14
|
226 | 223, 225 | readdcld 10069 |
. . . . . . . . . . . . 13
|
227 | 226 | recnd 10068 |
. . . . . . . . . . . 12
|
228 | 227 | abscld 14175 |
. . . . . . . . . . 11
|
229 | 223 | recnd 10068 |
. . . . . . . . . . . . 13
|
230 | 229 | abscld 14175 |
. . . . . . . . . . . 12
|
231 | 225 | recnd 10068 |
. . . . . . . . . . . . 13
|
232 | 231 | abscld 14175 |
. . . . . . . . . . . 12
|
233 | 230, 232 | readdcld 10069 |
. . . . . . . . . . 11
|
234 | 208 | rpred 11872 |
. . . . . . . . . . 11
|
235 | 229, 231 | abstrid 14195 |
. . . . . . . . . . 11
|
236 | 234 | rehalfcld 11279 |
. . . . . . . . . . . . 13
|
237 | 201, 216,
113 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
238 | 237 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
239 | 238 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
240 | 239, 230 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
|
241 | 201, 164 | syl 17 |
. . . . . . . . . . . . . . . 16
|
242 | 151, 203 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
|
243 | 201, 216,
58 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
244 | 242, 243 | resubcld 10458 |
. . . . . . . . . . . . . . . 16
|
245 | 241, 244 | remulcld 10070 |
. . . . . . . . . . . . . . 15
|
246 | 201, 7 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
247 | 201, 6 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
248 | 201, 107 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
249 | 162 | simprd 479 |
. . . . . . . . . . . . . . . . . . . 20
|
250 | 146 | breq2i 4661 |
. . . . . . . . . . . . . . . . . . . . 21
|
251 | 250 | ralbii 2980 |
. . . . . . . . . . . . . . . . . . . 20
|
252 | 249, 251 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
|
253 | 201, 252 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
254 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
|
255 | 254 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
256 | 255 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . 19
|
257 | 256 | cbvralv 3171 |
. . . . . . . . . . . . . . . . . 18
|
258 | 253, 257 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
|
259 | 201, 216,
103 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
260 | 243 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
|
261 | 201, 30 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
262 | 3, 216 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . 20
|
263 | 201, 216,
56 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
|
264 | 262, 263 | rereccld 10852 |
. . . . . . . . . . . . . . . . . . 19
|
265 | 247, 242 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . . 20
|
266 | 242, 247 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . . . . 22
|
267 | 266 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . 21
|
268 | 267 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . 20
|
269 | 265 | leabsd 14153 |
. . . . . . . . . . . . . . . . . . . . 21
|
270 | 201, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
271 | 242 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . 22
|
272 | 270, 271 | abssubd 14192 |
. . . . . . . . . . . . . . . . . . . . 21
|
273 | 269, 272 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . 20
|
274 | 199 | simprd 479 |
. . . . . . . . . . . . . . . . . . . 20
|
275 | 265, 268,
264, 273, 274 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . 19
|
276 | 247, 242,
264, 275 | ltsub23d 10632 |
. . . . . . . . . . . . . . . . . 18
|
277 | 201, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
278 | | iooltub 39735 |
. . . . . . . . . . . . . . . . . . 19
|
279 | 277, 261,
203, 278 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
|
280 | 260, 261,
242, 276, 279 | eliood 39720 |
. . . . . . . . . . . . . . . . 17
|
281 | 246, 247,
202, 248, 241, 258, 259, 280 | dvbdfbdioolem1 40143 |
. . . . . . . . . . . . . . . 16
|
282 | 281 | simpld 475 |
. . . . . . . . . . . . . . 15
|
283 | 201, 216,
57 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
284 | 241, 283 | remulcld 10070 |
. . . . . . . . . . . . . . . 16
|
285 | 156, 148 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . 21
|
286 | 285 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
|
287 | 286 | abscld 14175 |
. . . . . . . . . . . . . . . . . . 19
|
288 | 286 | absge0d 14183 |
. . . . . . . . . . . . . . . . . . 19
|
289 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
290 | 289 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
|
291 | 146 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
292 | 291 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
|
293 | 290, 292 | breq12d 4666 |
. . . . . . . . . . . . . . . . . . . . 21
|
294 | 293 | rspcva 3307 |
. . . . . . . . . . . . . . . . . . . 20
|
295 | 148, 249,
294 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
296 | 14, 287, 164, 288, 295 | letrd 10194 |
. . . . . . . . . . . . . . . . . 18
|
297 | 201, 296 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
298 | 283 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
|
299 | | sub31 39503 |
. . . . . . . . . . . . . . . . . . . 20
|
300 | 271, 270,
298, 299 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
|
301 | 242, 247 | posdifd 10614 |
. . . . . . . . . . . . . . . . . . . . . 22
|
302 | 279, 301 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . 21
|
303 | 265, 302 | elrpd 11869 |
. . . . . . . . . . . . . . . . . . . 20
|
304 | 283, 303 | ltsubrpd 11904 |
. . . . . . . . . . . . . . . . . . 19
|
305 | 300, 304 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . 18
|
306 | 244, 283,
305 | ltled 10185 |
. . . . . . . . . . . . . . . . 17
|
307 | 244, 283,
241, 297, 306 | lemul2ad 10964 |
. . . . . . . . . . . . . . . 16
|
308 | 284 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
309 | 236 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
310 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . 20
|
311 | 298 | mul02d 10234 |
. . . . . . . . . . . . . . . . . . . 20
|
312 | 310, 311 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . . 19
|
313 | 208 | rphalfcld 11884 |
. . . . . . . . . . . . . . . . . . . . 21
|
314 | 313 | rpgt0d 11875 |
. . . . . . . . . . . . . . . . . . . 20
|
315 | 314 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
316 | 312, 315 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . 18
|
317 | 308, 309,
316 | ltled 10185 |
. . . . . . . . . . . . . . . . 17
|
318 | 241 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
319 | 297 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
320 | | neqne 2802 |
. . . . . . . . . . . . . . . . . . . 20
|
321 | 320 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
322 | 318, 319,
321 | ne0gt0d 10174 |
. . . . . . . . . . . . . . . . . 18
|
323 | 284 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
324 | 3, 211 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . 22
|
325 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
326 | 201, 208,
142 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
327 | 201, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
328 | 201, 208,
187 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
329 | 325, 326,
324, 327, 328 | ltletrd 10197 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
330 | 329 | gt0ne0d 10592 |
. . . . . . . . . . . . . . . . . . . . . 22
|
331 | 324, 330 | rereccld 10852 |
. . . . . . . . . . . . . . . . . . . . 21
|
332 | 241, 331 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . 20
|
333 | 332 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
334 | 236 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
335 | 283 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
336 | 331 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
337 | 241 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
338 | 297 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
339 | 324, 329 | elrpd 11869 |
. . . . . . . . . . . . . . . . . . . . . 22
|
340 | 201, 216,
94 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
|
341 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . . 22
|
342 | 96 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
|
343 | 215, 189 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
344 | 339, 340,
341, 342, 343 | lediv2ad 11894 |
. . . . . . . . . . . . . . . . . . . . 21
|
345 | 344 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
346 | 335, 336,
337, 338, 345 | lemul2ad 10964 |
. . . . . . . . . . . . . . . . . . 19
|
347 | 234 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
348 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
349 | 208 | rpne0d 11877 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
350 | 174 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
351 | 347, 348,
349, 350 | divne0d 10817 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
352 | 241, 236,
351 | redivcld 10853 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
353 | 352 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
354 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
355 | 314 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
356 | 337, 334,
354, 355 | divgt0d 10959 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
357 | 353, 356 | elrpd 11869 |
. . . . . . . . . . . . . . . . . . . . . 22
|
358 | 357 | rprecred 11883 |
. . . . . . . . . . . . . . . . . . . . 21
|
359 | 339 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
360 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . . 22
|
361 | 96 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
|
362 | 352 | flcld 12599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
363 | 362 | peano2zd 11485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
364 | 363 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
365 | 201, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
366 | 363, 365 | ifcld 4131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
367 | 145, 366 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
368 | 367 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
369 | | flltp1 12601 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
370 | 352, 369 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
371 | 201, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
372 | | max2 12018 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
373 | 371, 364,
372 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
374 | 373, 145 | syl6breqr 4695 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
375 | 352, 364,
368, 370, 374 | ltletrd 10197 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
376 | 352, 324,
375 | ltled 10185 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
377 | 376 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
378 | 357, 359,
360, 361, 377 | lediv2ad 11894 |
. . . . . . . . . . . . . . . . . . . . 21
|
379 | 336, 358,
337, 338, 378 | lemul2ad 10964 |
. . . . . . . . . . . . . . . . . . . 20
|
380 | 337 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . 22
|
381 | 353 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . 22
|
382 | 356 | gt0ne0d 10592 |
. . . . . . . . . . . . . . . . . . . . . 22
|
383 | 380, 381,
382 | divrecd 10804 |
. . . . . . . . . . . . . . . . . . . . 21
|
384 | 334 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . 22
|
385 | 354 | gt0ne0d 10592 |
. . . . . . . . . . . . . . . . . . . . . 22
|
386 | 351 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
387 | 380, 384,
385, 386 | ddcand 10821 |
. . . . . . . . . . . . . . . . . . . . 21
|
388 | 383, 387 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . 20
|
389 | 379, 388 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . 19
|
390 | 323, 333,
334, 346, 389 | letrd 10194 |
. . . . . . . . . . . . . . . . . 18
|
391 | 322, 390 | syldan 487 |
. . . . . . . . . . . . . . . . 17
|
392 | 317, 391 | pm2.61dan 832 |
. . . . . . . . . . . . . . . 16
|
393 | 245, 284,
236, 307, 392 | letrd 10194 |
. . . . . . . . . . . . . . 15
|
394 | 240, 245,
236, 282, 393 | letrd 10194 |
. . . . . . . . . . . . . 14
|
395 | 239, 394 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
|
396 | | simpllr 799 |
. . . . . . . . . . . . . 14
|
397 | 199, 396 | syl 17 |
. . . . . . . . . . . . 13
|
398 | 230, 232,
236, 236, 395, 397 | leltaddd 10649 |
. . . . . . . . . . . 12
|
399 | 347 | 2halvesd 11278 |
. . . . . . . . . . . 12
|
400 | 398, 399 | breqtrd 4679 |
. . . . . . . . . . 11
|
401 | 228, 233,
234, 235, 400 | lelttrd 10195 |
. . . . . . . . . 10
|
402 | 222, 401 | eqbrtrd 4675 |
. . . . . . . . 9
|
403 | 198, 402 | sylbir 225 |
. . . . . . . 8
|
404 | 403 | adantrl 752 |
. . . . . . 7
|
405 | 404 | ex 450 |
. . . . . 6
|
406 | 405 | ralrimiva 2966 |
. . . . 5
|
407 | | breq2 4657 |
. . . . . . . . 9
|
408 | 407 | anbi2d 740 |
. . . . . . . 8
|
409 | 408 | imbi1d 331 |
. . . . . . 7
|
410 | 409 | ralbidv 2986 |
. . . . . 6
|
411 | 410 | rspcev 3309 |
. . . . 5
|
412 | 197, 406,
411 | syl2anc 693 |
. . . 4
|
413 | | simpr 477 |
. . . . . . . . . . 11
|
414 | 413 | iftrued 4094 |
. . . . . . . . . 10
|
415 | | uzid 11702 |
. . . . . . . . . . . 12
|
416 | 181, 415 | syl 17 |
. . . . . . . . . . 11
|
417 | 416 | adantr 481 |
. . . . . . . . . 10
|
418 | 414, 417 | eqeltrd 2701 |
. . . . . . . . 9
|
419 | 418 | adantlr 751 |
. . . . . . . 8
|
420 | | iffalse 4095 |
. . . . . . . . . 10
|
421 | 420 | adantl 482 |
. . . . . . . . 9
|
422 | 181 | ad2antrr 762 |
. . . . . . . . . 10
|
423 | | simplr 792 |
. . . . . . . . . 10
|
424 | 422 | zred 11482 |
. . . . . . . . . . 11
|
425 | 423 | zred 11482 |
. . . . . . . . . . 11
|
426 | | simpr 477 |
. . . . . . . . . . . 12
|
427 | 424, 425 | ltnled 10184 |
. . . . . . . . . . . 12
|
428 | 426, 427 | mpbird 247 |
. . . . . . . . . . 11
|
429 | 424, 425,
428 | ltled 10185 |
. . . . . . . . . 10
|
430 | | eluz2 11693 |
. . . . . . . . . 10
|
431 | 422, 423,
429, 430 | syl3anbrc 1246 |
. . . . . . . . 9
|
432 | 421, 431 | eqeltrd 2701 |
. . . . . . . 8
|
433 | 419, 432 | pm2.61dan 832 |
. . . . . . 7
|
434 | 433 | adantr 481 |
. . . . . 6
|
435 | | simpr 477 |
. . . . . . . 8
|
436 | | simpr 477 |
. . . . . . . . . 10
|
437 | 181 | adantr 481 |
. . . . . . . . . . 11
|
438 | 437, 436 | ifcld 4131 |
. . . . . . . . . 10
|
439 | 436 | zred 11482 |
. . . . . . . . . . 11
|
440 | 437 | zred 11482 |
. . . . . . . . . . 11
|
441 | | max1 12016 |
. . . . . . . . . . 11
|
442 | 439, 440,
441 | syl2anc 693 |
. . . . . . . . . 10
|
443 | | eluz2 11693 |
. . . . . . . . . 10
|
444 | 436, 438,
442, 443 | syl3anbrc 1246 |
. . . . . . . . 9
|
445 | 444 | adantr 481 |
. . . . . . . 8
|
446 | | fveq2 6191 |
. . . . . . . . . . 11
|
447 | 446 | eleq1d 2686 |
. . . . . . . . . 10
|
448 | 446 | oveq1d 6665 |
. . . . . . . . . . . 12
|
449 | 448 | fveq2d 6195 |
. . . . . . . . . . 11
|
450 | 449 | breq1d 4663 |
. . . . . . . . . 10
|
451 | 447, 450 | anbi12d 747 |
. . . . . . . . 9
|
452 | 451 | rspccva 3308 |
. . . . . . . 8
|
453 | 435, 445,
452 | syl2anc 693 |
. . . . . . 7
|
454 | 453 | simprd 479 |
. . . . . 6
|
455 | | fveq2 6191 |
. . . . . . . . . 10
|
456 | 455 | oveq1d 6665 |
. . . . . . . . 9
|
457 | 456 | fveq2d 6195 |
. . . . . . . 8
|
458 | 457 | breq1d 4663 |
. . . . . . 7
|
459 | 458 | rspcev 3309 |
. . . . . 6
|
460 | 434, 454,
459 | syl2anc 693 |
. . . . 5
|
461 | | ax-resscn 9993 |
. . . . . . . . . . . . . 14
|
462 | 461 | a1i 11 |
. . . . . . . . . . . . 13
|
463 | 26, 462 | fssd 6057 |
. . . . . . . . . . . . . 14
|
464 | | dvcn 23684 |
. . . . . . . . . . . . . 14
|
465 | 462, 463,
152, 107, 464 | syl31anc 1329 |
. . . . . . . . . . . . 13
|
466 | | cncffvrn 22701 |
. . . . . . . . . . . . 13
|
467 | 462, 465,
466 | syl2anc 693 |
. . . . . . . . . . . 12
|
468 | 26, 467 | mpbird 247 |
. . . . . . . . . . 11
|
469 | | ioodvbdlimc2lem.r |
. . . . . . . . . . . 12
|
470 | 103, 469 | fmptd 6385 |
. . . . . . . . . . 11
|
471 | | eqid 2622 |
. . . . . . . . . . 11
|
472 | | climrel 14223 |
. . . . . . . . . . . . 13
|
473 | 472 | a1i 11 |
. . . . . . . . . . . 12
|
474 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
|
475 | 474 | mptex 6486 |
. . . . . . . . . . . . . . . 16
|
476 | 475 | a1i 11 |
. . . . . . . . . . . . . . 15
|
477 | | eqidd 2623 |
. . . . . . . . . . . . . . . 16
|
478 | | eqidd 2623 |
. . . . . . . . . . . . . . . 16
|
479 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
480 | 6 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
481 | 477, 478,
479, 480 | fvmptd 6288 |
. . . . . . . . . . . . . . 15
|
482 | 23, 22, 476, 85, 481 | climconst 14274 |
. . . . . . . . . . . . . 14
|
483 | 474 | mptex 6486 |
. . . . . . . . . . . . . . . 16
|
484 | 469, 483 | eqeltri 2697 |
. . . . . . . . . . . . . . 15
|
485 | 484 | a1i 11 |
. . . . . . . . . . . . . 14
|
486 | | 1cnd 10056 |
. . . . . . . . . . . . . . 15
|
487 | | elnnnn0b 11337 |
. . . . . . . . . . . . . . . 16
|
488 | 21, 65, 487 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
|
489 | | divcnvg 39859 |
. . . . . . . . . . . . . . 15
|
490 | 486, 488,
489 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
491 | | eqidd 2623 |
. . . . . . . . . . . . . . . . 17
|
492 | | eqidd 2623 |
. . . . . . . . . . . . . . . . 17
|
493 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
494 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
495 | 491, 492,
493, 494 | fvmptd 6288 |
. . . . . . . . . . . . . . . 16
|
496 | 495, 494 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
|
497 | 496 | recnd 10068 |
. . . . . . . . . . . . . 14
|
498 | | eqidd 2623 |
. . . . . . . . . . . . . . . 16
|
499 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
500 | 499 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
501 | 3, 493 | sseldi 3601 |
. . . . . . . . . . . . . . . . 17
|
502 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . 19
|
503 | 60 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
504 | 65 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
505 | | eluzle 11700 |
. . . . . . . . . . . . . . . . . . . 20
|
506 | 505 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
507 | 502, 503,
501, 504, 506 | ltletrd 10197 |
. . . . . . . . . . . . . . . . . 18
|
508 | 507 | gt0ne0d 10592 |
. . . . . . . . . . . . . . . . 17
|
509 | 501, 508 | rereccld 10852 |
. . . . . . . . . . . . . . . 16
|
510 | 498, 500,
493, 509 | fvmptd 6288 |
. . . . . . . . . . . . . . 15
|
511 | 501 | recnd 10068 |
. . . . . . . . . . . . . . . 16
|
512 | 511, 508 | reccld 10794 |
. . . . . . . . . . . . . . 15
|
513 | 510, 512 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
|
514 | 499 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
515 | | ovex 6678 |
. . . . . . . . . . . . . . . . 17
|
516 | 514, 469,
515 | fvmpt 6282 |
. . . . . . . . . . . . . . . 16
|
517 | 516 | adantl 482 |
. . . . . . . . . . . . . . 15
|
518 | 495, 510 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
|
519 | 517, 518 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
|
520 | 23, 22, 482, 485, 490, 497, 513, 519 | climsub 14364 |
. . . . . . . . . . . . 13
|
521 | 85 | subid1d 10381 |
. . . . . . . . . . . . 13
|
522 | 520, 521 | breqtrd 4679 |
. . . . . . . . . . . 12
|
523 | | releldm 5358 |
. . . . . . . . . . . 12
|
524 | 473, 522,
523 | syl2anc 693 |
. . . . . . . . . . 11
|
525 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
526 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
527 | 526 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
528 | 527 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
529 | 528 | breq1d 4663 |
. . . . . . . . . . . . . . 15
|
530 | 525, 529 | raleqbidv 3152 |
. . . . . . . . . . . . . 14
|
531 | 530 | cbvrabv 3199 |
. . . . . . . . . . . . 13
|
532 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
|
533 | 532 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
534 | 533 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
535 | 534 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
|
536 | 535 | cbvralv 3171 |
. . . . . . . . . . . . . . 15
|
537 | 536 | rgenw 2924 |
. . . . . . . . . . . . . 14
|
538 | | rabbi 3120 |
. . . . . . . . . . . . . 14
|
539 | 537, 538 | mpbi 220 |
. . . . . . . . . . . . 13
|
540 | 531, 539 | eqtri 2644 |
. . . . . . . . . . . 12
|
541 | 540 | infeq1i 8384 |
. . . . . . . . . . 11
inf
inf
|
542 | 7, 6, 9, 468, 107, 108, 22, 470, 471, 524, 541 | ioodvbdlimc1lem1 40146 |
. . . . . . . . . 10
|
543 | 469 | fvmpt2 6291 |
. . . . . . . . . . . . . . 15
|
544 | 111, 58, 543 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
545 | 544 | eqcomd 2628 |
. . . . . . . . . . . . 13
|
546 | 545 | fveq2d 6195 |
. . . . . . . . . . . 12
|
547 | 546 | mpteq2dva 4744 |
. . . . . . . . . . 11
|
548 | 105, 547 | syl5eq 2668 |
. . . . . . . . . 10
|
549 | 548 | fveq2d 6195 |
. . . . . . . . . 10
|
550 | 542, 548,
549 | 3brtr4d 4685 |
. . . . . . . . 9
|
551 | 474 | mptex 6486 |
. . . . . . . . . . . 12
|
552 | 105, 551 | eqeltri 2697 |
. . . . . . . . . . 11
|
553 | 552 | a1i 11 |
. . . . . . . . . 10
|
554 | | eqidd 2623 |
. . . . . . . . . 10
|
555 | 553, 554 | clim 14225 |
. . . . . . . . 9
|
556 | 550, 555 | mpbid 222 |
. . . . . . . 8
|
557 | 556 | simprd 479 |
. . . . . . 7
|
558 | 557 | adantr 481 |
. . . . . 6
|
559 | | simpr 477 |
. . . . . . 7
|
560 | 559 | rphalfcld 11884 |
. . . . . 6
|
561 | | breq2 4657 |
. . . . . . . . 9
|
562 | 561 | anbi2d 740 |
. . . . . . . 8
|
563 | 562 | rexralbidv 3058 |
. . . . . . 7
|
564 | 563 | rspccva 3308 |
. . . . . 6
|
565 | 558, 560,
564 | syl2anc 693 |
. . . . 5
|
566 | 460, 565 | r19.29a 3078 |
. . . 4
|
567 | 412, 566 | r19.29a 3078 |
. . 3
|
568 | 567 | ralrimiva 2966 |
. 2
|
569 | | ioosscn 39716 |
. . . 4
|
570 | 569 | a1i 11 |
. . 3
|
571 | 463, 570,
85 | ellimc3 23643 |
. 2
lim
|
572 | 135, 568,
571 | mpbir2and 957 |
1
lim |