Metamath Proof Explorer

Theorem limcrecl

Description: If F is a real-valued function, B is a limit point of its domain, and the limit of F at B exists, then this limit is real. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses limcrecl.1 ${⊢}{\phi }\to {F}:{A}⟶ℝ$
limcrecl.2 ${⊢}{\phi }\to {A}\subseteq ℂ$
limcrecl.3 ${⊢}{\phi }\to {B}\in \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left({A}\right)$
limcrecl.4 ${⊢}{\phi }\to {L}\in \left({F}{lim}_{ℂ}{B}\right)$
Assertion limcrecl ${⊢}{\phi }\to {L}\in ℝ$

Proof

Step Hyp Ref Expression
1 limcrecl.1 ${⊢}{\phi }\to {F}:{A}⟶ℝ$
2 limcrecl.2 ${⊢}{\phi }\to {A}\subseteq ℂ$
3 limcrecl.3 ${⊢}{\phi }\to {B}\in \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left({A}\right)$
4 limcrecl.4 ${⊢}{\phi }\to {L}\in \left({F}{lim}_{ℂ}{B}\right)$
5 4 adantr ${⊢}\left({\phi }\wedge ¬{L}\in ℝ\right)\to {L}\in \left({F}{lim}_{ℂ}{B}\right)$
6 limccl ${⊢}{F}{lim}_{ℂ}{B}\subseteq ℂ$
7 6 4 sseldi ${⊢}{\phi }\to {L}\in ℂ$
8 7 adantr ${⊢}\left({\phi }\wedge ¬{L}\in ℝ\right)\to {L}\in ℂ$
9 simpr ${⊢}\left({\phi }\wedge ¬{L}\in ℝ\right)\to ¬{L}\in ℝ$
10 8 9 eldifd ${⊢}\left({\phi }\wedge ¬{L}\in ℝ\right)\to {L}\in \left(ℂ\setminus ℝ\right)$
11 10 dstregt0 ${⊢}\left({\phi }\wedge ¬{L}\in ℝ\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|$
12 cnxmet ${⊢}\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$
13 12 a1i ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\to \mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$
14 2 ad4antr ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\to {A}\subseteq ℂ$
15 14 ssdifssd ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\to {A}\setminus \left\{{B}\right\}\subseteq ℂ$
16 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
17 16 cnfldtop ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}$
18 17 a1i ${⊢}{\phi }\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}$
19 unicntop ${⊢}ℂ=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
20 2 19 sseqtrdi ${⊢}{\phi }\to {A}\subseteq \bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
21 eqid ${⊢}\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
22 21 lpdifsn ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}\wedge {A}\subseteq \bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\to \left({B}\in \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left({A}\right)↔{B}\in \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left({A}\setminus \left\{{B}\right\}\right)\right)$
23 18 20 22 syl2anc ${⊢}{\phi }\to \left({B}\in \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left({A}\right)↔{B}\in \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left({A}\setminus \left\{{B}\right\}\right)\right)$
24 3 23 mpbid ${⊢}{\phi }\to {B}\in \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left({A}\setminus \left\{{B}\right\}\right)$
25 24 ad4antr ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\to {B}\in \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left({A}\setminus \left\{{B}\right\}\right)$
26 simpr ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\to {y}\in {ℝ}^{+}$
27 16 cnfldtopn ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)$
28 27 lpbl ${⊢}\left(\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge {A}\setminus \left\{{B}\right\}\subseteq ℂ\wedge {B}\in \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left({A}\setminus \left\{{B}\right\}\right)\right)\wedge {y}\in {ℝ}^{+}\right)\to \exists {z}\in \left({A}\setminus \left\{{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)$
29 13 15 25 26 28 syl31anc ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\to \exists {z}\in \left({A}\setminus \left\{{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)$
30 eldif ${⊢}{z}\in \left({A}\setminus \left\{{B}\right\}\right)↔\left({z}\in {A}\wedge ¬{z}\in \left\{{B}\right\}\right)$
31 30 anbi1i ${⊢}\left({z}\in \left({A}\setminus \left\{{B}\right\}\right)\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)↔\left(\left({z}\in {A}\wedge ¬{z}\in \left\{{B}\right\}\right)\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)$
32 anass ${⊢}\left(\left({z}\in {A}\wedge ¬{z}\in \left\{{B}\right\}\right)\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)↔\left({z}\in {A}\wedge \left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\right)$
33 31 32 bitri ${⊢}\left({z}\in \left({A}\setminus \left\{{B}\right\}\right)\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)↔\left({z}\in {A}\wedge \left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\right)$
34 33 rexbii2 ${⊢}\exists {z}\in \left({A}\setminus \left\{{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)↔\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)$
35 29 34 sylib ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)$
36 simprl ${⊢}\left(\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\wedge \left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\right)\to ¬{z}\in \left\{{B}\right\}$
37 velsn ${⊢}{z}\in \left\{{B}\right\}↔{z}={B}$
38 37 necon3bbii ${⊢}¬{z}\in \left\{{B}\right\}↔{z}\ne {B}$
39 36 38 sylib ${⊢}\left(\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\wedge \left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\right)\to {z}\ne {B}$
40 simp-5l ${⊢}\left(\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\wedge \left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\right)\to {\phi }$
41 simplr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\wedge \left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\right)\to {y}\in {ℝ}^{+}$
42 simprr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\wedge \left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\right)\to {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)$
43 simp3 ${⊢}\left({\phi }\wedge {y}\in {ℝ}^{+}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\to {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)$
44 12 a1i ${⊢}\left({\phi }\wedge {y}\in {ℝ}^{+}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\to \mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)$
45 19 lpss ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}\wedge {A}\subseteq ℂ\right)\to \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left({A}\right)\subseteq ℂ$
46 18 2 45 syl2anc ${⊢}{\phi }\to \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left({A}\right)\subseteq ℂ$
47 46 3 sseldd ${⊢}{\phi }\to {B}\in ℂ$
48 47 3ad2ant1 ${⊢}\left({\phi }\wedge {y}\in {ℝ}^{+}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\to {B}\in ℂ$
49 rpxr ${⊢}{y}\in {ℝ}^{+}\to {y}\in {ℝ}^{*}$
50 49 3ad2ant2 ${⊢}\left({\phi }\wedge {y}\in {ℝ}^{+}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\to {y}\in {ℝ}^{*}$
51 elbl ${⊢}\left(\mathrm{abs}\circ -\in \mathrm{\infty Met}\left(ℂ\right)\wedge {B}\in ℂ\wedge {y}\in {ℝ}^{*}\right)\to \left({z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)↔\left({z}\in ℂ\wedge {B}\left(\mathrm{abs}\circ -\right){z}<{y}\right)\right)$
52 44 48 50 51 syl3anc ${⊢}\left({\phi }\wedge {y}\in {ℝ}^{+}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\to \left({z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)↔\left({z}\in ℂ\wedge {B}\left(\mathrm{abs}\circ -\right){z}<{y}\right)\right)$
53 43 52 mpbid ${⊢}\left({\phi }\wedge {y}\in {ℝ}^{+}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\to \left({z}\in ℂ\wedge {B}\left(\mathrm{abs}\circ -\right){z}<{y}\right)$
54 53 simpld ${⊢}\left({\phi }\wedge {y}\in {ℝ}^{+}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\to {z}\in ℂ$
55 54 48 abssubd ${⊢}\left({\phi }\wedge {y}\in {ℝ}^{+}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\to \left|{z}-{B}\right|=\left|{B}-{z}\right|$
56 eqid ${⊢}\mathrm{abs}\circ -=\mathrm{abs}\circ -$
57 56 cnmetdval ${⊢}\left({B}\in ℂ\wedge {z}\in ℂ\right)\to {B}\left(\mathrm{abs}\circ -\right){z}=\left|{B}-{z}\right|$
58 48 54 57 syl2anc ${⊢}\left({\phi }\wedge {y}\in {ℝ}^{+}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\to {B}\left(\mathrm{abs}\circ -\right){z}=\left|{B}-{z}\right|$
59 53 simprd ${⊢}\left({\phi }\wedge {y}\in {ℝ}^{+}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\to {B}\left(\mathrm{abs}\circ -\right){z}<{y}$
60 58 59 eqbrtrrd ${⊢}\left({\phi }\wedge {y}\in {ℝ}^{+}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\to \left|{B}-{z}\right|<{y}$
61 55 60 eqbrtrd ${⊢}\left({\phi }\wedge {y}\in {ℝ}^{+}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\to \left|{z}-{B}\right|<{y}$
62 40 41 42 61 syl3anc ${⊢}\left(\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\wedge \left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\right)\to \left|{z}-{B}\right|<{y}$
63 39 62 jca ${⊢}\left(\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\wedge \left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\right)\to \left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)$
64 63 adantlr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\wedge {z}\in {A}\right)\wedge \left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\right)\to \left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)$
65 40 adantlr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\wedge {z}\in {A}\right)\wedge \left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\right)\to {\phi }$
66 simplr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\wedge {z}\in {A}\right)\wedge \left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\right)\to {z}\in {A}$
67 65 66 jca ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\wedge {z}\in {A}\right)\wedge \left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\right)\to \left({\phi }\wedge {z}\in {A}\right)$
68 simp-5r ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\wedge {z}\in {A}\right)\wedge \left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\right)\to {x}\in {ℝ}^{+}$
69 simp-4r ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\wedge {z}\in {A}\right)\wedge \left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\right)\to \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|$
70 rpre ${⊢}{x}\in {ℝ}^{+}\to {x}\in ℝ$
71 70 ad2antlr ${⊢}\left(\left(\left({\phi }\wedge {z}\in {A}\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\to {x}\in ℝ$
72 1 ffvelrnda ${⊢}\left({\phi }\wedge {z}\in {A}\right)\to {F}\left({z}\right)\in ℝ$
73 72 recnd ${⊢}\left({\phi }\wedge {z}\in {A}\right)\to {F}\left({z}\right)\in ℂ$
74 73 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {z}\in {A}\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\to {F}\left({z}\right)\in ℂ$
75 7 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {z}\in {A}\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\to {L}\in ℂ$
76 74 75 subcld ${⊢}\left(\left(\left({\phi }\wedge {z}\in {A}\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\to {F}\left({z}\right)-{L}\in ℂ$
77 76 abscld ${⊢}\left(\left(\left({\phi }\wedge {z}\in {A}\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\to \left|{F}\left({z}\right)-{L}\right|\in ℝ$
78 72 adantr ${⊢}\left(\left({\phi }\wedge {z}\in {A}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\to {F}\left({z}\right)\in ℝ$
79 nfv ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}{\phi }$
80 nfra1 ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|$
81 79 80 nfan ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)$
82 rspa ${⊢}\left(\forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\wedge {w}\in ℝ\right)\to {x}<\left|{L}-{w}\right|$
83 82 adantll ${⊢}\left(\left({\phi }\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {w}\in ℝ\right)\to {x}<\left|{L}-{w}\right|$
84 7 adantr ${⊢}\left({\phi }\wedge {w}\in ℝ\right)\to {L}\in ℂ$
85 ax-resscn ${⊢}ℝ\subseteq ℂ$
86 85 a1i ${⊢}{\phi }\to ℝ\subseteq ℂ$
87 86 sselda ${⊢}\left({\phi }\wedge {w}\in ℝ\right)\to {w}\in ℂ$
88 84 87 abssubd ${⊢}\left({\phi }\wedge {w}\in ℝ\right)\to \left|{L}-{w}\right|=\left|{w}-{L}\right|$
89 88 adantlr ${⊢}\left(\left({\phi }\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {w}\in ℝ\right)\to \left|{L}-{w}\right|=\left|{w}-{L}\right|$
90 83 89 breqtrd ${⊢}\left(\left({\phi }\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {w}\in ℝ\right)\to {x}<\left|{w}-{L}\right|$
91 90 ex ${⊢}\left({\phi }\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\to \left({w}\in ℝ\to {x}<\left|{w}-{L}\right|\right)$
92 81 91 ralrimi ${⊢}\left({\phi }\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\to \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{w}-{L}\right|$
93 92 adantlr ${⊢}\left(\left({\phi }\wedge {z}\in {A}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\to \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{w}-{L}\right|$
94 fvoveq1 ${⊢}{w}={F}\left({z}\right)\to \left|{w}-{L}\right|=\left|{F}\left({z}\right)-{L}\right|$
95 94 breq2d ${⊢}{w}={F}\left({z}\right)\to \left({x}<\left|{w}-{L}\right|↔{x}<\left|{F}\left({z}\right)-{L}\right|\right)$
96 95 rspcv ${⊢}{F}\left({z}\right)\in ℝ\to \left(\forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{w}-{L}\right|\to {x}<\left|{F}\left({z}\right)-{L}\right|\right)$
97 78 93 96 sylc ${⊢}\left(\left({\phi }\wedge {z}\in {A}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\to {x}<\left|{F}\left({z}\right)-{L}\right|$
98 97 adantlr ${⊢}\left(\left(\left({\phi }\wedge {z}\in {A}\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\to {x}<\left|{F}\left({z}\right)-{L}\right|$
99 71 77 98 ltnsymd ${⊢}\left(\left(\left({\phi }\wedge {z}\in {A}\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\to ¬\left|{F}\left({z}\right)-{L}\right|<{x}$
100 67 68 69 99 syl21anc ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\wedge {z}\in {A}\right)\wedge \left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\right)\to ¬\left|{F}\left({z}\right)-{L}\right|<{x}$
101 64 100 jcnd ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\wedge {z}\in {A}\right)\wedge \left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\right)\to ¬\left(\left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)\to \left|{F}\left({z}\right)-{L}\right|<{x}\right)$
102 101 ex ${⊢}\left(\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\wedge {z}\in {A}\right)\to \left(\left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\to ¬\left(\left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)\to \left|{F}\left({z}\right)-{L}\right|<{x}\right)\right)$
103 102 reximdva ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\to \left(\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left\{{B}\right\}\wedge {z}\in \left({B}\mathrm{ball}\left(\mathrm{abs}\circ -\right){y}\right)\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}¬\left(\left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)\to \left|{F}\left({z}\right)-{L}\right|<{x}\right)\right)$
104 35 103 mpd ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}¬\left(\left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)\to \left|{F}\left({z}\right)-{L}\right|<{x}\right)$
105 rexnal ${⊢}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}¬\left(\left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)\to \left|{F}\left({z}\right)-{L}\right|<{x}\right)↔¬\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)\to \left|{F}\left({z}\right)-{L}\right|<{x}\right)$
106 104 105 sylib ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\wedge {y}\in {ℝ}^{+}\right)\to ¬\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)\to \left|{F}\left({z}\right)-{L}\right|<{x}\right)$
107 106 nrexdv ${⊢}\left(\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\wedge \forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\right)\to ¬\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)\to \left|{F}\left({z}\right)-{L}\right|<{x}\right)$
108 107 ex ${⊢}\left(\left({\phi }\wedge ¬{L}\in ℝ\right)\wedge {x}\in {ℝ}^{+}\right)\to \left(\forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\to ¬\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)\to \left|{F}\left({z}\right)-{L}\right|<{x}\right)\right)$
109 108 reximdva ${⊢}\left({\phi }\wedge ¬{L}\in ℝ\right)\to \left(\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℝ\phantom{\rule{.4em}{0ex}}{x}<\left|{L}-{w}\right|\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}¬\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)\to \left|{F}\left({z}\right)-{L}\right|<{x}\right)\right)$
110 11 109 mpd ${⊢}\left({\phi }\wedge ¬{L}\in ℝ\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}¬\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)\to \left|{F}\left({z}\right)-{L}\right|<{x}\right)$
111 rexnal ${⊢}\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}¬\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)\to \left|{F}\left({z}\right)-{L}\right|<{x}\right)↔¬\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)\to \left|{F}\left({z}\right)-{L}\right|<{x}\right)$
112 110 111 sylib ${⊢}\left({\phi }\wedge ¬{L}\in ℝ\right)\to ¬\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)\to \left|{F}\left({z}\right)-{L}\right|<{x}\right)$
113 112 intnand ${⊢}\left({\phi }\wedge ¬{L}\in ℝ\right)\to ¬\left({L}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)\to \left|{F}\left({z}\right)-{L}\right|<{x}\right)\right)$
114 1 86 fssd ${⊢}{\phi }\to {F}:{A}⟶ℂ$
115 114 2 47 ellimc3 ${⊢}{\phi }\to \left({L}\in \left({F}{lim}_{ℂ}{B}\right)↔\left({L}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)\to \left|{F}\left({z}\right)-{L}\right|<{x}\right)\right)\right)$
116 115 adantr ${⊢}\left({\phi }\wedge ¬{L}\in ℝ\right)\to \left({L}\in \left({F}{lim}_{ℂ}{B}\right)↔\left({L}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({z}\ne {B}\wedge \left|{z}-{B}\right|<{y}\right)\to \left|{F}\left({z}\right)-{L}\right|<{x}\right)\right)\right)$
117 113 116 mtbird ${⊢}\left({\phi }\wedge ¬{L}\in ℝ\right)\to ¬{L}\in \left({F}{lim}_{ℂ}{B}\right)$
118 5 117 condan ${⊢}{\phi }\to {L}\in ℝ$