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

Theorem pntlem3 24526
 Description: Lemma for pnt 24531. Equation 10.6.35 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 8-Apr-2016.) (Proof shortened by AV, 27-Sep-2020.)
Hypotheses
Ref Expression
pntlem3.r ψ
pntlem3.a
pntlem3.A
pntlem3.1
pntlem3.2
pntlem3.3
Assertion
Ref Expression
pntlem3 ψ
Distinct variable groups:   ,,,,   ,,,,   ,   ,,,,,   ,   ,,   ,,,,,
Allowed substitution hints:   ()   (,)   (,,,,)   ()   (,,,)

Proof of Theorem pntlem3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rpssre 11335 . . . 4
2 eqid 2471 . . . . . . . . . . 11 fld fld
32subcn 21976 . . . . . . . . . . . 12 fld fld fld
43a1i 11 . . . . . . . . . . 11 inf fld fld fld
5 ssid 3437 . . . . . . . . . . . . 13
6 cncfmptid 22022 . . . . . . . . . . . . 13
75, 5, 6mp2an 686 . . . . . . . . . . . 12
87a1i 11 . . . . . . . . . . 11 inf
9 pntlem3.2 . . . . . . . . . . . . . . 15
109adantr 472 . . . . . . . . . . . . . 14 inf
1110rpcnd 11366 . . . . . . . . . . . . 13 inf
125a1i 11 . . . . . . . . . . . . 13 inf
13 cncfmptc 22021 . . . . . . . . . . . . 13
1411, 12, 12, 13syl3anc 1292 . . . . . . . . . . . 12 inf
15 3nn0 10911 . . . . . . . . . . . . . 14
162expcn 21982 . . . . . . . . . . . . . 14 fld fld
1715, 16mp1i 13 . . . . . . . . . . . . 13 inf fld fld
182cncfcn1 22020 . . . . . . . . . . . . 13 fld fld
1917, 18syl6eleqr 2560 . . . . . . . . . . . 12 inf
2014, 19mulcncf 22476 . . . . . . . . . . 11 inf
212, 4, 8, 20cncfmpt2f 22024 . . . . . . . . . 10 inf
22 pntlem3.1 . . . . . . . . . . . . . . 15
23 ssrab2 3500 . . . . . . . . . . . . . . 15
2422, 23eqsstri 3448 . . . . . . . . . . . . . 14
25 0re 9661 . . . . . . . . . . . . . . 15
26 pntlem3.a . . . . . . . . . . . . . . . 16
2726rpred 11364 . . . . . . . . . . . . . . 15
28 iccssre 11741 . . . . . . . . . . . . . . 15
2925, 27, 28sylancr 676 . . . . . . . . . . . . . 14
3024, 29syl5ss 3429 . . . . . . . . . . . . 13
31 0xr 9705 . . . . . . . . . . . . . . . . 17
3231a1i 11 . . . . . . . . . . . . . . . 16
3326rpxrd 11365 . . . . . . . . . . . . . . . 16
3426rpge0d 11368 . . . . . . . . . . . . . . . 16
35 ubicc2 11775 . . . . . . . . . . . . . . . 16
3632, 33, 34, 35syl3anc 1292 . . . . . . . . . . . . . . 15
37 1rp 11329 . . . . . . . . . . . . . . . 16
38 1re 9660 . . . . . . . . . . . . . . . . . . . . 21
39 elicopnf 11755 . . . . . . . . . . . . . . . . . . . . 21
4038, 39mp1i 13 . . . . . . . . . . . . . . . . . . . 20
4140simprbda 635 . . . . . . . . . . . . . . . . . . 19
42 0red 9662 . . . . . . . . . . . . . . . . . . . 20
4338a1i 11 . . . . . . . . . . . . . . . . . . . 20
44 0lt1 10157 . . . . . . . . . . . . . . . . . . . . 21
4544a1i 11 . . . . . . . . . . . . . . . . . . . 20
4640simplbda 636 . . . . . . . . . . . . . . . . . . . 20
4742, 43, 41, 45, 46ltletrd 9812 . . . . . . . . . . . . . . . . . . 19
4841, 47elrpd 11361 . . . . . . . . . . . . . . . . . 18
49 pntlem3.A . . . . . . . . . . . . . . . . . . 19
5049adantr 472 . . . . . . . . . . . . . . . . . 18
51 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . 22
52 id 22 . . . . . . . . . . . . . . . . . . . . . 22
5351, 52oveq12d 6326 . . . . . . . . . . . . . . . . . . . . 21
5453fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20
5554breq1d 4405 . . . . . . . . . . . . . . . . . . 19
5655rspcv 3132 . . . . . . . . . . . . . . . . . 18
5748, 50, 56sylc 61 . . . . . . . . . . . . . . . . 17
5857ralrimiva 2809 . . . . . . . . . . . . . . . 16
59 oveq1 6315 . . . . . . . . . . . . . . . . . 18
6059raleqdv 2979 . . . . . . . . . . . . . . . . 17
6160rspcev 3136 . . . . . . . . . . . . . . . 16
6237, 58, 61sylancr 676 . . . . . . . . . . . . . . 15
63 breq2 4399 . . . . . . . . . . . . . . . . 17
6463rexralbidv 2898 . . . . . . . . . . . . . . . 16
6564, 22elrab2 3186 . . . . . . . . . . . . . . 15
6636, 62, 65sylanbrc 677 . . . . . . . . . . . . . 14
67 ne0i 3728 . . . . . . . . . . . . . 14
6866, 67syl 17 . . . . . . . . . . . . 13
69 elicc2 11724 . . . . . . . . . . . . . . . . . . . 20
7025, 27, 69sylancr 676 . . . . . . . . . . . . . . . . . . 19
7170biimpa 492 . . . . . . . . . . . . . . . . . 18
7271simp2d 1043 . . . . . . . . . . . . . . . . 17
7372a1d 25 . . . . . . . . . . . . . . . 16
7473ralrimiva 2809 . . . . . . . . . . . . . . 15
7522raleqi 2977 . . . . . . . . . . . . . . . 16
76 breq2 4399 . . . . . . . . . . . . . . . . 17
7776ralrab2 3192 . . . . . . . . . . . . . . . 16
7875, 77bitri 257 . . . . . . . . . . . . . . 15
7974, 78sylibr 217 . . . . . . . . . . . . . 14
80 breq1 4398 . . . . . . . . . . . . . . . 16
8180ralbidv 2829 . . . . . . . . . . . . . . 15
8281rspcev 3136 . . . . . . . . . . . . . 14
8325, 79, 82sylancr 676 . . . . . . . . . . . . 13
84 infrecl 10612 . . . . . . . . . . . . 13 inf
8530, 68, 83, 84syl3anc 1292 . . . . . . . . . . . 12 inf
8685recnd 9687 . . . . . . . . . . 11 inf
8786adantr 472 . . . . . . . . . 10 inf inf
88 elrp 11327 . . . . . . . . . . . . . 14 inf inf inf
8988biimpri 211 . . . . . . . . . . . . 13 inf inf inf
9085, 89sylan 479 . . . . . . . . . . . 12 inf inf
91 3z 10994 . . . . . . . . . . . 12
92 rpexpcl 12329 . . . . . . . . . . . 12 inf inf
9390, 91, 92sylancl 675 . . . . . . . . . . 11 inf inf
9410, 93rpmulcld 11380 . . . . . . . . . 10 inf inf
95 cncfi 22004 . . . . . . . . . 10 inf inf inf inf inf
9621, 87, 94, 95syl3anc 1292 . . . . . . . . 9 inf inf inf inf
9785ad2antrr 740 . . . . . . . . . . . . 13 inf inf
98 rphalfcl 11350 . . . . . . . . . . . . . 14
9998adantl 473 . . . . . . . . . . . . 13 inf
10097, 99ltaddrpd 11394 . . . . . . . . . . . 12 inf inf inf
10199rpred 11364 . . . . . . . . . . . . . 14 inf
10297, 101readdcld 9688 . . . . . . . . . . . . 13 inf inf
10397, 102ltnled 9799 . . . . . . . . . . . 12 inf inf inf inf inf
104100, 103mpbid 215 . . . . . . . . . . 11 inf inf inf
105 ax-resscn 9614 . . . . . . . . . . . . . . 15
10630, 105syl6ss 3430 . . . . . . . . . . . . . 14
107106ad2antrr 740 . . . . . . . . . . . . 13 inf
108 ssralv 3479 . . . . . . . . . . . . 13 inf inf inf inf inf inf
109107, 108syl 17 . . . . . . . . . . . 12 inf inf inf inf inf inf inf
11030ad2antrr 740 . . . . . . . . . . . . . . . . . . 19 inf
111110sselda 3418 . . . . . . . . . . . . . . . . . 18 inf
112102adantr 472 . . . . . . . . . . . . . . . . . 18 inf inf
113111, 112ltnled 9799 . . . . . . . . . . . . . . . . 17 inf inf inf
11485ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . 21 inf inf
115101adantr 472 . . . . . . . . . . . . . . . . . . . . 21 inf
116114, 115resubcld 10068 . . . . . . . . . . . . . . . . . . . 20 inf inf
11797, 99ltsubrpd 11393 . . . . . . . . . . . . . . . . . . . . 21 inf inf inf
118117adantr 472 . . . . . . . . . . . . . . . . . . . 20 inf inf inf
11930ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . 21 inf
12083ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . 21 inf
121 simpr 468 . . . . . . . . . . . . . . . . . . . . 21 inf
122 infrelb 10618 . . . . . . . . . . . . . . . . . . . . 21 inf
123119, 120, 121, 122syl3anc 1292 . . . . . . . . . . . . . . . . . . . 20 inf inf
124116, 114, 111, 118, 123ltletrd 9812 . . . . . . . . . . . . . . . . . . 19 inf inf
125111, 114, 115absdifltd 13572 . . . . . . . . . . . . . . . . . . . 20 inf inf inf inf
126125biimprd 231 . . . . . . . . . . . . . . . . . . 19 inf inf inf inf
127124, 126mpand 689 . . . . . . . . . . . . . . . . . 18 inf inf inf
128 rphalflt 11352 . . . . . . . . . . . . . . . . . . . 20
129128ad2antlr 741 . . . . . . . . . . . . . . . . . . 19 inf
130111, 114resubcld 10068 . . . . . . . . . . . . . . . . . . . . . 22 inf inf
131130recnd 9687 . . . . . . . . . . . . . . . . . . . . 21 inf inf
132131abscld 13575 . . . . . . . . . . . . . . . . . . . 20 inf inf
133 rpre 11331 . . . . . . . . . . . . . . . . . . . . 21
134133ad2antlr 741 . . . . . . . . . . . . . . . . . . . 20 inf
135 lttr 9728 . . . . . . . . . . . . . . . . . . . 20 inf inf inf
136132, 115, 134, 135syl3anc 1292 . . . . . . . . . . . . . . . . . . 19 inf inf inf
137129, 136mpan2d 688 . . . . . . . . . . . . . . . . . 18 inf inf inf
138127, 137syld 44 . . . . . . . . . . . . . . . . 17 inf inf inf
139113, 138sylbird 243 . . . . . . . . . . . . . . . 16 inf inf inf
140139con1d 129 . . . . . . . . . . . . . . 15 inf inf inf
141111recnd 9687 . . . . . . . . . . . . . . . . . . . 20 inf
142 id 22 . . . . . . . . . . . . . . . . . . . . . 22
143 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . 23
144143oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . 22
145142, 144oveq12d 6326 . . . . . . . . . . . . . . . . . . . . 21
146 eqid 2471 . . . . . . . . . . . . . . . . . . . . 21
147 ovex 6336 . . . . . . . . . . . . . . . . . . . . 21
148145, 146, 147fvmpt 5963 . . . . . . . . . . . . . . . . . . . 20
149141, 148syl 17 . . . . . . . . . . . . . . . . . . 19 inf
15087ad2antrr 740 . . . . . . . . . . . . . . . . . . . 20 inf inf
151 id 22 . . . . . . . . . . . . . . . . . . . . . 22 inf inf
152 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . 23 inf inf
153152oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . 22 inf inf
154151, 153oveq12d 6326 . . . . . . . . . . . . . . . . . . . . 21 inf inf inf
155 ovex 6336 . . . . . . . . . . . . . . . . . . . . 21 inf inf
156154, 146, 155fvmpt 5963 . . . . . . . . . . . . . . . . . . . 20 inf inf inf inf
157150, 156syl 17 . . . . . . . . . . . . . . . . . . 19 inf inf inf inf
158149, 157oveq12d 6326 . . . . . . . . . . . . . . . . . 18 inf inf inf inf
159158fveq2d 5883 . . . . . . . . . . . . . . . . 17 inf inf inf inf
160159breq1d 4405 . . . . . . . . . . . . . . . 16 inf inf inf inf inf inf
1619rpred 11364 . . . . . . . . . . . . . . . . . . . . 21
162161ad3antrrr 744 . . . . . . . . . . . . . . . . . . . 20 inf
163 reexpcl 12327 . . . . . . . . . . . . . . . . . . . . 21
164111, 15, 163sylancl 675 . . . . . . . . . . . . . . . . . . . 20 inf
165162, 164remulcld 9689 . . . . . . . . . . . . . . . . . . 19 inf
166111, 165resubcld 10068 . . . . . . . . . . . . . . . . . 18 inf
16715a1i 11 . . . . . . . . . . . . . . . . . . . . 21 inf
168114, 167reexpcld 12471 . . . . . . . . . . . . . . . . . . . 20 inf inf
169162, 168remulcld 9689 . . . . . . . . . . . . . . . . . . 19 inf inf
170114, 169resubcld 10068 . . . . . . . . . . . . . . . . . 18 inf inf inf
171166, 170, 169absdifltd 13572 . . . . . . . . . . . . . . . . 17 inf inf inf inf inf inf inf inf inf inf
172169recnd 9687 . . . . . . . . . . . . . . . . . . . . 21 inf inf
173150, 172npcand 10009 . . . . . . . . . . . . . . . . . . . 20 inf inf inf inf inf
174173breq2d 4407 . . . . . . . . . . . . . . . . . . 19 inf inf inf inf inf
175 pntlem3.3 . . . . . . . . . . . . . . . . . . . . . . 23
176175ad4ant14 1259 . . . . . . . . . . . . . . . . . . . . . 22 inf
177 infrelb 10618 . . . . . . . . . . . . . . . . . . . . . 22 inf
178119, 120, 176, 177syl3anc 1292 . . . . . . . . . . . . . . . . . . . . 21 inf inf
179114, 166, 178lensymd 9803 . . . . . . . . . . . . . . . . . . . 20 inf inf
180179pm2.21d 109 . . . . . . . . . . . . . . . . . . 19 inf inf inf
181174, 180sylbid 223 . . . . . . . . . . . . . . . . . 18 inf inf inf inf inf
182181adantld 474 . . . . . . . . . . . . . . . . 17 inf inf inf inf inf inf inf inf
183171, 182sylbid 223 . . . . . . . . . . . . . . . 16 inf inf inf inf inf
184160, 183sylbid 223 . . . . . . . . . . . . . . 15 inf inf inf inf
185140, 184jad 167 . . . . . . . . . . . . . 14 inf inf inf inf inf
186185ralimdva 2805 . . . . . . . . . . . . 13 inf inf inf inf inf
18768ad2antrr 740 . . . . . . . . . . . . . 14 inf
18883ad2antrr 740 . . . . . . . . . . . . . 14 inf
189 infregelb 10616 . . . . . . . . . . . . . 14 inf inf inf inf
190110, 187, 188, 102, 189syl31anc 1295 . . . . . . . . . . . . 13 inf inf inf inf
191186, 190sylibrd 242 . . . . . . . . . . . 12 inf inf inf inf inf inf
192109, 191syld 44 . . . . . . . . . . 11 inf inf inf inf inf inf
193104, 192mtod 182 . . . . . . . . . 10 inf inf inf inf
194193nrexdv 2842 . . . . . . . . 9 inf inf inf inf
19596, 194pm2.65da 586 . . . . . . . 8 inf
196195adantr 472 . . . . . . 7 inf
19730adantr 472 . . . . . . . . . 10
19868adantr 472 . . . . . . . . . 10
19983adantr 472 . . . . . . . . . 10
200133adantl 473 . . . . . . . . . 10
201 infregelb 10616 . . . . . . . . . 10 inf
202197, 198, 199, 200, 201syl31anc 1295 . . . . . . . . 9 inf
20322raleqi 2977 . . . . . . . . . 10
204 breq2 4399 . . . . . . . . . . 11
205204ralrab2 3192 . . . . . . . . . 10
206203, 205bitri 257 . . . . . . . . 9
207202, 206syl6bb 269 . . . . . . . 8 inf
208 rpgt0 11336 . . . . . . . . . 10
209208adantl 473 . . . . . . . . 9
210 0red 9662 . . . . . . . . . 10
21185adantr 472 . . . . . . . . . 10 inf
212 ltletr 9743 . . . . . . . . . 10 inf inf inf
213210, 200, 211, 212syl3anc 1292 . . . . . . . . 9 inf inf
214209, 213mpand 689 . . . . . . . 8 inf inf
215207, 214sylbird 243 . . . . . . 7 inf
216196, 215mtod 182 . . . . . 6
217 rexanali 2839 . . . . . 6
218216, 217sylibr 217 . . . . 5
219 fveq2 5879 . . . . . . . . . . . . . . 15
220 id 22 . . . . . . . . . . . . . . 15
221219, 220oveq12d 6326 . . . . . . . . . . . . . 14
222221fveq2d 5883 . . . . . . . . . . . . 13
223222breq1d 4405 . . . . . . . . . . . 12
224223cbvralv 3005 . . . . . . . . . . 11
225 rpre 11331 . . . . . . . . . . . . . . . . 17
226225ad2antll 743 . . . . . . . . . . . . . . . 16
227 simprl 772 . . . . . . . . . . . . . . . 16
228 simplr 770 . . . . . . . . . . . . . . . . . 18
229228rpred 11364 . . . . . . . . . . . . . . . . 17
230 elicopnf 11755 . . . . . . . . . . . . . . . . 17
231229, 230syl 17 . . . . . . . . . . . . . . . 16
232226, 227, 231mpbir2and 936 . . . . . . . . . . . . . . 15
233 pntlem3.r . . . . . . . . . . . . . . . . . . . . . 22 ψ
234233pntrval 24479 . . . . . . . . . . . . . . . . . . . . 21 ψ
235234ad2antll 743 . . . . . . . . . . . . . . . . . . . 20 ψ
236235oveq1d 6323 . . . . . . . . . . . . . . . . . . 19 ψ
237 chpcl 24130 . . . . . . . . . . . . . . . . . . . . . 22 ψ
238226, 237syl 17 . . . . . . . . . . . . . . . . . . . . 21 ψ
239238recnd 9687 . . . . . . . . . . . . . . . . . . . 20 ψ
240 rpcn 11333 . . . . . . . . . . . . . . . . . . . . 21
241240ad2antll 743 . . . . . . . . . . . . . . . . . . . 20
242 rpne0 11340 . . . . . . . . . . . . . . . . . . . . 21
243242ad2antll 743 . . . . . . . . . . . . . . . . . . . 20
244239, 241, 241, 243divsubdird 10444 . . . . . . . . . . . . . . . . . . 19 ψ ψ
245241, 243dividd 10403 . . . . . . . . . . . . . . . . . . . 20
246245oveq2d 6324 . . . . . . . . . . . . . . . . . . 19 ψ ψ
247236, 244, 2463eqtrrd 2510 . . . . . . . . . . . . . . . . . 18 ψ
248247fveq2d 5883 . . . . . . . . . . . . . . . . 17 ψ
249248breq1d 4405 . . . . . . . . . . . . . . . 16 ψ
250 simprr 774 . . . . . . . . . . . . . . . . . . 19
251250ad2antrr 740 . . . . . . . . . . . . . . . . . 18
25229ad2antrr 740 . . . . . . . . . . . . . . . . . . . . 21
253252ad2antrr 740 . . . . . . . . . . . . . . . . . . . 20
254 simplrl 778 . . . . . . . . . . . . . . . . . . . . 21
255254adantr 472 . . . . . . . . . . . . . . . . . . . 20
256253, 255sseldd 3419 . . . . . . . . . . . . . . . . . . 19
257 simp-4r 785 . . . . . . . . . . . . . . . . . . . 20
258257rpred 11364 . . . . . . . . . . . . . . . . . . 19
259256, 258ltnled 9799 . . . . . . . . . . . . . . . . . 18
260251, 259mpbird 240 . . . . . . . . . . . . . . . . 17
261225, 237syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ψ
262 rerpdivcl 11353 . . . . . . . . . . . . . . . . . . . . . . 23 ψ ψ
263261, 262mpancom 682 . . . . . . . . . . . . . . . . . . . . . 22 ψ
264263ad2antll 743 . . . . . . . . . . . . . . . . . . . . 21 ψ
265 resubcl 9958 . . . . . . . . . . . . . . . . . . . . 21 ψ ψ
266264, 38, 265sylancl 675 . . . . . . . . . . . . . . . . . . . 20 ψ
267266recnd 9687 . . . . . . . . . . . . . . . . . . 19 ψ
268267abscld 13575 . . . . . . . . . . . . . . . . . 18 ψ
269 lelttr 9742 . . . . . . . . . . . . . . . . . 18 ψ ψ ψ
270268, 256, 258, 269syl3anc 1292 . . . . . . . . . . . . . . . . 17 ψ ψ
271260, 270mpan2d 688 . . . . . . . . . . . . . . . 16 ψ ψ
272249, 271sylbird 243 . . . . . . . . . . . . . . 15 ψ
273232, 272embantd 55 . . . . . . . . . . . . . 14 ψ
274273exp32 616 . . . . . . . . . . . . 13 ψ
275274com24 89 . . . . . . . . . . . 12 ψ
276275ralimdv2 2804 . . . . . . . . . . 11 ψ
277224, 276syl5bi 225 . . . . . . . . . 10 ψ
278277reximdva 2858 . . . . . . . . 9 ψ
279278anassrs 660 . . . . . . . 8 ψ
280279impancom 447 . . . . . . 7 ψ
281280expimpd 614 . . . . . 6 ψ
282281rexlimdva 2871 . . . . 5 ψ
283218, 282mpd 15 . . . 4 ψ
284 ssrexv 3480 . . . 4 ψ ψ
2851, 283, 284mpsyl 64 . . 3 ψ
286285ralrimiva 2809 . 2 ψ
287263recnd 9687 . . . . 5 ψ
288287rgen 2766 . . . 4 ψ
289288a1i 11 . . 3 ψ
2901a1i 11 . . 3
291 1cnd 9677 . . 3
292289, 290, 291rlim2 13637 . 2 ψ ψ
293286, 292mpbird 240 1 ψ
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wa 376   w3a 1007   wceq 1452   wcel 1904   wne 2641  wral 2756  wrex 2757  crab 2760   wss 3390  c0 3722   class class class wbr 4395   cmpt 4454  cfv 5589  (class class class)co 6308  infcinf 7973  cc 9555  cr 9556  cc0 9557  c1 9558   caddc 9560   cmul 9562   cpnf 9690  cxr 9692   clt 9693   cle 9694   cmin 9880   cdiv 10291  c2 10681  c3 10682  cn0 10893  cz 10961  crp 11325  cico 11662  cicc 11663  cexp 12310  cabs 13374   crli 13626  ctopn 15398  ℂfldccnfld 19047   ccn 20317   ctx 20652  ccncf 21986  ψ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-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:  pntleml  24528
 Copyright terms: Public domain W3C validator