# Metamath Proof Explorer

## Theorem limclr

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. In this case, the three limits coincide. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses limclr.k ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
limclr.a ${⊢}{\phi }\to {A}\subseteq ℝ$
limclr.j ${⊢}{J}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
limclr.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
limclr.lp1 ${⊢}{\phi }\to {B}\in \mathrm{limPt}\left({J}\right)\left({A}\cap \left(\mathrm{-\infty },{B}\right)\right)$
limclr.lp2 ${⊢}{\phi }\to {B}\in \mathrm{limPt}\left({J}\right)\left({A}\cap \left({B},\mathrm{+\infty }\right)\right)$
limclr.l ${⊢}{\phi }\to {L}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{B}\right)}\right){lim}_{ℂ}{B}\right)$
limclr.r ${⊢}{\phi }\to {R}\in \left(\left({{F}↾}_{\left({B},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{B}\right)$
Assertion limclr ${⊢}{\phi }\to \left(\left({F}{lim}_{ℂ}{B}\ne \varnothing ↔{L}={R}\right)\wedge \left({L}={R}\to {L}\in \left({F}{lim}_{ℂ}{B}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 limclr.k ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
2 limclr.a ${⊢}{\phi }\to {A}\subseteq ℝ$
3 limclr.j ${⊢}{J}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
4 limclr.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
5 limclr.lp1 ${⊢}{\phi }\to {B}\in \mathrm{limPt}\left({J}\right)\left({A}\cap \left(\mathrm{-\infty },{B}\right)\right)$
6 limclr.lp2 ${⊢}{\phi }\to {B}\in \mathrm{limPt}\left({J}\right)\left({A}\cap \left({B},\mathrm{+\infty }\right)\right)$
7 limclr.l ${⊢}{\phi }\to {L}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{B}\right)}\right){lim}_{ℂ}{B}\right)$
8 limclr.r ${⊢}{\phi }\to {R}\in \left(\left({{F}↾}_{\left({B},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{B}\right)$
9 neqne ${⊢}¬{L}={R}\to {L}\ne {R}$
10 2 adantr ${⊢}\left({\phi }\wedge {L}\ne {R}\right)\to {A}\subseteq ℝ$
11 4 adantr ${⊢}\left({\phi }\wedge {L}\ne {R}\right)\to {F}:{A}⟶ℂ$
12 5 adantr ${⊢}\left({\phi }\wedge {L}\ne {R}\right)\to {B}\in \mathrm{limPt}\left({J}\right)\left({A}\cap \left(\mathrm{-\infty },{B}\right)\right)$
13 6 adantr ${⊢}\left({\phi }\wedge {L}\ne {R}\right)\to {B}\in \mathrm{limPt}\left({J}\right)\left({A}\cap \left({B},\mathrm{+\infty }\right)\right)$
14 7 adantr ${⊢}\left({\phi }\wedge {L}\ne {R}\right)\to {L}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{B}\right)}\right){lim}_{ℂ}{B}\right)$
15 8 adantr ${⊢}\left({\phi }\wedge {L}\ne {R}\right)\to {R}\in \left(\left({{F}↾}_{\left({B},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{B}\right)$
16 simpr ${⊢}\left({\phi }\wedge {L}\ne {R}\right)\to {L}\ne {R}$
17 1 10 3 11 12 13 14 15 16 limclner ${⊢}\left({\phi }\wedge {L}\ne {R}\right)\to {F}{lim}_{ℂ}{B}=\varnothing$
18 nne ${⊢}¬{F}{lim}_{ℂ}{B}\ne \varnothing ↔{F}{lim}_{ℂ}{B}=\varnothing$
19 17 18 sylibr ${⊢}\left({\phi }\wedge {L}\ne {R}\right)\to ¬{F}{lim}_{ℂ}{B}\ne \varnothing$
20 9 19 sylan2 ${⊢}\left({\phi }\wedge ¬{L}={R}\right)\to ¬{F}{lim}_{ℂ}{B}\ne \varnothing$
21 20 ex ${⊢}{\phi }\to \left(¬{L}={R}\to ¬{F}{lim}_{ℂ}{B}\ne \varnothing \right)$
22 21 con4d ${⊢}{\phi }\to \left({F}{lim}_{ℂ}{B}\ne \varnothing \to {L}={R}\right)$
23 2 adantr ${⊢}\left({\phi }\wedge {L}={R}\right)\to {A}\subseteq ℝ$
24 4 adantr ${⊢}\left({\phi }\wedge {L}={R}\right)\to {F}:{A}⟶ℂ$
25 retop ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$
26 3 25 eqeltri ${⊢}{J}\in \mathrm{Top}$
27 inss2 ${⊢}{A}\cap \left(\mathrm{-\infty },{B}\right)\subseteq \left(\mathrm{-\infty },{B}\right)$
28 ioossre ${⊢}\left(\mathrm{-\infty },{B}\right)\subseteq ℝ$
29 27 28 sstri ${⊢}{A}\cap \left(\mathrm{-\infty },{B}\right)\subseteq ℝ$
30 uniretop ${⊢}ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
31 3 eqcomi ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)={J}$
32 31 unieqi ${⊢}\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\bigcup {J}$
33 30 32 eqtri ${⊢}ℝ=\bigcup {J}$
34 33 lpss ${⊢}\left({J}\in \mathrm{Top}\wedge {A}\cap \left(\mathrm{-\infty },{B}\right)\subseteq ℝ\right)\to \mathrm{limPt}\left({J}\right)\left({A}\cap \left(\mathrm{-\infty },{B}\right)\right)\subseteq ℝ$
35 26 29 34 mp2an ${⊢}\mathrm{limPt}\left({J}\right)\left({A}\cap \left(\mathrm{-\infty },{B}\right)\right)\subseteq ℝ$
36 35 5 sseldi ${⊢}{\phi }\to {B}\in ℝ$
37 36 adantr ${⊢}\left({\phi }\wedge {L}={R}\right)\to {B}\in ℝ$
38 7 adantr ${⊢}\left({\phi }\wedge {L}={R}\right)\to {L}\in \left(\left({{F}↾}_{\left(\mathrm{-\infty },{B}\right)}\right){lim}_{ℂ}{B}\right)$
39 8 adantr ${⊢}\left({\phi }\wedge {L}={R}\right)\to {R}\in \left(\left({{F}↾}_{\left({B},\mathrm{+\infty }\right)}\right){lim}_{ℂ}{B}\right)$
40 simpr ${⊢}\left({\phi }\wedge {L}={R}\right)\to {L}={R}$
41 1 23 3 24 37 38 39 40 limcleqr ${⊢}\left({\phi }\wedge {L}={R}\right)\to {L}\in \left({F}{lim}_{ℂ}{B}\right)$
42 41 ne0d ${⊢}\left({\phi }\wedge {L}={R}\right)\to {F}{lim}_{ℂ}{B}\ne \varnothing$
43 42 ex ${⊢}{\phi }\to \left({L}={R}\to {F}{lim}_{ℂ}{B}\ne \varnothing \right)$
44 22 43 impbid ${⊢}{\phi }\to \left({F}{lim}_{ℂ}{B}\ne \varnothing ↔{L}={R}\right)$
45 41 ex ${⊢}{\phi }\to \left({L}={R}\to {L}\in \left({F}{lim}_{ℂ}{B}\right)\right)$
46 44 45 jca ${⊢}{\phi }\to \left(\left({F}{lim}_{ℂ}{B}\ne \varnothing ↔{L}={R}\right)\wedge \left({L}={R}\to {L}\in \left({F}{lim}_{ℂ}{B}\right)\right)\right)$