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 = TopOpen (ℂ_{fld})$
	limclr.a	$⊢ φ \to A \subseteq ℝ$
	limclr.j	$⊢ J = topGen (ran (.))$
	limclr.f	$⊢ φ \to F : A ⟶ ℂ$
	limclr.lp1	$⊢ φ \to B \in limPt (J) (A \cap (−∞, B))$
	limclr.lp2	$⊢ φ \to B \in limPt (J) (A \cap (B, +∞))$
	limclr.l	$⊢ φ \to L \in (({F ↾}_{(−∞, B)}) {lim}_{ℂ} B)$
	limclr.r	$⊢ φ \to R \in (({F ↾}_{(B, +∞)}) {lim}_{ℂ} B)$
Assertion	limclr	$⊢ φ \to ((F {lim}_{ℂ} B \neq \emptyset \leftrightarrow L = R) \land (L = R \to L \in (F {lim}_{ℂ} B)))$

Proof

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

Metamath Proof Explorer

Theorem limclr

Proof