Metamath Proof Explorer


Theorem limclner

Description: For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses limclner.k K = TopOpen fld
limclner.a φ A
limclner.j J = topGen ran .
limclner.f φ F : A
limclner.blp1 φ B limPt J A −∞ B
limclner.blp2 φ B limPt J A B +∞
limclner.l φ L F −∞ B lim B
limclner.r φ R F B +∞ lim B
limclner.lner φ L R
Assertion limclner φ F lim B =

Proof

Step Hyp Ref Expression
1 limclner.k K = TopOpen fld
2 limclner.a φ A
3 limclner.j J = topGen ran .
4 limclner.f φ F : A
5 limclner.blp1 φ B limPt J A −∞ B
6 limclner.blp2 φ B limPt J A B +∞
7 limclner.l φ L F −∞ B lim B
8 limclner.r φ R F B +∞ lim B
9 limclner.lner φ L R
10 limccl F B +∞ lim B
11 10 8 sseldi φ R
12 11 ad2antrr φ x y + z + w A w B w B < z F w x < y R
13 limccl F −∞ B lim B
14 13 7 sseldi φ L
15 14 ad2antrr φ x y + z + w A w B w B < z F w x < y L
16 12 15 subcld φ x y + z + w A w B w B < z F w x < y R L
17 9 necomd φ R L
18 17 ad2antrr φ x y + z + w A w B w B < z F w x < y R L
19 12 15 18 subne0d φ x y + z + w A w B w B < z F w x < y R L 0
20 16 19 absrpcld φ x y + z + w A w B w B < z F w x < y R L +
21 4re 4
22 4pos 0 < 4
23 21 22 elrpii 4 +
24 23 a1i φ x y + z + w A w B w B < z F w x < y 4 +
25 20 24 rpdivcld φ x y + z + w A w B w B < z F w x < y R L 4 +
26 nfv y φ x
27 nfra1 y y + z + w A w B w B < z F w x < y
28 26 27 nfan y φ x y + z + w A w B w B < z F w x < y
29 nfv y R L 4 + a A b A R L < 4 R L 4
30 28 29 nfim y φ x y + z + w A w B w B < z F w x < y R L 4 + a A b A R L < 4 R L 4
31 ovex R L 4 V
32 eleq1 y = R L 4 y + R L 4 +
33 oveq2 y = R L 4 4 y = 4 R L 4
34 33 breq2d y = R L 4 R L < 4 y R L < 4 R L 4
35 34 2rexbidv y = R L 4 a A b A R L < 4 y a A b A R L < 4 R L 4
36 32 35 imbi12d y = R L 4 y + a A b A R L < 4 y R L 4 + a A b A R L < 4 R L 4
37 36 imbi2d y = R L 4 φ x y + z + w A w B w B < z F w x < y y + a A b A R L < 4 y φ x y + z + w A w B w B < z F w x < y R L 4 + a A b A R L < 4 R L 4
38 simpll φ x y + z + w A w B w B < z F w x < y y + φ x
39 simpr φ x y + z + w A w B w B < z F w x < y y + y +
40 rspa y + z + w A w B w B < z F w x < y y + z + w A w B w B < z F w x < y
41 40 adantll φ x y + z + w A w B w B < z F w x < y y + z + w A w B w B < z F w x < y
42 fresin F : A F B +∞ : A B +∞
43 4 42 syl φ F B +∞ : A B +∞
44 inss2 A B +∞ B +∞
45 ioosscn B +∞
46 44 45 sstri A B +∞
47 46 a1i φ A B +∞
48 retop topGen ran . Top
49 3 48 eqeltri J Top
50 inss2 A −∞ B −∞ B
51 ioossre −∞ B
52 50 51 sstri A −∞ B
53 uniretop = topGen ran .
54 3 unieqi J = topGen ran .
55 53 54 eqtr4i = J
56 55 lpss J Top A −∞ B limPt J A −∞ B
57 49 52 56 mp2an limPt J A −∞ B
58 57 5 sseldi φ B
59 58 recnd φ B
60 43 47 59 ellimc3 φ R F B +∞ lim B R y + v + w A B +∞ w B w B < v F B +∞ w R < y
61 8 60 mpbid φ R y + v + w A B +∞ w B w B < v F B +∞ w R < y
62 61 simprd φ y + v + w A B +∞ w B w B < v F B +∞ w R < y
63 62 r19.21bi φ y + v + w A B +∞ w B w B < v F B +∞ w R < y
64 63 3ad2ant1 φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y
65 simp11l φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y φ
66 simp12 φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y z +
67 simp2 φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y v +
68 breq2 u = if z v z v b B < u b B < if z v z v
69 68 rexbidv u = if z v z v b A B +∞ B b B < u b A B +∞ B b B < if z v z v
70 inss1 limPt K A B +∞ limPt K A B +∞
71 70 a1i φ limPt K A B +∞ limPt K A B +∞
72 1 cnfldtop K Top
73 72 a1i φ K Top
74 ax-resscn
75 74 a1i φ
76 ioossre B +∞
77 44 76 sstri A B +∞
78 77 a1i φ A B +∞
79 unicntop = TopOpen fld
80 1 unieqi K = TopOpen fld
81 79 80 eqtr4i = K
82 1 tgioo2 topGen ran . = K 𝑡
83 3 82 eqtri J = K 𝑡
84 81 83 restlp K Top A B +∞ limPt J A B +∞ = limPt K A B +∞
85 73 75 78 84 syl3anc φ limPt J A B +∞ = limPt K A B +∞
86 1 eqcomi TopOpen fld = K
87 86 fveq2i limPt TopOpen fld = limPt K
88 87 fveq1i limPt TopOpen fld A B +∞ = limPt K A B +∞
89 88 a1i φ limPt TopOpen fld A B +∞ = limPt K A B +∞
90 71 85 89 3sstr4d φ limPt J A B +∞ limPt TopOpen fld A B +∞
91 90 6 sseldd φ B limPt TopOpen fld A B +∞
92 47 59 islpcn φ B limPt TopOpen fld A B +∞ u + b A B +∞ B b B < u
93 91 92 mpbid φ u + b A B +∞ B b B < u
94 93 3ad2ant1 φ z + v + u + b A B +∞ B b B < u
95 ifcl z + v + if z v z v +
96 95 3adant1 φ z + v + if z v z v +
97 69 94 96 rspcdva φ z + v + b A B +∞ B b B < if z v z v
98 eldifi b A B +∞ B b A B +∞
99 77 98 sseldi b A B +∞ B b
100 75 sselda φ b b
101 59 adantr φ b B
102 100 101 subcld φ b b B
103 102 abscld φ b b B
104 103 3ad2antl1 φ z + v + b b B
105 104 adantr φ z + v + b b B < if z v z v b B
106 96 rpred φ z + v + if z v z v
107 106 ad2antrr φ z + v + b b B < if z v z v if z v z v
108 rpre z + z
109 108 3ad2ant2 φ z + v + z
110 109 ad2antrr φ z + v + b b B < if z v z v z
111 simpr φ z + v + b b B < if z v z v b B < if z v z v
112 rpre v + v
113 min1 z v if z v z v z
114 108 112 113 syl2an z + v + if z v z v z
115 114 3adant1 φ z + v + if z v z v z
116 115 ad2antrr φ z + v + b b B < if z v z v if z v z v z
117 105 107 110 111 116 ltletrd φ z + v + b b B < if z v z v b B < z
118 112 3ad2ant3 φ z + v + v
119 118 ad2antrr φ z + v + b b B < if z v z v v
120 110 119 min2d φ z + v + b b B < if z v z v if z v z v v
121 105 107 119 111 120 ltletrd φ z + v + b b B < if z v z v b B < v
122 117 121 jca φ z + v + b b B < if z v z v b B < z b B < v
123 122 ex φ z + v + b b B < if z v z v b B < z b B < v
124 99 123 sylan2 φ z + v + b A B +∞ B b B < if z v z v b B < z b B < v
125 124 reximdva φ z + v + b A B +∞ B b B < if z v z v b A B +∞ B b B < z b B < v
126 97 125 mpd φ z + v + b A B +∞ B b B < z b B < v
127 65 66 67 126 syl3anc φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y b A B +∞ B b B < z b B < v
128 nfv b φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y
129 nfre1 b b A F b x < y F b R < y
130 98 elin1d b A B +∞ B b A
131 130 3ad2ant2 φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y b A B +∞ B b B < z b B < v b A
132 simp113 φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y b A B +∞ B b B < z b B < v w A w B w B < z F w x < y
133 eldifsni b A B +∞ B b B
134 133 adantr b A B +∞ B b B < z b B < v b B
135 simprl b A B +∞ B b B < z b B < v b B < z
136 134 135 jca b A B +∞ B b B < z b B < v b B b B < z
137 136 3adant1 φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y b A B +∞ B b B < z b B < v b B b B < z
138 neeq1 w = b w B b B
139 fvoveq1 w = b w B = b B
140 139 breq1d w = b w B < z b B < z
141 138 140 anbi12d w = b w B w B < z b B b B < z
142 141 imbrov2fvoveq w = b w B w B < z F w x < y b B b B < z F b x < y
143 142 rspcva b A w A w B w B < z F w x < y b B b B < z F b x < y
144 143 imp b A w A w B w B < z F w x < y b B b B < z F b x < y
145 131 132 137 144 syl21anc φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y b A B +∞ B b B < z b B < v F b x < y
146 98 3ad2ant2 φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y b A B +∞ B b B < z b B < v b A B +∞
147 65 3ad2ant1 φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y b A B +∞ B b B < z b B < v φ
148 simp13 φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y b A B +∞ B b B < z b B < v w A B +∞ w B w B < v F B +∞ w R < y
149 nfv w φ
150 nfra1 w w A B +∞ w B w B < v F B +∞ w R < y
151 149 150 nfan w φ w A B +∞ w B w B < v F B +∞ w R < y
152 elinel2 w A B +∞ w B +∞
153 152 fvresd w A B +∞ F B +∞ w = F w
154 153 eqcomd w A B +∞ F w = F B +∞ w
155 154 fvoveq1d w A B +∞ F w R = F B +∞ w R
156 155 3ad2ant2 φ w A B +∞ w B w B < v F B +∞ w R < y w A B +∞ w B w B < v F w R = F B +∞ w R
157 rspa w A B +∞ w B w B < v F B +∞ w R < y w A B +∞ w B w B < v F B +∞ w R < y
158 157 3impia w A B +∞ w B w B < v F B +∞ w R < y w A B +∞ w B w B < v F B +∞ w R < y
159 158 3adant1l φ w A B +∞ w B w B < v F B +∞ w R < y w A B +∞ w B w B < v F B +∞ w R < y
160 156 159 eqbrtrd φ w A B +∞ w B w B < v F B +∞ w R < y w A B +∞ w B w B < v F w R < y
161 160 3exp φ w A B +∞ w B w B < v F B +∞ w R < y w A B +∞ w B w B < v F w R < y
162 151 161 ralrimi φ w A B +∞ w B w B < v F B +∞ w R < y w A B +∞ w B w B < v F w R < y
163 147 148 162 syl2anc φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y b A B +∞ B b B < z b B < v w A B +∞ w B w B < v F w R < y
164 133 anim1i b A B +∞ B b B < v b B b B < v
165 164 adantrl b A B +∞ B b B < z b B < v b B b B < v
166 165 3adant1 φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y b A B +∞ B b B < z b B < v b B b B < v
167 139 breq1d w = b w B < v b B < v
168 138 167 anbi12d w = b w B w B < v b B b B < v
169 168 imbrov2fvoveq w = b w B w B < v F w R < y b B b B < v F b R < y
170 169 rspcva b A B +∞ w A B +∞ w B w B < v F w R < y b B b B < v F b R < y
171 170 imp b A B +∞ w A B +∞ w B w B < v F w R < y b B b B < v F b R < y
172 146 163 166 171 syl21anc φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y b A B +∞ B b B < z b B < v F b R < y
173 rspe b A F b x < y F b R < y b A F b x < y F b R < y
174 131 145 172 173 syl12anc φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y b A B +∞ B b B < z b B < v b A F b x < y F b R < y
175 174 3exp φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y b A B +∞ B b B < z b B < v b A F b x < y F b R < y
176 128 129 175 rexlimd φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y b A B +∞ B b B < z b B < v b A F b x < y F b R < y
177 127 176 mpd φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y b A F b x < y F b R < y
178 177 3exp φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y b A F b x < y F b R < y
179 178 rexlimdv φ y + z + w A w B w B < z F w x < y v + w A B +∞ w B w B < v F B +∞ w R < y b A F b x < y F b R < y
180 64 179 mpd φ y + z + w A w B w B < z F w x < y b A F b x < y F b R < y
181 180 3exp φ y + z + w A w B w B < z F w x < y b A F b x < y F b R < y
182 181 rexlimdv φ y + z + w A w B w B < z F w x < y b A F b x < y F b R < y
183 182 imp φ y + z + w A w B w B < z F w x < y b A F b x < y F b R < y
184 183 adantllr φ x y + z + w A w B w B < z F w x < y b A F b x < y F b R < y
185 184 ad2antrr φ x y + z + w A w B w B < z F w x < y a A F a x < y F a L < y b A F b x < y F b R < y
186 11 ad6antr φ x y + a A F a x < y F a L < y b A F b x < y F b R < y R
187 14 ad6antr φ x y + a A F a x < y F a L < y b A F b x < y F b R < y L
188 186 187 subcld φ x y + a A F a x < y F a L < y b A F b x < y F b R < y R L
189 188 abscld φ x y + a A F a x < y F a L < y b A F b x < y F b R < y R L
190 simp-6l φ x y + a A F a x < y F a L < y b A F b x < y F b R < y φ
191 simplr φ x y + a A F a x < y F a L < y b A F b x < y F b R < y b A
192 4 ffvelrnda φ b A F b
193 190 191 192 syl2anc φ x y + a A F a x < y F a L < y b A F b x < y F b R < y F b
194 186 193 subcld φ x y + a A F a x < y F a L < y b A F b x < y F b R < y R F b
195 194 abscld φ x y + a A F a x < y F a L < y b A F b x < y F b R < y R F b
196 simp-6r φ x y + a A F a x < y F a L < y b A F b x < y F b R < y x
197 193 196 subcld φ x y + a A F a x < y F a L < y b A F b x < y F b R < y F b x
198 197 abscld φ x y + a A F a x < y F a L < y b A F b x < y F b R < y F b x
199 195 198 readdcld φ x y + a A F a x < y F a L < y b A F b x < y F b R < y R F b + F b x
200 simp-4r φ x y + a A F a x < y F a L < y b A F b x < y F b R < y a A
201 4 ffvelrnda φ a A F a
202 190 200 201 syl2anc φ x y + a A F a x < y F a L < y b A F b x < y F b R < y F a
203 196 202 subcld φ x y + a A F a x < y F a L < y b A F b x < y F b R < y x F a
204 203 abscld φ x y + a A F a x < y F a L < y b A F b x < y F b R < y x F a
205 199 204 readdcld φ x y + a A F a x < y F a L < y b A F b x < y F b R < y R F b + F b x + x F a
206 202 187 subcld φ x y + a A F a x < y F a L < y b A F b x < y F b R < y F a L
207 206 abscld φ x y + a A F a x < y F a L < y b A F b x < y F b R < y F a L
208 205 207 readdcld φ x y + a A F a x < y F a L < y b A F b x < y F b R < y R F b + F b x + x F a + F a L
209 21 a1i φ x y + a A F a x < y F a L < y b A F b x < y F b R < y 4
210 rpre y + y
211 210 ad5antlr φ x y + a A F a x < y F a L < y b A F b x < y F b R < y y
212 209 211 remulcld φ x y + a A F a x < y F a L < y b A F b x < y F b R < y 4 y
213 186 193 196 202 187 absnpncan3d φ x y + a A F a x < y F a L < y b A F b x < y F b R < y R L R F b + F b x + x F a + F a L
214 186 193 abssubd φ x y + a A F a x < y F a L < y b A F b x < y F b R < y R F b = F b R
215 simprr φ x y + a A F a x < y F a L < y b A F b x < y F b R < y F b R < y
216 214 215 eqbrtrd φ x y + a A F a x < y F a L < y b A F b x < y F b R < y R F b < y
217 simprl φ x y + a A F a x < y F a L < y b A F b x < y F b R < y F b x < y
218 simp-5r φ x y + a A F a x < y F a L < y b A x
219 201 ad5ant14 φ x y + a A F a x < y F a L < y F a
220 219 adantr φ x y + a A F a x < y F a L < y b A F a
221 218 220 abssubd φ x y + a A F a x < y F a L < y b A x F a = F a x
222 simplrl φ x y + a A F a x < y F a L < y b A F a x < y
223 221 222 eqbrtrd φ x y + a A F a x < y F a L < y b A x F a < y
224 223 adantr φ x y + a A F a x < y F a L < y b A F b x < y F b R < y x F a < y
225 simplrr φ x y + a A F a x < y F a L < y b A F a L < y
226 225 adantr φ x y + a A F a x < y F a L < y b A F b x < y F b R < y F a L < y
227 195 198 204 207 211 216 217 224 226 lt4addmuld φ x y + a A F a x < y F a L < y b A F b x < y F b R < y R F b + F b x + x F a + F a L < 4 y
228 189 208 212 213 227 lelttrd φ x y + a A F a x < y F a L < y b A F b x < y F b R < y R L < 4 y
229 228 ex φ x y + a A F a x < y F a L < y b A F b x < y F b R < y R L < 4 y
230 229 adantl3r φ x y + z + w A w B w B < z F w x < y a A F a x < y F a L < y b A F b x < y F b R < y R L < 4 y
231 230 reximdva φ x y + z + w A w B w B < z F w x < y a A F a x < y F a L < y b A F b x < y F b R < y b A R L < 4 y
232 185 231 mpd φ x y + z + w A w B w B < z F w x < y a A F a x < y F a L < y b A R L < 4 y
233 fresin F : A F −∞ B : A −∞ B
234 4 233 syl φ F −∞ B : A −∞ B
235 ioosscn −∞ B
236 50 235 sstri A −∞ B
237 236 a1i φ A −∞ B
238 234 237 59 ellimc3 φ L F −∞ B lim B L y + v + w A −∞ B w B w B < v F −∞ B w L < y
239 7 238 mpbid φ L y + v + w A −∞ B w B w B < v F −∞ B w L < y
240 239 simprd φ y + v + w A −∞ B w B w B < v F −∞ B w L < y
241 240 r19.21bi φ y + v + w A −∞ B w B w B < v F −∞ B w L < y
242 241 3ad2ant1 φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y
243 simp11l φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y φ
244 simp12 φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y z +
245 simp2 φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y v +
246 breq2 u = if z v z v a B < u a B < if z v z v
247 246 rexbidv u = if z v z v a A −∞ B B a B < u a A −∞ B B a B < if z v z v
248 inss1 limPt K A −∞ B limPt K A −∞ B
249 248 a1i φ limPt K A −∞ B limPt K A −∞ B
250 52 a1i φ A −∞ B
251 81 83 restlp K Top A −∞ B limPt J A −∞ B = limPt K A −∞ B
252 73 75 250 251 syl3anc φ limPt J A −∞ B = limPt K A −∞ B
253 87 fveq1i limPt TopOpen fld A −∞ B = limPt K A −∞ B
254 253 a1i φ limPt TopOpen fld A −∞ B = limPt K A −∞ B
255 249 252 254 3sstr4d φ limPt J A −∞ B limPt TopOpen fld A −∞ B
256 255 5 sseldd φ B limPt TopOpen fld A −∞ B
257 237 59 islpcn φ B limPt TopOpen fld A −∞ B u + a A −∞ B B a B < u
258 256 257 mpbid φ u + a A −∞ B B a B < u
259 258 3ad2ant1 φ z + v + u + a A −∞ B B a B < u
260 247 259 96 rspcdva φ z + v + a A −∞ B B a B < if z v z v
261 eldifi a A −∞ B B a A −∞ B
262 52 261 sseldi a A −∞ B B a
263 75 sselda φ a a
264 59 adantr φ a B
265 263 264 subcld φ a a B
266 265 abscld φ a a B
267 266 3ad2antl1 φ z + v + a a B
268 267 adantr φ z + v + a a B < if z v z v a B
269 106 ad2antrr φ z + v + a a B < if z v z v if z v z v
270 109 ad2antrr φ z + v + a a B < if z v z v z
271 simpr φ z + v + a a B < if z v z v a B < if z v z v
272 115 ad2antrr φ z + v + a a B < if z v z v if z v z v z
273 268 269 270 271 272 ltletrd φ z + v + a a B < if z v z v a B < z
274 118 ad2antrr φ z + v + a a B < if z v z v v
275 min2 z v if z v z v v
276 108 112 275 syl2an z + v + if z v z v v
277 276 3adant1 φ z + v + if z v z v v
278 277 ad2antrr φ z + v + a a B < if z v z v if z v z v v
279 268 269 274 271 278 ltletrd φ z + v + a a B < if z v z v a B < v
280 273 279 jca φ z + v + a a B < if z v z v a B < z a B < v
281 280 ex φ z + v + a a B < if z v z v a B < z a B < v
282 262 281 sylan2 φ z + v + a A −∞ B B a B < if z v z v a B < z a B < v
283 282 reximdva φ z + v + a A −∞ B B a B < if z v z v a A −∞ B B a B < z a B < v
284 260 283 mpd φ z + v + a A −∞ B B a B < z a B < v
285 243 244 245 284 syl3anc φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y a A −∞ B B a B < z a B < v
286 nfv a φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y
287 nfre1 a a A F a x < y F a L < y
288 261 elin1d a A −∞ B B a A
289 288 3ad2ant2 φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y a A −∞ B B a B < z a B < v a A
290 simp113 φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y a A −∞ B B a B < z a B < v w A w B w B < z F w x < y
291 eldifsni a A −∞ B B a B
292 291 adantr a A −∞ B B a B < z a B < v a B
293 simprl a A −∞ B B a B < z a B < v a B < z
294 292 293 jca a A −∞ B B a B < z a B < v a B a B < z
295 294 3adant1 φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y a A −∞ B B a B < z a B < v a B a B < z
296 neeq1 w = a w B a B
297 fvoveq1 w = a w B = a B
298 297 breq1d w = a w B < z a B < z
299 296 298 anbi12d w = a w B w B < z a B a B < z
300 299 imbrov2fvoveq w = a w B w B < z F w x < y a B a B < z F a x < y
301 300 rspcva a A w A w B w B < z F w x < y a B a B < z F a x < y
302 301 imp a A w A w B w B < z F w x < y a B a B < z F a x < y
303 289 290 295 302 syl21anc φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y a A −∞ B B a B < z a B < v F a x < y
304 261 3ad2ant2 φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y a A −∞ B B a B < z a B < v a A −∞ B
305 243 3ad2ant1 φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y a A −∞ B B a B < z a B < v φ
306 simp13 φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y a A −∞ B B a B < z a B < v w A −∞ B w B w B < v F −∞ B w L < y
307 nfra1 w w A −∞ B w B w B < v F −∞ B w L < y
308 149 307 nfan w φ w A −∞ B w B w B < v F −∞ B w L < y
309 elinel2 w A −∞ B w −∞ B
310 309 fvresd w A −∞ B F −∞ B w = F w
311 310 eqcomd w A −∞ B F w = F −∞ B w
312 311 fvoveq1d w A −∞ B F w L = F −∞ B w L
313 312 3ad2ant2 φ w A −∞ B w B w B < v F −∞ B w L < y w A −∞ B w B w B < v F w L = F −∞ B w L
314 rspa w A −∞ B w B w B < v F −∞ B w L < y w A −∞ B w B w B < v F −∞ B w L < y
315 314 3impia w A −∞ B w B w B < v F −∞ B w L < y w A −∞ B w B w B < v F −∞ B w L < y
316 315 3adant1l φ w A −∞ B w B w B < v F −∞ B w L < y w A −∞ B w B w B < v F −∞ B w L < y
317 313 316 eqbrtrd φ w A −∞ B w B w B < v F −∞ B w L < y w A −∞ B w B w B < v F w L < y
318 317 3exp φ w A −∞ B w B w B < v F −∞ B w L < y w A −∞ B w B w B < v F w L < y
319 308 318 ralrimi φ w A −∞ B w B w B < v F −∞ B w L < y w A −∞ B w B w B < v F w L < y
320 305 306 319 syl2anc φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y a A −∞ B B a B < z a B < v w A −∞ B w B w B < v F w L < y
321 291 anim1i a A −∞ B B a B < v a B a B < v
322 321 adantrl a A −∞ B B a B < z a B < v a B a B < v
323 322 3adant1 φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y a A −∞ B B a B < z a B < v a B a B < v
324 297 breq1d w = a w B < v a B < v
325 296 324 anbi12d w = a w B w B < v a B a B < v
326 325 imbrov2fvoveq w = a w B w B < v F w L < y a B a B < v F a L < y
327 326 rspcva a A −∞ B w A −∞ B w B w B < v F w L < y a B a B < v F a L < y
328 327 imp a A −∞ B w A −∞ B w B w B < v F w L < y a B a B < v F a L < y
329 304 320 323 328 syl21anc φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y a A −∞ B B a B < z a B < v F a L < y
330 rspe a A F a x < y F a L < y a A F a x < y F a L < y
331 289 303 329 330 syl12anc φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y a A −∞ B B a B < z a B < v a A F a x < y F a L < y
332 331 3exp φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y a A −∞ B B a B < z a B < v a A F a x < y F a L < y
333 286 287 332 rexlimd φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y a A −∞ B B a B < z a B < v a A F a x < y F a L < y
334 285 333 mpd φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y a A F a x < y F a L < y
335 334 3exp φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y a A F a x < y F a L < y
336 335 rexlimdv φ y + z + w A w B w B < z F w x < y v + w A −∞ B w B w B < v F −∞ B w L < y a A F a x < y F a L < y
337 242 336 mpd φ y + z + w A w B w B < z F w x < y a A F a x < y F a L < y
338 337 3exp φ y + z + w A w B w B < z F w x < y a A F a x < y F a L < y
339 338 rexlimdv φ y + z + w A w B w B < z F w x < y a A F a x < y F a L < y
340 339 imp φ y + z + w A w B w B < z F w x < y a A F a x < y F a L < y
341 340 adantllr φ x y + z + w A w B w B < z F w x < y a A F a x < y F a L < y
342 232 341 reximddv3 φ x y + z + w A w B w B < z F w x < y a A b A R L < 4 y
343 38 39 41 342 syl21anc φ x y + z + w A w B w B < z F w x < y y + a A b A R L < 4 y
344 343 ex φ x y + z + w A w B w B < z F w x < y y + a A b A R L < 4 y
345 30 31 37 344 vtoclf φ x y + z + w A w B w B < z F w x < y R L 4 + a A b A R L < 4 R L 4
346 25 345 mpd φ x y + z + w A w B w B < z F w x < y a A b A R L < 4 R L 4
347 simpr φ R L < 4 R L 4 R L < 4 R L 4
348 abssubrp R L R L R L +
349 11 14 17 348 syl3anc φ R L +
350 349 rpcnd φ R L
351 350 adantr φ R L < 4 R L 4 R L
352 4cn 4
353 352 a1i φ R L < 4 R L 4 4
354 4ne0 4 0
355 354 a1i φ R L < 4 R L 4 4 0
356 351 353 355 divcan2d φ R L < 4 R L 4 4 R L 4 = R L
357 347 356 breqtrd φ R L < 4 R L 4 R L < R L
358 357 ex φ R L < 4 R L 4 R L < R L
359 358 a1d φ a A b A R L < 4 R L 4 R L < R L
360 359 ad2antrr φ x y + z + w A w B w B < z F w x < y a A b A R L < 4 R L 4 R L < R L
361 360 rexlimdvv φ x y + z + w A w B w B < z F w x < y a A b A R L < 4 R L 4 R L < R L
362 346 361 mpd φ x y + z + w A w B w B < z F w x < y R L < R L
363 16 abscld φ x y + z + w A w B w B < z F w x < y R L
364 363 ltnrd φ x y + z + w A w B w B < z F w x < y ¬ R L < R L
365 362 364 pm2.65da φ x ¬ y + z + w A w B w B < z F w x < y
366 365 ex φ x ¬ y + z + w A w B w B < z F w x < y
367 imnan x ¬ y + z + w A w B w B < z F w x < y ¬ x y + z + w A w B w B < z F w x < y
368 366 367 sylib φ ¬ x y + z + w A w B w B < z F w x < y
369 2 75 sstrd φ A
370 4 369 59 ellimc3 φ x F lim B x y + z + w A w B w B < z F w x < y
371 368 370 mtbird φ ¬ x F lim B
372 371 eq0rdv φ F lim B =