Metamath Proof Explorer


Theorem pntlem3

Description: Lemma for pnt . Equation 10.6.35 in Shapiro, p. 436. (Contributed by Mario Carneiro, 8-Apr-2016) (Proof shortened by AV, 27-Sep-2020)

Ref Expression
Hypotheses pntlem3.r R = a + ψ a a
pntlem3.a φ A +
pntlem3.A φ x + R x x A
pntlem3.1 T = t 0 A | y + z y +∞ R z z t
pntlem3.2 φ C +
pntlem3.3 φ u T u C u 3 T
Assertion pntlem3 φ x + ψ x x 1

Proof

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