This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
limclr.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
limclr.j ⊢ 𝐽 = ( topGen ‘ ran (,) )
limclr.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
limclr.lp1 ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) )
limclr.lp2 ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) )
limclr.l ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) limℂ 𝐵 ) )
limclr.r ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) limℂ 𝐵 ) )
Assertion limclr ( 𝜑 → ( ( ( 𝐹 limℂ 𝐵 ) ≠ ∅ ↔ 𝐿 = 𝑅 ) ∧ ( 𝐿 = 𝑅 → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 limclr.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
2 limclr.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3 limclr.j ⊢ 𝐽 = ( topGen ‘ ran (,) )
4 limclr.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
5 limclr.lp1 ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) )
6 limclr.lp2 ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) )
7 limclr.l ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) limℂ 𝐵 ) )
8 limclr.r ⊢ ( 𝜑 → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) limℂ 𝐵 ) )
9 neqne ⊢ ( ¬ 𝐿 = 𝑅 → 𝐿 ≠ 𝑅 )
10 2 adantr ⊢ ( ( 𝜑 ∧ 𝐿 ≠ 𝑅 ) → 𝐴 ⊆ ℝ )
11 4 adantr ⊢ ( ( 𝜑 ∧ 𝐿 ≠ 𝑅 ) → 𝐹 : 𝐴 ⟶ ℂ )
12 5 adantr ⊢ ( ( 𝜑 ∧ 𝐿 ≠ 𝑅 ) → 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) )
13 6 adantr ⊢ ( ( 𝜑 ∧ 𝐿 ≠ 𝑅 ) → 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( 𝐵 (,) +∞ ) ) ) )
14 7 adantr ⊢ ( ( 𝜑 ∧ 𝐿 ≠ 𝑅 ) → 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) limℂ 𝐵 ) )
15 8 adantr ⊢ ( ( 𝜑 ∧ 𝐿 ≠ 𝑅 ) → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) limℂ 𝐵 ) )
16 simpr ⊢ ( ( 𝜑 ∧ 𝐿 ≠ 𝑅 ) → 𝐿 ≠ 𝑅 )
17 1 10 3 11 12 13 14 15 16 limclner ⊢ ( ( 𝜑 ∧ 𝐿 ≠ 𝑅 ) → ( 𝐹 limℂ 𝐵 ) = ∅ )
18 nne ⊢ ( ¬ ( 𝐹 limℂ 𝐵 ) ≠ ∅ ↔ ( 𝐹 limℂ 𝐵 ) = ∅ )
19 17 18 sylibr ⊢ ( ( 𝜑 ∧ 𝐿 ≠ 𝑅 ) → ¬ ( 𝐹 limℂ 𝐵 ) ≠ ∅ )
20 9 19 sylan2 ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 𝑅 ) → ¬ ( 𝐹 limℂ 𝐵 ) ≠ ∅ )
21 20 ex ⊢ ( 𝜑 → ( ¬ 𝐿 = 𝑅 → ¬ ( 𝐹 limℂ 𝐵 ) ≠ ∅ ) )
22 21 con4d ⊢ ( 𝜑 → ( ( 𝐹 limℂ 𝐵 ) ≠ ∅ → 𝐿 = 𝑅 ) )
23 2 adantr ⊢ ( ( 𝜑 ∧ 𝐿 = 𝑅 ) → 𝐴 ⊆ ℝ )
24 4 adantr ⊢ ( ( 𝜑 ∧ 𝐿 = 𝑅 ) → 𝐹 : 𝐴 ⟶ ℂ )
25 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
26 3 25 eqeltri ⊢ 𝐽 ∈ Top
27 inss2 ⊢ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ( -∞ (,) 𝐵 )
28 ioossre ⊢ ( -∞ (,) 𝐵 ) ⊆ ℝ
29 27 28 sstri ⊢ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ℝ
30 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
31 3 eqcomi ⊢ ( topGen ‘ ran (,) ) = 𝐽
32 31 unieqi ⊢ ∪ ( topGen ‘ ran (,) ) = ∪ 𝐽
33 30 32 eqtri ⊢ ℝ = ∪ 𝐽
34 33 lpss ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ⊆ ℝ ) → ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) ⊆ ℝ )
35 26 29 34 mp2an ⊢ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 ∩ ( -∞ (,) 𝐵 ) ) ) ⊆ ℝ
36 35 5 sselid ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝐿 = 𝑅 ) → 𝐵 ∈ ℝ )
38 7 adantr ⊢ ( ( 𝜑 ∧ 𝐿 = 𝑅 ) → 𝐿 ∈ ( ( 𝐹 ↾ ( -∞ (,) 𝐵 ) ) limℂ 𝐵 ) )
39 8 adantr ⊢ ( ( 𝜑 ∧ 𝐿 = 𝑅 ) → 𝑅 ∈ ( ( 𝐹 ↾ ( 𝐵 (,) +∞ ) ) limℂ 𝐵 ) )
40 simpr ⊢ ( ( 𝜑 ∧ 𝐿 = 𝑅 ) → 𝐿 = 𝑅 )
41 1 23 3 24 37 38 39 40 limcleqr ⊢ ( ( 𝜑 ∧ 𝐿 = 𝑅 ) → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )
42 41 ne0d ⊢ ( ( 𝜑 ∧ 𝐿 = 𝑅 ) → ( 𝐹 limℂ 𝐵 ) ≠ ∅ )
43 42 ex ⊢ ( 𝜑 → ( 𝐿 = 𝑅 → ( 𝐹 limℂ 𝐵 ) ≠ ∅ ) )
44 22 43 impbid ⊢ ( 𝜑 → ( ( 𝐹 limℂ 𝐵 ) ≠ ∅ ↔ 𝐿 = 𝑅 ) )
45 41 ex ⊢ ( 𝜑 → ( 𝐿 = 𝑅 → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) ) )
46 44 45 jca ⊢ ( 𝜑 → ( ( ( 𝐹 limℂ 𝐵 ) ≠ ∅ ↔ 𝐿 = 𝑅 ) ∧ ( 𝐿 = 𝑅 → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) ) ) )