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	sseldi	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
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ℂ 𝐵 ) ) ) )