Step |
Hyp |
Ref |
Expression |
1 |
|
pntlem3.r |
|
2 |
|
pntlem3.a |
|
3 |
|
pntlem3.A |
|
4 |
|
pntlem3.1 |
|
5 |
|
pntlem3.2 |
|
6 |
|
pntlem3.3 |
|
7 |
|
rpssre |
|
8 |
|
eqid |
|
9 |
8
|
subcn |
|
10 |
9
|
a1i |
|
11 |
|
ssid |
|
12 |
|
cncfmptid |
|
13 |
11 11 12
|
mp2an |
|
14 |
13
|
a1i |
|
15 |
5
|
adantr |
|
16 |
15
|
rpcnd |
|
17 |
11
|
a1i |
|
18 |
|
cncfmptc |
|
19 |
16 17 17 18
|
syl3anc |
|
20 |
|
3nn0 |
|
21 |
8
|
expcn |
|
22 |
20 21
|
mp1i |
|
23 |
8
|
cncfcn1 |
|
24 |
22 23
|
eleqtrrdi |
|
25 |
19 24
|
mulcncf |
|
26 |
8 10 14 25
|
cncfmpt2f |
|
27 |
4
|
ssrab3 |
|
28 |
|
0re |
|
29 |
2
|
rpred |
|
30 |
|
iccssre |
|
31 |
28 29 30
|
sylancr |
|
32 |
27 31
|
sstrid |
|
33 |
|
0xr |
|
34 |
2
|
rpxrd |
|
35 |
2
|
rpge0d |
|
36 |
|
ubicc2 |
|
37 |
33 34 35 36
|
mp3an2i |
|
38 |
|
1rp |
|
39 |
|
fveq2 |
|
40 |
|
id |
|
41 |
39 40
|
oveq12d |
|
42 |
41
|
fveq2d |
|
43 |
42
|
breq1d |
|
44 |
3
|
adantr |
|
45 |
|
1re |
|
46 |
|
elicopnf |
|
47 |
45 46
|
mp1i |
|
48 |
47
|
simprbda |
|
49 |
|
0red |
|
50 |
45
|
a1i |
|
51 |
|
0lt1 |
|
52 |
51
|
a1i |
|
53 |
47
|
simplbda |
|
54 |
49 50 48 52 53
|
ltletrd |
|
55 |
48 54
|
elrpd |
|
56 |
43 44 55
|
rspcdva |
|
57 |
56
|
ralrimiva |
|
58 |
|
oveq1 |
|
59 |
58
|
raleqdv |
|
60 |
59
|
rspcev |
|
61 |
38 57 60
|
sylancr |
|
62 |
|
breq2 |
|
63 |
62
|
rexralbidv |
|
64 |
63 4
|
elrab2 |
|
65 |
37 61 64
|
sylanbrc |
|
66 |
65
|
ne0d |
|
67 |
|
elicc2 |
|
68 |
28 29 67
|
sylancr |
|
69 |
68
|
biimpa |
|
70 |
69
|
simp2d |
|
71 |
70
|
a1d |
|
72 |
71
|
ralrimiva |
|
73 |
4
|
raleqi |
|
74 |
|
breq2 |
|
75 |
74
|
ralrab2 |
|
76 |
73 75
|
bitri |
|
77 |
72 76
|
sylibr |
|
78 |
|
breq1 |
|
79 |
78
|
ralbidv |
|
80 |
79
|
rspcev |
|
81 |
28 77 80
|
sylancr |
|
82 |
|
infrecl |
|
83 |
32 66 81 82
|
syl3anc |
|
84 |
83
|
recnd |
|
85 |
84
|
adantr |
|
86 |
|
elrp |
|
87 |
86
|
biimpri |
|
88 |
83 87
|
sylan |
|
89 |
|
3z |
|
90 |
|
rpexpcl |
|
91 |
88 89 90
|
sylancl |
|
92 |
15 91
|
rpmulcld |
|
93 |
|
cncfi |
|
94 |
26 85 92 93
|
syl3anc |
|
95 |
83
|
ad2antrr |
|
96 |
|
rphalfcl |
|
97 |
96
|
adantl |
|
98 |
95 97
|
ltaddrpd |
|
99 |
97
|
rpred |
|
100 |
95 99
|
readdcld |
|
101 |
95 100
|
ltnled |
|
102 |
98 101
|
mpbid |
|
103 |
|
ax-resscn |
|
104 |
32 103
|
sstrdi |
|
105 |
104
|
ad2antrr |
|
106 |
|
ssralv |
|
107 |
105 106
|
syl |
|
108 |
32
|
ad2antrr |
|
109 |
108
|
sselda |
|
110 |
100
|
adantr |
|
111 |
109 110
|
ltnled |
|
112 |
83
|
ad3antrrr |
|
113 |
99
|
adantr |
|
114 |
112 113
|
resubcld |
|
115 |
95 97
|
ltsubrpd |
|
116 |
115
|
adantr |
|
117 |
32
|
ad3antrrr |
|
118 |
81
|
ad3antrrr |
|
119 |
|
simpr |
|
120 |
|
infrelb |
|
121 |
117 118 119 120
|
syl3anc |
|
122 |
114 112 109 116 121
|
ltletrd |
|
123 |
109 112 113
|
absdifltd |
|
124 |
123
|
biimprd |
|
125 |
122 124
|
mpand |
|
126 |
|
rphalflt |
|
127 |
126
|
ad2antlr |
|
128 |
109 112
|
resubcld |
|
129 |
128
|
recnd |
|
130 |
129
|
abscld |
|
131 |
|
rpre |
|
132 |
131
|
ad2antlr |
|
133 |
|
lttr |
|
134 |
130 113 132 133
|
syl3anc |
|
135 |
127 134
|
mpan2d |
|
136 |
125 135
|
syld |
|
137 |
111 136
|
sylbird |
|
138 |
137
|
con1d |
|
139 |
109
|
recnd |
|
140 |
|
id |
|
141 |
|
oveq1 |
|
142 |
141
|
oveq2d |
|
143 |
140 142
|
oveq12d |
|
144 |
|
eqid |
|
145 |
|
ovex |
|
146 |
143 144 145
|
fvmpt |
|
147 |
139 146
|
syl |
|
148 |
85
|
ad2antrr |
|
149 |
|
id |
|
150 |
|
oveq1 |
|
151 |
150
|
oveq2d |
|
152 |
149 151
|
oveq12d |
|
153 |
|
ovex |
|
154 |
152 144 153
|
fvmpt |
|
155 |
148 154
|
syl |
|
156 |
147 155
|
oveq12d |
|
157 |
156
|
fveq2d |
|
158 |
157
|
breq1d |
|
159 |
5
|
rpred |
|
160 |
159
|
ad3antrrr |
|
161 |
|
reexpcl |
|
162 |
109 20 161
|
sylancl |
|
163 |
160 162
|
remulcld |
|
164 |
109 163
|
resubcld |
|
165 |
20
|
a1i |
|
166 |
112 165
|
reexpcld |
|
167 |
160 166
|
remulcld |
|
168 |
112 167
|
resubcld |
|
169 |
164 168 167
|
absdifltd |
|
170 |
167
|
recnd |
|
171 |
148 170
|
npcand |
|
172 |
171
|
breq2d |
|
173 |
6
|
ad4ant14 |
|
174 |
|
infrelb |
|
175 |
117 118 173 174
|
syl3anc |
|
176 |
112 164 175
|
lensymd |
|
177 |
176
|
pm2.21d |
|
178 |
172 177
|
sylbid |
|
179 |
178
|
adantld |
|
180 |
169 179
|
sylbid |
|
181 |
158 180
|
sylbid |
|
182 |
138 181
|
jad |
|
183 |
182
|
ralimdva |
|
184 |
66
|
ad2antrr |
|
185 |
81
|
ad2antrr |
|
186 |
|
infregelb |
|
187 |
108 184 185 100 186
|
syl31anc |
|
188 |
183 187
|
sylibrd |
|
189 |
107 188
|
syld |
|
190 |
102 189
|
mtod |
|
191 |
190
|
nrexdv |
|
192 |
94 191
|
pm2.65da |
|
193 |
192
|
adantr |
|
194 |
32
|
adantr |
|
195 |
66
|
adantr |
|
196 |
81
|
adantr |
|
197 |
131
|
adantl |
|
198 |
|
infregelb |
|
199 |
194 195 196 197 198
|
syl31anc |
|
200 |
4
|
raleqi |
|
201 |
|
breq2 |
|
202 |
201
|
ralrab2 |
|
203 |
200 202
|
bitri |
|
204 |
199 203
|
bitrdi |
|
205 |
|
rpgt0 |
|
206 |
205
|
adantl |
|
207 |
83
|
adantr |
|
208 |
|
ltletr |
|
209 |
28 197 207 208
|
mp3an2i |
|
210 |
206 209
|
mpand |
|
211 |
204 210
|
sylbird |
|
212 |
193 211
|
mtod |
|
213 |
|
rexanali |
|
214 |
212 213
|
sylibr |
|
215 |
|
fveq2 |
|
216 |
|
id |
|
217 |
215 216
|
oveq12d |
|
218 |
217
|
fveq2d |
|
219 |
218
|
breq1d |
|
220 |
219
|
cbvralvw |
|
221 |
|
rpre |
|
222 |
221
|
ad2antll |
|
223 |
|
simprl |
|
224 |
|
simplr |
|
225 |
224
|
rpred |
|
226 |
|
elicopnf |
|
227 |
225 226
|
syl |
|
228 |
222 223 227
|
mpbir2and |
|
229 |
1
|
pntrval |
|
230 |
229
|
ad2antll |
|
231 |
230
|
oveq1d |
|
232 |
|
chpcl |
|
233 |
222 232
|
syl |
|
234 |
233
|
recnd |
|
235 |
|
rpcn |
|
236 |
235
|
ad2antll |
|
237 |
|
rpne0 |
|
238 |
237
|
ad2antll |
|
239 |
234 236 236 238
|
divsubdird |
|
240 |
236 238
|
dividd |
|
241 |
240
|
oveq2d |
|
242 |
231 239 241
|
3eqtrrd |
|
243 |
242
|
fveq2d |
|
244 |
243
|
breq1d |
|
245 |
|
simprr |
|
246 |
245
|
ad2antrr |
|
247 |
31
|
ad2antrr |
|
248 |
247
|
ad2antrr |
|
249 |
|
simplrl |
|
250 |
249
|
adantr |
|
251 |
248 250
|
sseldd |
|
252 |
|
simp-4r |
|
253 |
252
|
rpred |
|
254 |
251 253
|
ltnled |
|
255 |
246 254
|
mpbird |
|
256 |
221 232
|
syl |
|
257 |
|
rerpdivcl |
|
258 |
256 257
|
mpancom |
|
259 |
258
|
ad2antll |
|
260 |
|
resubcl |
|
261 |
259 45 260
|
sylancl |
|
262 |
261
|
recnd |
|
263 |
262
|
abscld |
|
264 |
|
lelttr |
|
265 |
263 251 253 264
|
syl3anc |
|
266 |
255 265
|
mpan2d |
|
267 |
244 266
|
sylbird |
|
268 |
228 267
|
embantd |
|
269 |
268
|
exp32 |
|
270 |
269
|
com24 |
|
271 |
270
|
ralimdv2 |
|
272 |
220 271
|
syl5bi |
|
273 |
272
|
reximdva |
|
274 |
273
|
anassrs |
|
275 |
274
|
impancom |
|
276 |
275
|
expimpd |
|
277 |
276
|
rexlimdva |
|
278 |
214 277
|
mpd |
|
279 |
|
ssrexv |
|
280 |
7 278 279
|
mpsyl |
|
281 |
280
|
ralrimiva |
|
282 |
258
|
recnd |
|
283 |
282
|
rgen |
|
284 |
283
|
a1i |
|
285 |
7
|
a1i |
|
286 |
|
1cnd |
|
287 |
284 285 286
|
rlim2 |
|
288 |
281 287
|
mpbird |
|