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	$⊢ φ \to F : A ⟶ ℝ$
	limcrecl.2	$⊢ φ \to A \subseteq ℂ$
	limcrecl.3	$⊢ φ \to B \in limPt (TopOpen (ℂ_{fld})) (A)$
	limcrecl.4	$⊢ φ \to L \in (F {lim}_{ℂ} B)$
Assertion	limcrecl	$⊢ φ \to L \in ℝ$

Proof

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

Metamath Proof Explorer

Theorem limcrecl

Proof