Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pntlemj Structured version   Visualization version   Unicode version

Theorem pntlemj 24520
 Description: Lemma for pnt 24531. The induction step. Using pntibnd 24510, we find an interval in which is sufficiently large and has a much smaller value, (instead of our original bound ). (Contributed by Mario Carneiro, 13-Apr-2016.)
Hypotheses
Ref Expression
pntlem1.r ψ
pntlem1.a
pntlem1.b
pntlem1.l
pntlem1.d
pntlem1.f ;
pntlem1.u
pntlem1.u2
pntlem1.e
pntlem1.k
pntlem1.y
pntlem1.x
pntlem1.c
pntlem1.w ;
pntlem1.z
pntlem1.m
pntlem1.n
pntlem1.U
pntlem1.K
pntlem1.o
pntlem1.v
pntlem1.V
pntlem1.j ..^
pntlem1.i
Assertion
Ref Expression
pntlemj
Distinct variable groups:   ,   ,   ,,,   ,,,,   ,,,   ,,   ,,   ,   ,,   ,,,,   ,,   ,,   ,,   ,,,   ,,   ,,,,,   ,,,
Allowed substitution hints:   (,,,)   (,,,,)   (,,,,)   (,,,)   (,,,,)   ()   (,,)   (,,,,)   (,,,)   (,)   (,)   ()   (,,)   (,,)   (,,)   (,,)   (,,)   (,)   (,,)   (,)

