Step | Hyp | Ref
| Expression |
1 | | 0cnd 10033 |
. 2
|
2 | | 0ellimcdiv.d |
. . . . . . . . 9
lim |
3 | | 0ellimcdiv.c |
. . . . . . . . . . . 12
|
4 | 3 | eldifad 3586 |
. . . . . . . . . . 11
|
5 | | 0ellimcdiv.g |
. . . . . . . . . . 11
|
6 | 4, 5 | fmptd 6385 |
. . . . . . . . . 10
|
7 | | 0ellimcdiv.f |
. . . . . . . . . . 11
|
8 | | 0ellimcdiv.b |
. . . . . . . . . . 11
|
9 | | 0ellimcdiv.0limf |
. . . . . . . . . . 11
lim |
10 | 7, 8, 9 | limcmptdm 39867 |
. . . . . . . . . 10
|
11 | | limcrcl 23638 |
. . . . . . . . . . . 12
lim
|
12 | 2, 11 | syl 17 |
. . . . . . . . . . 11
|
13 | 12 | simp3d 1075 |
. . . . . . . . . 10
|
14 | 6, 10, 13 | ellimc3 23643 |
. . . . . . . . 9
lim
|
15 | 2, 14 | mpbid 222 |
. . . . . . . 8
|
16 | 15 | simprd 479 |
. . . . . . 7
|
17 | 15 | simpld 475 |
. . . . . . . . 9
|
18 | | 0ellimcdiv.dne0 |
. . . . . . . . 9
|
19 | 17, 18 | absrpcld 14187 |
. . . . . . . 8
|
20 | 19 | rphalfcld 11884 |
. . . . . . 7
|
21 | | breq2 4657 |
. . . . . . . . . 10
|
22 | 21 | imbi2d 330 |
. . . . . . . . 9
|
23 | 22 | rexralbidv 3058 |
. . . . . . . 8
|
24 | 23 | rspccva 3308 |
. . . . . . 7
|
25 | 16, 20, 24 | syl2anc 693 |
. . . . . 6
|
26 | | simpl1l 1112 |
. . . . . . . . . 10
|
27 | | simpl3 1066 |
. . . . . . . . . 10
|
28 | | simpr 477 |
. . . . . . . . . . 11
|
29 | | simpl2 1065 |
. . . . . . . . . . 11
|
30 | 27, 28, 29 | mp2d 49 |
. . . . . . . . . 10
|
31 | 19 | rpcnd 11874 |
. . . . . . . . . . . . . . . 16
|
32 | 31 | 2halvesd 11278 |
. . . . . . . . . . . . . . 15
|
33 | 32 | eqcomd 2628 |
. . . . . . . . . . . . . 14
|
34 | 33 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
35 | | 2cnd 11093 |
. . . . . . . . . . . . . . . 16
|
36 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . 17
|
37 | 36 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
38 | 17, 35, 37 | absdivd 14194 |
. . . . . . . . . . . . . . 15
|
39 | | 2re 11090 |
. . . . . . . . . . . . . . . . . 18
|
40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
41 | | 0le2 11111 |
. . . . . . . . . . . . . . . . . 18
|
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
43 | 40, 42 | absidd 14161 |
. . . . . . . . . . . . . . . 16
|
44 | 43 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
45 | 38, 44 | eqtr2d 2657 |
. . . . . . . . . . . . . 14
|
46 | 45 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
47 | 20 | rpcnd 11874 |
. . . . . . . . . . . . . 14
|
48 | 47, 47 | pncand 10393 |
. . . . . . . . . . . . 13
|
49 | 34, 46, 48 | 3eqtr3rd 2665 |
. . . . . . . . . . . 12
|
50 | 49 | 3ad2ant1 1082 |
. . . . . . . . . . 11
|
51 | 45 | eqcomd 2628 |
. . . . . . . . . . . . . 14
|
52 | 51 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
|
53 | 52 | oveq2d 6666 |
. . . . . . . . . . . 12
|
54 | 17 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
55 | 54 | abscld 14175 |
. . . . . . . . . . . . . . 15
|
56 | 55 | 3adant3 1081 |
. . . . . . . . . . . . . 14
|
57 | 6 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
|
58 | 57 | 3adant3 1081 |
. . . . . . . . . . . . . . . 16
|
59 | 58 | abscld 14175 |
. . . . . . . . . . . . . . 15
|
60 | 17 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . 17
|
61 | 60, 58 | subcld 10392 |
. . . . . . . . . . . . . . . 16
|
62 | 61 | abscld 14175 |
. . . . . . . . . . . . . . 15
|
63 | 59, 62 | readdcld 10069 |
. . . . . . . . . . . . . 14
|
64 | 56 | rehalfcld 11279 |
. . . . . . . . . . . . . . 15
|
65 | 59, 64 | readdcld 10069 |
. . . . . . . . . . . . . 14
|
66 | 57, 54 | pncan3d 10395 |
. . . . . . . . . . . . . . . . . 18
|
67 | 66 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
|
68 | 67 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
69 | 54, 57 | subcld 10392 |
. . . . . . . . . . . . . . . . 17
|
70 | 57, 69 | abstrid 14195 |
. . . . . . . . . . . . . . . 16
|
71 | 68, 70 | eqbrtrd 4675 |
. . . . . . . . . . . . . . 15
|
72 | 71 | 3adant3 1081 |
. . . . . . . . . . . . . 14
|
73 | 60, 58 | abssubd 14192 |
. . . . . . . . . . . . . . . 16
|
74 | | simp3 1063 |
. . . . . . . . . . . . . . . 16
|
75 | 73, 74 | eqbrtrd 4675 |
. . . . . . . . . . . . . . 15
|
76 | 62, 64, 59, 75 | ltadd2dd 10196 |
. . . . . . . . . . . . . 14
|
77 | 56, 63, 65, 72, 76 | lelttrd 10195 |
. . . . . . . . . . . . 13
|
78 | 57 | abscld 14175 |
. . . . . . . . . . . . . . 15
|
79 | 78 | 3adant3 1081 |
. . . . . . . . . . . . . 14
|
80 | 56, 64, 79 | ltsubaddd 10623 |
. . . . . . . . . . . . 13
|
81 | 77, 80 | mpbird 247 |
. . . . . . . . . . . 12
|
82 | 53, 81 | eqbrtrd 4675 |
. . . . . . . . . . 11
|
83 | 50, 82 | eqbrtrd 4675 |
. . . . . . . . . 10
|
84 | 26, 27, 30, 83 | syl3anc 1326 |
. . . . . . . . 9
|
85 | 84 | 3exp1 1283 |
. . . . . . . 8
|
86 | 85 | ralimdv2 2961 |
. . . . . . 7
|
87 | 86 | reximdva 3017 |
. . . . . 6
|
88 | 25, 87 | mpd 15 |
. . . . 5
|
89 | 88 | adantr 481 |
. . . 4
|
90 | | simpr 477 |
. . . . . . . . 9
|
91 | 17 | adantr 481 |
. . . . . . . . . . 11
|
92 | 18 | adantr 481 |
. . . . . . . . . . 11
|
93 | 91, 92 | absrpcld 14187 |
. . . . . . . . . 10
|
94 | 93 | rphalfcld 11884 |
. . . . . . . . 9
|
95 | 90, 94 | rpmulcld 11888 |
. . . . . . . 8
|
96 | 95 | ex 450 |
. . . . . . . . 9
|
97 | 96 | imdistani 726 |
. . . . . . . 8
|
98 | | eleq1 2689 |
. . . . . . . . . . 11
|
99 | 98 | anbi2d 740 |
. . . . . . . . . 10
|
100 | | breq2 4657 |
. . . . . . . . . . . 12
|
101 | 100 | imbi2d 330 |
. . . . . . . . . . 11
|
102 | 101 | rexralbidv 3058 |
. . . . . . . . . 10
|
103 | 99, 102 | imbi12d 334 |
. . . . . . . . 9
|
104 | 8, 7 | fmptd 6385 |
. . . . . . . . . . . . 13
|
105 | 104, 10, 13 | ellimc3 23643 |
. . . . . . . . . . . 12
lim
|
106 | 9, 105 | mpbid 222 |
. . . . . . . . . . 11
|
107 | 106 | simprd 479 |
. . . . . . . . . 10
|
108 | 107 | r19.21bi 2932 |
. . . . . . . . 9
|
109 | 103, 108 | vtoclg 3266 |
. . . . . . . 8
|
110 | 95, 97, 109 | sylc 65 |
. . . . . . 7
|
111 | 110 | 3ad2ant1 1082 |
. . . . . 6
|
112 | | simp12 1092 |
. . . . . . . . 9
|
113 | | simp2 1062 |
. . . . . . . . 9
|
114 | 112, 113 | ifcld 4131 |
. . . . . . . 8
|
115 | | nfv 1843 |
. . . . . . . . . . 11
|
116 | | nfv 1843 |
. . . . . . . . . . 11
|
117 | | nfra1 2941 |
. . . . . . . . . . 11
|
118 | 115, 116,
117 | nf3an 1831 |
. . . . . . . . . 10
|
119 | | nfv 1843 |
. . . . . . . . . 10
|
120 | | nfra1 2941 |
. . . . . . . . . 10
|
121 | 118, 119,
120 | nf3an 1831 |
. . . . . . . . 9
|
122 | | simp111 1190 |
. . . . . . . . . . . . 13
|
123 | | simp112 1191 |
. . . . . . . . . . . . 13
|
124 | | simp12 1092 |
. . . . . . . . . . . . 13
|
125 | 122, 123,
124 | jca31 557 |
. . . . . . . . . . . 12
|
126 | | simp2 1062 |
. . . . . . . . . . . 12
|
127 | | simp3l 1089 |
. . . . . . . . . . . 12
|
128 | 125, 126,
127 | jca31 557 |
. . . . . . . . . . 11
|
129 | 10 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
130 | 129 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . 18
|
131 | 130 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . 17
|
132 | 131 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
|
133 | 132, 126 | sseldd 3604 |
. . . . . . . . . . . . . . 15
|
134 | 13 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
135 | 134 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . 17
|
136 | 135 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
|
137 | 136 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
|
138 | 133, 137 | subcld 10392 |
. . . . . . . . . . . . . 14
|
139 | 138 | abscld 14175 |
. . . . . . . . . . . . 13
|
140 | 123 | rpred 11872 |
. . . . . . . . . . . . . 14
|
141 | 124 | rpred 11872 |
. . . . . . . . . . . . . 14
|
142 | 140, 141 | ifcld 4131 |
. . . . . . . . . . . . 13
|
143 | | simp3r 1090 |
. . . . . . . . . . . . 13
|
144 | | min1 12020 |
. . . . . . . . . . . . . 14
|
145 | 140, 141,
144 | syl2anc 693 |
. . . . . . . . . . . . 13
|
146 | 139, 142,
140, 143, 145 | ltletrd 10197 |
. . . . . . . . . . . 12
|
147 | | simp113 1192 |
. . . . . . . . . . . . 13
|
148 | | rspa 2930 |
. . . . . . . . . . . . 13
|
149 | 147, 126,
148 | syl2anc 693 |
. . . . . . . . . . . 12
|
150 | 127, 146,
149 | mp2and 715 |
. . . . . . . . . . 11
|
151 | | simp13 1093 |
. . . . . . . . . . . . 13
|
152 | | rspa 2930 |
. . . . . . . . . . . . 13
|
153 | 151, 126,
152 | syl2anc 693 |
. . . . . . . . . . . 12
|
154 | | min2 12021 |
. . . . . . . . . . . . . . 15
|
155 | 140, 141,
154 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
156 | 139, 142,
141, 143, 155 | ltletrd 10197 |
. . . . . . . . . . . . 13
|
157 | 127, 156 | jca 554 |
. . . . . . . . . . . 12
|
158 | 122 | simpld 475 |
. . . . . . . . . . . . . . 15
|
159 | 158 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
|
160 | | simp12 1092 |
. . . . . . . . . . . . . 14
|
161 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . 19
|
162 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . . . . . . . 22
|
163 | 7, 162 | nfcxfr 2762 |
. . . . . . . . . . . . . . . . . . . . 21
|
164 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . 21
|
165 | 163, 164 | nffv 6198 |
. . . . . . . . . . . . . . . . . . . 20
|
166 | 165 | nfel1 2779 |
. . . . . . . . . . . . . . . . . . 19
|
167 | 161, 166 | nfim 1825 |
. . . . . . . . . . . . . . . . . 18
|
168 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . 20
|
169 | 168 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . 19
|
170 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
171 | 170 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . 19
|
172 | 169, 171 | imbi12d 334 |
. . . . . . . . . . . . . . . . . 18
|
173 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
174 | 7 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . . . 20
|
175 | 173, 8, 174 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
176 | 175, 8 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . 18
|
177 | 167, 172,
176 | chvar 2262 |
. . . . . . . . . . . . . . . . 17
|
178 | 177 | subid1d 10381 |
. . . . . . . . . . . . . . . 16
|
179 | 178 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
|
180 | 179 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
181 | 159, 160,
180 | syl2anc 693 |
. . . . . . . . . . . . 13
|
182 | | simp3 1063 |
. . . . . . . . . . . . . 14
|
183 | | simp2 1062 |
. . . . . . . . . . . . . 14
|
184 | 182, 183 | mpd 15 |
. . . . . . . . . . . . 13
|
185 | 181, 184 | eqbrtrd 4675 |
. . . . . . . . . . . 12
|
186 | 153, 157,
185 | mpd3an23 1426 |
. . . . . . . . . . 11
|
187 | | simp-7l 812 |
. . . . . . . . . . . . 13
|
188 | | simp-4r 807 |
. . . . . . . . . . . . 13
|
189 | | eldifsni 4320 |
. . . . . . . . . . . . . . . . . . . 20
|
190 | 3, 189 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
191 | 8, 4, 190 | divcld 10801 |
. . . . . . . . . . . . . . . . . 18
|
192 | | 0ellimcdiv.h |
. . . . . . . . . . . . . . . . . 18
|
193 | 191, 192 | fmptd 6385 |
. . . . . . . . . . . . . . . . 17
|
194 | 193 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . 16
|
195 | 194 | subid1d 10381 |
. . . . . . . . . . . . . . 15
|
196 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . . . . . 20
|
197 | 192, 196 | nfcxfr 2762 |
. . . . . . . . . . . . . . . . . . 19
|
198 | 197, 164 | nffv 6198 |
. . . . . . . . . . . . . . . . . 18
|
199 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
|
200 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . . . . . . 21
|
201 | 5, 200 | nfcxfr 2762 |
. . . . . . . . . . . . . . . . . . . 20
|
202 | 201, 164 | nffv 6198 |
. . . . . . . . . . . . . . . . . . 19
|
203 | 165, 199,
202 | nfov 6676 |
. . . . . . . . . . . . . . . . . 18
|
204 | 198, 203 | nfeq 2776 |
. . . . . . . . . . . . . . . . 17
|
205 | 161, 204 | nfim 1825 |
. . . . . . . . . . . . . . . 16
|
206 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
207 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
|
208 | 170, 207 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
|
209 | 206, 208 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . 17
|
210 | 169, 209 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
|
211 | 192 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . 18
|
212 | 173, 191,
211 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
213 | 175 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . 18
|
214 | 5 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . . . 20
|
215 | 173, 3, 214 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
216 | 215 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . 18
|
217 | 213, 216 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
|
218 | 212, 217 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
219 | 205, 210,
218 | chvar 2262 |
. . . . . . . . . . . . . . 15
|
220 | 195, 219 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
221 | 220 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
222 | 187, 188,
221 | syl2anc 693 |
. . . . . . . . . . . 12
|
223 | | simp-6l 810 |
. . . . . . . . . . . . . 14
|
224 | 223, 188 | jca 554 |
. . . . . . . . . . . . 13
|
225 | | simplr 792 |
. . . . . . . . . . . . 13
|
226 | | simpr 477 |
. . . . . . . . . . . . 13
|
227 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . 20
|
228 | 202, 227 | nfne 2894 |
. . . . . . . . . . . . . . . . . . 19
|
229 | 161, 228 | nfim 1825 |
. . . . . . . . . . . . . . . . . 18
|
230 | 207 | neeq1d 2853 |
. . . . . . . . . . . . . . . . . . 19
|
231 | 169, 230 | imbi12d 334 |
. . . . . . . . . . . . . . . . . 18
|
232 | 215, 190 | eqnetrd 2861 |
. . . . . . . . . . . . . . . . . 18
|
233 | 229, 231,
232 | chvar 2262 |
. . . . . . . . . . . . . . . . 17
|
234 | 177, 57, 233 | absdivd 14194 |
. . . . . . . . . . . . . . . 16
|
235 | 234 | adantlr 751 |
. . . . . . . . . . . . . . 15
|
236 | 235 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
237 | 177 | abscld 14175 |
. . . . . . . . . . . . . . . . . 18
|
238 | 57, 233 | absne0d 14186 |
. . . . . . . . . . . . . . . . . 18
|
239 | 237, 78, 238 | redivcld 10853 |
. . . . . . . . . . . . . . . . 17
|
240 | 239 | adantlr 751 |
. . . . . . . . . . . . . . . 16
|
241 | 240 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
242 | | rpre 11839 |
. . . . . . . . . . . . . . . . . . 19
|
243 | 242 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
|
244 | 20 | rpred 11872 |
. . . . . . . . . . . . . . . . . . 19
|
245 | 244 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
246 | 243, 245 | remulcld 10070 |
. . . . . . . . . . . . . . . . 17
|
247 | 246 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
248 | 57, 233 | absrpcld 14187 |
. . . . . . . . . . . . . . . . . 18
|
249 | 248 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
|
250 | 249 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
251 | 247, 250 | rerpdivcld 11903 |
. . . . . . . . . . . . . . 15
|
252 | 243 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
253 | | simp-4l 806 |
. . . . . . . . . . . . . . . . 17
|
254 | | simpllr 799 |
. . . . . . . . . . . . . . . . 17
|
255 | 253, 254,
237 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
256 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
257 | 255, 247,
250, 256 | ltdiv1dd 11929 |
. . . . . . . . . . . . . . 15
|
258 | 243 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
|
259 | 47 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
|
260 | 249 | rpcnd 11874 |
. . . . . . . . . . . . . . . . . . . 20
|
261 | 238 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . 20
|
262 | 258, 259,
260, 261 | divassd 10836 |
. . . . . . . . . . . . . . . . . . 19
|
263 | 262 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
264 | 245, 249 | rerpdivcld 11903 |
. . . . . . . . . . . . . . . . . . . 20
|
265 | 264 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
266 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . 19
|
267 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . 19
|
268 | 244 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
|
269 | | 1rp 11836 |
. . . . . . . . . . . . . . . . . . . . . 22
|
270 | 269 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
271 | 248 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
272 | 47 | div1d 10793 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
273 | 272 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
|
274 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
|
275 | 273, 274 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . . 21
|
276 | 268, 270,
271, 275 | ltdiv23d 11937 |
. . . . . . . . . . . . . . . . . . . 20
|
277 | 276 | adantllr 755 |
. . . . . . . . . . . . . . . . . . 19
|
278 | 265, 266,
267, 277 | ltmul2dd 11928 |
. . . . . . . . . . . . . . . . . 18
|
279 | 263, 278 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . 17
|
280 | 258 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . 18
|
281 | 280 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
282 | 279, 281 | breqtrd 4679 |
. . . . . . . . . . . . . . . 16
|
283 | 282 | adantr 481 |
. . . . . . . . . . . . . . 15
|
284 | 241, 251,
252, 257, 283 | lttrd 10198 |
. . . . . . . . . . . . . 14
|
285 | 236, 284 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
|
286 | 224, 225,
226, 285 | syl21anc 1325 |
. . . . . . . . . . . 12
|
287 | 222, 286 | eqbrtrd 4675 |
. . . . . . . . . . 11
|
288 | 128, 150,
186, 287 | syl21anc 1325 |
. . . . . . . . . 10
|
289 | 288 | 3exp 1264 |
. . . . . . . . 9
|
290 | 121, 289 | ralrimi 2957 |
. . . . . . . 8
|
291 | | breq2 4657 |
. . . . . . . . . . . 12
|
292 | 291 | anbi2d 740 |
. . . . . . . . . . 11
|
293 | 292 | imbi1d 331 |
. . . . . . . . . 10
|
294 | 293 | ralbidv 2986 |
. . . . . . . . 9
|
295 | 294 | rspcev 3309 |
. . . . . . . 8
|
296 | 114, 290,
295 | syl2anc 693 |
. . . . . . 7
|
297 | 296 | rexlimdv3a 3033 |
. . . . . 6
|
298 | 111, 297 | mpd 15 |
. . . . 5
|
299 | 298 | rexlimdv3a 3033 |
. . . 4
|
300 | 89, 299 | mpd 15 |
. . 3
|
301 | 300 | ralrimiva 2966 |
. 2
|
302 | 193, 10, 13 | ellimc3 23643 |
. 2
lim
|
303 | 1, 301, 302 | mpbir2and 957 |
1
lim |