limciccioolb

Description: The limit of a function at the lower bound of a closed interval only depends on the values in the inner open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	limciccioolb.1	$⊢ φ \to A \in ℝ$
	limciccioolb.2	$⊢ φ \to B \in ℝ$
	limciccioolb.3	$⊢ φ \to A < B$
	limciccioolb.4	$⊢ φ \to F : [A, B] ⟶ ℂ$
Assertion	limciccioolb	$⊢ φ \to ({F ↾}_{(A, B)}) {lim}_{ℂ} A = F {lim}_{ℂ} A$

Proof

Step	Hyp	Ref	Expression
1		limciccioolb.1	$⊢ φ \to A \in ℝ$
2		limciccioolb.2	$⊢ φ \to B \in ℝ$
3		limciccioolb.3	$⊢ φ \to A < B$
4		limciccioolb.4	$⊢ φ \to F : [A, B] ⟶ ℂ$
5		ioossicc	$⊢ (A, B) \subseteq [A, B]$
6	5	a1i	$⊢ φ \to (A, B) \subseteq [A, B]$
7	1 2	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
8		ax-resscn	$⊢ ℝ \subseteq ℂ$
9	7 8	sstrdi	$⊢ φ \to [A, B] \subseteq ℂ$
10		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
11		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ([A, B] \cup \{A\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ([A, B] \cup \{A\})$
12		retop	$⊢ topGen (ran (.)) \in Top$
13	12	a1i	$⊢ φ \to topGen (ran (.)) \in Top$
14	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
15		icossre	$⊢ (A \in ℝ \land B \in ℝ^{*}) \to [A, B) \subseteq ℝ$
16	1 14 15	syl2anc	$⊢ φ \to [A, B) \subseteq ℝ$
17		difssd	$⊢ φ \to ℝ ∖ [A, B] \subseteq ℝ$
18	16 17	unssd	$⊢ φ \to [A, B) \cup (ℝ ∖ [A, B]) \subseteq ℝ$
19		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
20	18 19	sseqtrdi	$⊢ φ \to [A, B) \cup (ℝ ∖ [A, B]) \subseteq ⋃ topGen (ran (.))$
21		elioore	$⊢ x \in (−∞, B) \to x \in ℝ$
22	21	ad2antlr	$⊢ ((φ \land x \in (−∞, B)) \land A \leq x) \to x \in ℝ$
23		simpr	$⊢ ((φ \land x \in (−∞, B)) \land A \leq x) \to A \leq x$
24		simpr	$⊢ (φ \land x \in (−∞, B)) \to x \in (−∞, B)$
25		mnfxr	$⊢ −∞ \in ℝ^{*}$
26	25	a1i	$⊢ (φ \land x \in (−∞, B)) \to −∞ \in ℝ^{*}$
27	14	adantr	$⊢ (φ \land x \in (−∞, B)) \to B \in ℝ^{*}$
28		elioo2	$⊢ (−∞ \in ℝ^{} \land B \in ℝ^{}) \to (x \in (−∞, B) \leftrightarrow (x \in ℝ \land −∞ < x \land x < B))$
29	26 27 28	syl2anc	$⊢ (φ \land x \in (−∞, B)) \to (x \in (−∞, B) \leftrightarrow (x \in ℝ \land −∞ < x \land x < B))$
30	24 29	mpbid	$⊢ (φ \land x \in (−∞, B)) \to (x \in ℝ \land −∞ < x \land x < B)$
31	30	simp3d	$⊢ (φ \land x \in (−∞, B)) \to x < B$
32	31	adantr	$⊢ ((φ \land x \in (−∞, B)) \land A \leq x) \to x < B$
33	1	ad2antrr	$⊢ ((φ \land x \in (−∞, B)) \land A \leq x) \to A \in ℝ$
34	14	ad2antrr	$⊢ ((φ \land x \in (−∞, B)) \land A \leq x) \to B \in ℝ^{*}$
35		elico2	$⊢ (A \in ℝ \land B \in ℝ^{*}) \to (x \in [A, B) \leftrightarrow (x \in ℝ \land A \leq x \land x < B))$
36	33 34 35	syl2anc	$⊢ ((φ \land x \in (−∞, B)) \land A \leq x) \to (x \in [A, B) \leftrightarrow (x \in ℝ \land A \leq x \land x < B))$
37	22 23 32 36	mpbir3and	$⊢ ((φ \land x \in (−∞, B)) \land A \leq x) \to x \in [A, B)$
38	37	orcd	$⊢ ((φ \land x \in (−∞, B)) \land A \leq x) \to (x \in [A, B) \lor x \in (ℝ ∖ [A, B]))$
39	21	ad2antlr	$⊢ ((φ \land x \in (−∞, B)) \land \neg A \leq x) \to x \in ℝ$
40		simpr	$⊢ ((φ \land x \in (−∞, B)) \land \neg A \leq x) \to \neg A \leq x$
41	40	intnanrd	$⊢ ((φ \land x \in (−∞, B)) \land \neg A \leq x) \to \neg (A \leq x \land x \leq B)$
42	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
43	42	ad2antrr	$⊢ ((φ \land x \in (−∞, B)) \land \neg A \leq x) \to A \in ℝ^{*}$
44	14	ad2antrr	$⊢ ((φ \land x \in (−∞, B)) \land \neg A \leq x) \to B \in ℝ^{*}$
45	39	rexrd	$⊢ ((φ \land x \in (−∞, B)) \land \neg A \leq x) \to x \in ℝ^{*}$
46		elicc4	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land x \in ℝ^{*}) \to (x \in [A, B] \leftrightarrow (A \leq x \land x \leq B))$
47	43 44 45 46	syl3anc	$⊢ ((φ \land x \in (−∞, B)) \land \neg A \leq x) \to (x \in [A, B] \leftrightarrow (A \leq x \land x \leq B))$
48	41 47	mtbird	$⊢ ((φ \land x \in (−∞, B)) \land \neg A \leq x) \to \neg x \in [A, B]$
49	39 48	eldifd	$⊢ ((φ \land x \in (−∞, B)) \land \neg A \leq x) \to x \in (ℝ ∖ [A, B])$
50	49	olcd	$⊢ ((φ \land x \in (−∞, B)) \land \neg A \leq x) \to (x \in [A, B) \lor x \in (ℝ ∖ [A, B]))$
51	38 50	pm2.61dan	$⊢ (φ \land x \in (−∞, B)) \to (x \in [A, B) \lor x \in (ℝ ∖ [A, B]))$
52		elun	$⊢ x \in ([A, B) \cup (ℝ ∖ [A, B])) \leftrightarrow (x \in [A, B) \lor x \in (ℝ ∖ [A, B]))$
53	51 52	sylibr	$⊢ (φ \land x \in (−∞, B)) \to x \in ([A, B) \cup (ℝ ∖ [A, B]))$
54	53	ralrimiva	$⊢ φ \to \forall x \in (−∞, B) x \in ([A, B) \cup (ℝ ∖ [A, B]))$
55		dfss3	$⊢ (−∞, B) \subseteq [A, B) \cup (ℝ ∖ [A, B]) \leftrightarrow \forall x \in (−∞, B) x \in ([A, B) \cup (ℝ ∖ [A, B]))$
56	54 55	sylibr	$⊢ φ \to (−∞, B) \subseteq [A, B) \cup (ℝ ∖ [A, B])$
57		eqid	$⊢ ⋃ topGen (ran (.)) = ⋃ topGen (ran (.))$
58	57	ntrss	$⊢ (topGen (ran (.)) \in Top \land [A, B) \cup (ℝ ∖ [A, B]) \subseteq ⋃ topGen (ran (.)) \land (−∞, B) \subseteq [A, B) \cup (ℝ ∖ [A, B])) \to int (topGen (ran (.))) ((−∞, B)) \subseteq int (topGen (ran (.))) ([A, B) \cup (ℝ ∖ [A, B]))$
59	13 20 56 58	syl3anc	$⊢ φ \to int (topGen (ran (.))) ((−∞, B)) \subseteq int (topGen (ran (.))) ([A, B) \cup (ℝ ∖ [A, B]))$
60	25	a1i	$⊢ φ \to −∞ \in ℝ^{*}$
61	1	mnfltd	$⊢ φ \to −∞ < A$
62	60 14 1 61 3	eliood	$⊢ φ \to A \in (−∞, B)$
63		iooretop	$⊢ (−∞, B) \in topGen (ran (.))$
64	63	a1i	$⊢ φ \to (−∞, B) \in topGen (ran (.))$
65		isopn3i	$⊢ (topGen (ran (.)) \in Top \land (−∞, B) \in topGen (ran (.))) \to int (topGen (ran (.))) ((−∞, B)) = (−∞, B)$
66	13 64 65	syl2anc	$⊢ φ \to int (topGen (ran (.))) ((−∞, B)) = (−∞, B)$
67	62 66	eleqtrrd	$⊢ φ \to A \in int (topGen (ran (.))) ((−∞, B))$
68	59 67	sseldd	$⊢ φ \to A \in int (topGen (ran (.))) ([A, B) \cup (ℝ ∖ [A, B]))$
69	1	leidd	$⊢ φ \to A \leq A$
70	1 2 3	ltled	$⊢ φ \to A \leq B$
71	1 2 1 69 70	eliccd	$⊢ φ \to A \in [A, B]$
72	68 71	elind	$⊢ φ \to A \in (int (topGen (ran (.))) ([A, B) \cup (ℝ ∖ [A, B])) \cap [A, B])$
73		icossicc	$⊢ [A, B) \subseteq [A, B]$
74	73	a1i	$⊢ φ \to [A, B) \subseteq [A, B]$
75		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [A, B] = topGen (ran (.)) ↾_{𝑡} [A, B]$
76	19 75	restntr	$⊢ (topGen (ran (.)) \in Top \land [A, B] \subseteq ℝ \land [A, B) \subseteq [A, B]) \to int (topGen (ran (.)) ↾_{𝑡} [A, B]) ([A, B)) = int (topGen (ran (.))) ([A, B) \cup (ℝ ∖ [A, B])) \cap [A, B]$
77	13 7 74 76	syl3anc	$⊢ φ \to int (topGen (ran (.)) ↾_{𝑡} [A, B]) ([A, B)) = int (topGen (ran (.))) ([A, B) \cup (ℝ ∖ [A, B])) \cap [A, B]$
78	72 77	eleqtrrd	$⊢ φ \to A \in int (topGen (ran (.)) ↾_{𝑡} [A, B]) ([A, B))$
79		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
80	10 79	rerest	$⊢ [A, B] \subseteq ℝ \to TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B] = topGen (ran (.)) ↾_{𝑡} [A, B]$
81	7 80	syl	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B] = topGen (ran (.)) ↾_{𝑡} [A, B]$
82	81	eqcomd	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [A, B] = TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]$
83	82	fveq2d	$⊢ φ \to int (topGen (ran (.)) ↾_{𝑡} [A, B]) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B])$
84	83	fveq1d	$⊢ φ \to int (topGen (ran (.)) ↾_{𝑡} [A, B]) ([A, B)) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ([A, B))$
85	78 84	eleqtrd	$⊢ φ \to A \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ([A, B))$
86	71	snssd	$⊢ φ \to \{A\} \subseteq [A, B]$
87		ssequn2	$⊢ \{A\} \subseteq [A, B] \leftrightarrow [A, B] \cup \{A\} = [A, B]$
88	86 87	sylib	$⊢ φ \to [A, B] \cup \{A\} = [A, B]$
89	88	eqcomd	$⊢ φ \to [A, B] = [A, B] \cup \{A\}$
90	89	oveq2d	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B] = TopOpen (ℂ_{fld}) ↾_{𝑡} ([A, B] \cup \{A\})$
91	90	fveq2d	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ([A, B] \cup \{A\}))$
92		uncom	$⊢ (A, B) \cup \{A\} = \{A\} \cup (A, B)$
93		snunioo	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to \{A\} \cup (A, B) = [A, B)$
94	42 14 3 93	syl3anc	$⊢ φ \to \{A\} \cup (A, B) = [A, B)$
95	92 94	syl5req	$⊢ φ \to [A, B) = (A, B) \cup \{A\}$
96	91 95	fveq12d	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ([A, B)) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ([A, B] \cup \{A\})) ((A, B) \cup \{A\})$
97	85 96	eleqtrd	$⊢ φ \to A \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ([A, B] \cup \{A\})) ((A, B) \cup \{A\})$
98	4 6 9 10 11 97	limcres	$⊢ φ \to ({F ↾}_{(A, B)}) {lim}_{ℂ} A = F {lim}_{ℂ} A$

Metamath Proof Explorer

Theorem limciccioolb

Proof