Proof of Theorem pntlemj
StepHypRef Expression
1 pntlem1.r . . . . . . 7 ψ
2 pntlem1.a . . . . . . 7
3 pntlem1.b . . . . . . 7
4 pntlem1.l . . . . . . 7
5 pntlem1.d . . . . . . 7
6 pntlem1.f . . . . . . 7 ;
7 pntlem1.u . . . . . . 7
8 pntlem1.u2 . . . . . . 7
9 pntlem1.e . . . . . . 7
10 pntlem1.k . . . . . . 7
111, 2, 3, 4, 5, 6, 7, 8, 9, 10pntlemc 24512 . . . . . 6
1211simp3d 1044 . . . . 5
1312simp3d 1044 . . . 4
141, 2, 3, 4, 5, 6pntlemd 24511 . . . . . . . 8
1514simp1d 1042 . . . . . . 7
1611simp1d 1042 . . . . . . 7
1715, 16rpmulcld 11380 . . . . . 6
18 8nn 10796 . . . . . . 7
19 nnrp 11334 . . . . . . 7
2018, 19ax-mp 5 . . . . . 6
21 rpdivcl 11348 . . . . . 6
2217, 20, 21sylancl 675 . . . . 5
23 pntlem1.y . . . . . . . . 9
24 pntlem1.x . . . . . . . . 9
25 pntlem1.c . . . . . . . . 9
26 pntlem1.w . . . . . . . . 9 ;
27 pntlem1.z . . . . . . . . 9
281, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27pntlemb 24514 . . . . . . . 8 ;
2928simp1d 1042 . . . . . . 7
3029rpred 11364 . . . . . 6
3128simp2d 1043 . . . . . . 7
3231simp1d 1042 . . . . . 6
3330, 32rplogcld 23657 . . . . 5
3422, 33rpmulcld 11380 . . . 4
3513, 34rpmulcld 11380 . . 3
3635rpred 11364 . 2
37 pntlem1.i . . . . . 6
38 fzfid 12224 . . . . . 6
3937, 38syl5eqel 2553 . . . . 5
40 hashcl 12576 . . . . 5
4139, 40syl 17 . . . 4
4241nn0red 10950 . . 3
4313rpred 11364 . . . 4
44 pntlem1.v . . . . . . 7
4529, 44rpdivcld 11381 . . . . . 6
4645relogcld 23651 . . . . 5
4746, 45rerpdivcld 11392 . . . 4
4843, 47remulcld 9689 . . 3
4942, 48remulcld 9689 . 2
50 pntlem1.o . . . 4
51 fzfid 12224 . . . 4
5250, 51syl5eqel 2553 . . 3
537rpred 11364 . . . . . . 7
5453adantr 472 . . . . . 6
5511simp2d 1043 . . . . . . . . . . 11
56 pntlem1.j . . . . . . . . . . . . 13 ..^
57 elfzoelz 11947 . . . . . . . . . . . . 13 ..^
5856, 57syl 17 . . . . . . . . . . . 12
5958peano2zd 11066 . . . . . . . . . . 11
6055, 59rpexpcld 12477 . . . . . . . . . 10
6129, 60rpdivcld 11381 . . . . . . . . 9
6261rprege0d 11371 . . . . . . . 8
63 flge0nn0 12087 . . . . . . . 8
64 nn0p1nn 10933 . . . . . . . 8
6562, 63, 643syl 18 . . . . . . 7
66 elfzuz 11822 . . . . . . . 8
6766, 50eleq2s 2567 . . . . . . 7
68 eluznn 11252 . . . . . . 7
6965, 67, 68syl2an 485 . . . . . 6
7054, 69nndivred 10680 . . . . 5
7129adantr 472 . . . . . . . . . 10
7269nnrpd 11362 . . . . . . . . . 10
7371, 72rpdivcld 11381 . . . . . . . . 9
741pntrf 24480 . . . . . . . . . 10
7574ffvelrni 6036 . . . . . . . . 9
7673, 75syl 17 . . . . . . . 8
7776, 71rerpdivcld 11392 . . . . . . 7
7877recnd 9687 . . . . . 6
7978abscld 13575 . . . . 5
8070, 79resubcld 10068 . . . 4
8172relogcld 23651 . . . 4
8280, 81remulcld 9689 . . 3
8352, 82fsumrecl 13877 . 2
84 pntlem1.m . . 3
85 pntlem1.n . . 3
86 pntlem1.U . . 3
87 pntlem1.K . . 3
88 pntlem1.V . . 3
891, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85, 86, 87, 50, 44, 88, 56, 37pntlemr 24519 . 2
9048recnd 9687 . . . . 5
91 fsumconst 13928 . . . . 5
9239, 90, 91syl2anc 673 . . . 4
931, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85, 86, 87, 50, 44, 88, 56, 37pntlemq 24518 . . . . 5
9490ralrimivw 2810 . . . . 5
9552olcd 400 . . . . 5
96 sumss2 13869 . . . . 5
9793, 94, 95, 96syl21anc 1291 . . . 4
9892, 97eqtr3d 2507 . . 3
9948adantr 472 . . . . . 6
10099adantlr 729 . . . . 5
101 0red 9662 . . . . 5
102100, 101ifclda 3904 . . . 4
103 breq1 4398 . . . . 5
104 breq1 4398 . . . . 5
10513rpregt0d 11370 . . . . . . . . . 10
106105adantr 472 . . . . . . . . 9
107106simpld 466 . . . . . . . 8
108 1rp 11329 . . . . . . . . . . . . . . . . 17
109 rpaddcl 11346 . . . . . . . . . . . . . . . . 17
110108, 17, 109sylancr 676 . . . . . . . . . . . . . . . 16
111110, 44rpmulcld 11380 . . . . . . . . . . . . . . 15
11229, 111rpdivcld 11381 . . . . . . . . . . . . . 14
113112rprege0d 11371 . . . . . . . . . . . . 13
114 flge0nn0 12087 . . . . . . . . . . . . 13
115 nn0p1nn 10933 . . . . . . . . . . . . 13
116113, 114, 1153syl 18 . . . . . . . . . . . 12
117 elfzuz 11822 . . . . . . . . . . . . 13
118117, 37eleq2s 2567 . . . . . . . . . . . 12
119 eluznn 11252 . . . . . . . . . . . 12
120116, 118, 119syl2an 485 . . . . . . . . . . 11
121120nnrpd 11362 . . . . . . . . . 10
122121relogcld 23651 . . . . . . . . 9
123122, 120nndivred 10680 . . . . . . . 8
124107, 123remulcld 9689 . . . . . . 7
12593sselda 3418 . . . . . . . 8
126125, 82syldan 478 . . . . . . 7
127 simpr 468 . . . . . . . . . . . 12
128127, 37syl6eleq 2559 . . . . . . . . . . 11
129 elfzle2 11829 . . . . . . . . . . 11
130128, 129syl 17 . . . . . . . . . 10
13145rpred 11364 . . . . . . . . . . . 12
132131adantr 472 . . . . . . . . . . 11
133 elfzelz 11826 . . . . . . . . . . . 12
134128, 133syl 17 . . . . . . . . . . 11
135 flge 12074 . . . . . . . . . . 11
136132, 134, 135syl2anc 673 . . . . . . . . . 10
137130, 136mpbird 240 . . . . . . . . 9
138120nnred 10646 . . . . . . . . . 10
139 ere 14220 . . . . . . . . . . . 12
140139a1i 11 . . . . . . . . . . 11
141112rpred 11364 . . . . . . . . . . . 12
142141adantr 472 . . . . . . . . . . 11
143139a1i 11 . . . . . . . . . . . . 13
14429rpsqrtcld 13550 . . . . . . . . . . . . . 14
145144rpred 11364 . . . . . . . . . . . . 13
14631simp2d 1043 . . . . . . . . . . . . 13
147111rpred 11364 . . . . . . . . . . . . . . . . 17
14860rpred 11364 . . . . . . . . . . . . . . . . 17
14988simpld 466 . . . . . . . . . . . . . . . . . . . 20
150149simprd 470 . . . . . . . . . . . . . . . . . . 19
15155rpcnd 11366 . . . . . . . . . . . . . . . . . . . . 21
15255, 58rpexpcld 12477 . . . . . . . . . . . . . . . . . . . . . 22
153152rpcnd 11366 . . . . . . . . . . . . . . . . . . . . 21
154151, 153mulcomd 9682 . . . . . . . . . . . . . . . . . . . 20
1551, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemg 24515 . . . . . . . . . . . . . . . . . . . . . . . 24
156155simp1d 1042 . . . . . . . . . . . . . . . . . . . . . . 23
157 elfzouz 11951 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
15856, 157syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
159 eluznn 11252 . . . . . . . . . . . . . . . . . . . . . . 23
160156, 158, 159syl2anc 673 . . . . . . . . . . . . . . . . . . . . . 22
161160nnnn0d 10949 . . . . . . . . . . . . . . . . . . . . 21
162151, 161expp1d 12455 . . . . . . . . . . . . . . . . . . . 20
163154, 162eqtr4d 2508 . . . . . . . . . . . . . . . . . . 19
164150, 163breqtrd 4420 . . . . . . . . . . . . . . . . . 18
165147, 148, 164ltled 9800 . . . . . . . . . . . . . . . . 17
166 fzofzp1 12037 . . . . . . . . . . . . . . . . . . . 20 ..^
16756, 166syl 17 . . . . . . . . . . . . . . . . . . 19
1681, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemh 24516 . . . . . . . . . . . . . . . . . . 19
169167, 168mpdan 681 . . . . . . . . . . . . . . . . . 18
170169simprd 470 . . . . . . . . . . . . . . . . 17
171147, 148, 145, 165, 170letrd 9809 . . . . . . . . . . . . . . . 16
172147, 145, 144lemul2d 11405 . . . . . . . . . . . . . . . 16
173171, 172mpbid 215 . . . . . . . . . . . . . . 15
17429rprege0d 11371 . . . . . . . . . . . . . . . 16
175 remsqsqrt 13397 . . . . . . . . . . . . . . . 16
176174, 175syl 17 . . . . . . . . . . . . . . 15
177173, 176breqtrd 4420 . . . . . . . . . . . . . 14
178145, 30, 111lemuldivd 11410 . . . . . . . . . . . . . 14
179177, 178mpbid 215 . . . . . . . . . . . . 13
180143, 145, 141, 146, 179letrd 9809 . . . . . . . . . . . 12
181180adantr 472 . . . . . . . . . . 11
182 reflcl 12065 . . . . . . . . . . . . . 14
183 peano2re 9824 . . . . . . . . . . . . . 14
184141, 182, 1833syl 18 . . . . . . . . . . . . 13
185184adantr 472 . . . . . . . . . . . 12
186 fllep1 12070 . . . . . . . . . . . . 13
187142, 186syl 17 . . . . . . . . . . . 12
188 elfzle1 11828 . . . . . . . . . . . . 13
189128, 188syl 17 . . . . . . . . . . . 12
190142, 185, 138, 187, 189letrd 9809 . . . . . . . . . . 11
191140, 142, 138, 181, 190letrd 9809 . . . . . . . . . 10
192140, 138, 132, 191, 137letrd 9809 . . . . . . . . . 10
193 logdivle 23650 . . . . . . . . . 10
194138, 191, 132, 192, 193syl22anc 1293 . . . . . . . . 9
195137, 194mpbid 215 . . . . . . . 8
19647adantr 472 . . . . . . . . 9
197 lemul2 10480 . . . . . . . . 9
198196, 123, 106, 197syl3anc 1292 . . . . . . . 8
199195, 198mpbid 215 . . . . . . 7
20013rpcnd 11366 . . . . . . . . . . 11
201200adantr 472 . . . . . . . . . 10
202122recnd 9687 . . . . . . . . . 10
203121rpcnne0d 11373 . . . . . . . . . 10
204 div23 10311 . . . . . . . . . 10
205201, 202, 203, 204syl3anc 1292 . . . . . . . . 9
206 divass 10310 . . . . . . . . . 10
207201, 202, 203, 206syl3anc 1292 . . . . . . . . 9
208205, 207eqtr3d 2507 . . . . . . . 8
20943adantr 472 . . . . . . . . . 10
210209, 120nndivred 10680 . . . . . . . . 9
211125, 80syldan 478 . . . . . . . . 9
212 log1 23614 . . . . . . . . . 10
213120nnge1d 10674 . . . . . . . . . . 11
214 logleb 23631 . . . . . . . . . . . 12
215108, 121, 214sylancr 676 . . . . . . . . . . 11
216213, 215mpbid 215 . . . . . . . . . 10
217212, 216syl5eqbrr 4430 . . . . . . . . 9
2187rpcnd 11366 . . . . . . . . . . . 12
219218adantr 472 . . . . . . . . . . 11
22016rpred 11364 . . . . . . . . . . . . 13
221220adantr 472 . . . . . . . . . . . 12
222221recnd 9687 . . . . . . . . . . 11
223 divsubdir 10325 . . . . . . . . . . 11
224219, 222, 203, 223syl3anc 1292 . . . . . . . . . 10
225125, 79syldan 478 . . . . . . . . . . 11
226221, 120nndivred 10680 . . . . . . . . . . 11
227125, 70syldan 478 . . . . . . . . . . 11
228125, 76syldan 478 . . . . . . . . . . . . . . . . . 18
229228recnd 9687 . . . . . . . . . . . . . . . . 17
23029adantr 472 . . . . . . . . . . . . . . . . . 18
231230rpcnne0d 11373 . . . . . . . . . . . . . . . . 17
232 divdiv2 10341 . . . . . . . . . . . . . . . . 17
233229, 231, 203, 232syl3anc 1292 . . . . . . . . . . . . . . . 16
234121rpcnd 11366 . . . . . . . . . . . . . . . . 17
235 div23 10311 . . . . . . . . . . . . . . . . 17
236229, 234, 231, 235syl3anc 1292 . . . . . . . . . . . . . . . 16
237233, 236eqtrd 2505 . . . . . . . . . . . . . . 15
238237fveq2d 5883 . . . . . . . . . . . . . 14
239125, 78syldan 478 . . . . . . . . . . . . . . 15
240239, 234absmuld 13593 . . . . . . . . . . . . . 14
241121rprege0d 11371 . . . . . . . . . . . . . . . 16
242 absid 13436 . . . . . . . . . . . . . . . 16
243241, 242syl 17 . . . . . . . . . . . . . . 15
244243oveq2d 6324 . . . . . . . . . . . . . 14
245238, 240, 2443eqtrd 2509 . . . . . . . . . . . . 13
24630adantr 472 . . . . . . . . . . . . . . . 16
247246, 120nndivred 10680 . . . . . . . . . . . . . . 15
24844rpregt0d 11370 . . . . . . . . . . . . . . . . . . 19
249248adantr 472 . . . . . . . . . . . . . . . . . 18
250 lemuldiv2 10509 . . . . . . . . . . . . . . . . . 18
251138, 246, 249, 250syl3anc 1292 . . . . . . . . . . . . . . . . 17
252137, 251mpbird 240 . . . . . . . . . . . . . . . 16
253249simpld 466 . . . . . . . . . . . . . . . . 17
254253, 246, 121lemuldivd 11410 . . . . . . . . . . . . . . . 16
255252, 254mpbid 215 . . . . . . . . . . . . . . 15
256111rpregt0d 11370 . . . . . . . . . . . . . . . . . 18
257256adantr 472 . . . . . . . . . . . . . . . . 17
258121rpregt0d 11370 . . . . . . . . . . . . . . . . 17
259 lediv23 10520 . . . . . . . . . . . . . . . . 17
260246, 257, 258, 259syl3anc 1292 . . . . . . . . . . . . . . . 16
261190, 260mpbid 215 . . . . . . . . . . . . . . 15
26244rpred 11364 . . . . . . . . . . . . . . . . 17
263262adantr 472 . . . . . . . . . . . . . . . 16
264147adantr 472 . . . . . . . . . . . . . . . 16
265 elicc2 11724 . . . . . . . . . . . . . . . 16
266263, 264, 265syl2anc 673 . . . . . . . . . . . . . . 15
267247, 255, 261, 266mpbir3and 1213 . . . . . . . . . . . . . 14
26888simprd 470 . . . . . . . . . . . . . . 15
269268adantr 472 . . . . . . . . . . . . . 14
270 fveq2 5879 . . . . . . . . . . . . . . . . . 18
271 id 22 . . . . . . . . . . . . . . . . . 18
272270, 271oveq12d 6326 . . . . . . . . . . . . . . . . 17
273272fveq2d 5883 . . . . . . . . . . . . . . . 16
274273breq1d 4405 . . . . . . . . . . . . . . 15
275274rspcv 3132 . . . . . . . . . . . . . 14
276267, 269, 275sylc 61 . . . . . . . . . . . . 13
277245, 276eqbrtrrd 4418 . . . . . . . . . . . 12
278225, 221, 121lemuldivd 11410 . . . . . . . . . . . 12
279277, 278mpbid 215 . . . . . . . . . . 11
280225, 226, 227, 279lesub2dd 10251 . . . . . . . . . 10
281224, 280eqbrtrd 4416 . . . . . . . . 9
282210, 211, 122, 217, 281lemul1ad 10568 . . . . . . . 8
283208, 282eqbrtrrd 4418 . . . . . . 7
28499, 124, 126, 199, 283letrd 9809 . . . . . 6
285284adantlr 729 . . . . 5
28669nnred 10646 . . . . . . . . 9
28729, 152rpdivcld 11381 . . . . . . . . . . 11
288287rpred 11364 . . . . . . . . . 10
289288adantr 472 . . . . . . . . 9
29023simpld 466 . . . . . . . . . . . 12
29129, 290rpdivcld 11381 . . . . . . . . . . 11
292291rpred 11364 . . . . . . . . . 10
293292adantr 472 . . . . . . . . 9
294 simpr 468 . . . . . . . . . . . 12
295294, 50syl6eleq 2559 . . . . . . . . . . 11
296 elfzle2 11829 . . . . . . . . . . 11
297295, 296syl 17 . . . . . . . . . 10
29869nnzd 11062 . . . . . . . . . . 11
299 flge 12074 . . . . . . . . . . 11
300289, 298, 299syl2anc 673 . . . . . . . . . 10
301297, 300mpbird 240 . . . . . . . . 9
302290rpred 11364 . . . . . . . . . . . 12
30324simpld 466 . . . . . . . . . . . . 13
304303rpred 11364 . . . . . . . . . . . 12
305152rpred 11364 . . . . . . . . . . . 12
30624simprd 470 . . . . . . . . . . . . 13
307302, 304, 306ltled 9800 . . . . . . . . . . . 12
308 elfzofz 11962 . . . . . . . . . . . . . . . 16 ..^
30956, 308syl 17 . . . . . . . . . . . . . . 15
3101, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85pntlemh 24516 . . . . . . . . . . . . . . 15
311309, 310mpdan 681 . . . . . . . . . . . . . 14
312311simpld 466 . . . . . . . . . . . . 13
313304, 305, 312ltled 9800 . . . . . . . . . . . 12
314302, 304, 305, 307, 313letrd 9809 . . . . . . . . . . 11
315290, 152, 29lediv2d 11388 . . . . . . . . . . 11
316314, 315mpbid 215 . . . . . . . . . 10
317316adantr 472 . . . . . . . . 9
318286, 289, 293, 301, 317letrd 9809 . . . . . . . 8
31969, 318jca 541 . . . . . . 7
3201, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 24, 25, 26, 27, 84, 85, 86pntlemn 24517 . . . . . . 7
321319, 320syldan 478 . . . . . 6
322321adantr 472 . . . . 5
323103, 104, 285, 322ifbothda 3907 . . . 4
32452, 102, 82, 323fsumle 13936 . . 3
32598, 324eqbrtrd 4416 . 2
32636, 49, 83, 89, 325letrd 9809 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wo 375   wa 376   w3a 1007   wceq 1452   wcel 1904   wne 2641  wral 2756  wrex 2757   wss 3390  cif 3872   class class class wbr 4395   cmpt 4454  cfv 5589  (class class class)co 6308  cfn 7587  cc 9555  cr 9556  cc0 9557  c1 9558   caddc 9560   cmul 9562   cpnf 9690   clt 9693   cle 9694   cmin 9880   cdiv 10291  cn 10631  c2 10681  c3 10682  c4 10683  c8 10687  cn0 10893  cz 10961  ;cdc 11074  cuz 11182  crp 11325  cioo 11660  cico 11662  cicc 11663  cfz 11810  ..^cfzo 11942  cfl 12059  cexp 12310  chash 12553  csqrt 13373  cabs 13374  csu 13829  ce 14191  ceu 14192  clog 23583  ψcchp 24098 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635  ax-addf 9636  ax-mulf 9637 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-iin 4272  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-om 6712  df-1st 6812  df-2nd 6813  df-supp 6934  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-ixp 7541  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fsupp 7902  df-fi 7943  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-4 10692  df-5 10693  df-6 10694  df-7 10695  df-8 10696  df-9 10697  df-10 10698  df-n0 10894  df-z 10962  df-dec 11075  df-uz 11183  df-q 11288  df-rp 11326  df-xneg 11432  df-xadd 11433  df-xmul 11434  df-ioo 11664  df-ioc 11665  df-ico 11666  df-icc 11667  df-fz 11811  df-fzo 11943  df-fl 12061  df-mod 12130  df-seq 12252  df-exp 12311  df-fac 12498  df-bc 12526  df-hash 12554  df-shft 13207  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-limsup 13603  df-clim 13629  df-rlim 13630  df-sum 13830  df-ef 14198  df-e 14199  df-sin 14200  df-cos 14201  df-pi 14203  df-dvds 14383  df-gcd 14548  df-prm 14702  df-pc 14866  df-struct 15201  df-ndx 15202  df-slot 15203  df-base 15204  df-sets 15205  df-ress 15206  df-plusg 15281  df-mulr 15282  df-starv 15283  df-sca 15284  df-vsca 15285  df-ip 15286  df-tset 15287  df-ple 15288  df-ds 15290  df-unif 15291  df-hom 15292  df-cco 15293  df-rest 15399  df-topn 15400  df-0g 15418  df-gsum 15419  df-topgen 15420  df-pt 15421  df-prds 15424  df-xrs 15478  df-qtop 15484  df-imas 15485  df-xps 15488  df-mre 15570  df-mrc 15571  df-acs 15573  df-mgm 16566  df-sgrp 16605  df-mnd 16615  df-submnd 16661  df-mulg 16754  df-cntz 17049  df-cmn 17510  df-psmet 19039  df-xmet 19040  df-met 19041  df-bl 19042  df-mopn 19043  df-fbas 19044  df-fg 19045  df-cnfld 19048  df-top 19998  df-bases 19999  df-topon 20000  df-topsp 20001  df-cld 20111  df-ntr 20112  df-cls 20113  df-nei 20191  df-lp 20229  df-perf 20230  df-cn 20320  df-cnp 20321  df-haus 20408  df-tx 20654  df-hmeo 20847  df-fil 20939  df-fm 21031  df-flim 21032  df-flf 21033  df-xms 21413  df-ms 21414  df-tms 21415  df-cncf 21988  df-limc 22900  df-dv 22901  df-log 23585  df-vma 24103  df-chp 24104 This theorem is referenced by:  pntlemi  24521
 Copyright terms: Public domain W3C validator