limcicciooub

Description: The limit of a function at the upper 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	limcicciooub.1	$⊢ φ \to A \in ℝ$
	limcicciooub.2	$⊢ φ \to B \in ℝ$
	limcicciooub.3	$⊢ φ \to A < B$
	limcicciooub.4	$⊢ φ \to F : [A, B] ⟶ ℂ$
Assertion	limcicciooub	$⊢ φ \to ({F ↾}_{(A, B)}) {lim}_{ℂ} B = F {lim}_{ℂ} B$

Proof

Step	Hyp	Ref	Expression
1		limcicciooub.1	$⊢ φ \to A \in ℝ$
2		limcicciooub.2	$⊢ φ \to B \in ℝ$
3		limcicciooub.3	$⊢ φ \to A < B$
4		limcicciooub.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 \{B\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ([A, B] \cup \{B\})$
12		retop	$⊢ topGen (ran (.)) \in Top$
13	12	a1i	$⊢ φ \to topGen (ran (.)) \in Top$
14	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
15		iocssre	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A, B] \subseteq ℝ$
16	14 2 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 (A, +∞) \to x \in ℝ$
22	21	ad2antlr	$⊢ ((φ \land x \in (A, +∞)) \land x \leq B) \to x \in ℝ$
23		simplr	$⊢ ((φ \land x \in (A, +∞)) \land x \leq B) \to x \in (A, +∞)$
24	14	ad2antrr	$⊢ ((φ \land x \in (A, +∞)) \land x \leq B) \to A \in ℝ^{*}$
25		pnfxr	$⊢ +∞ \in ℝ^{*}$
26		elioo2	$⊢ (A \in ℝ^{} \land +∞ \in ℝ^{}) \to (x \in (A, +∞) \leftrightarrow (x \in ℝ \land A < x \land x < +∞))$
27	24 25 26	sylancl	$⊢ ((φ \land x \in (A, +∞)) \land x \leq B) \to (x \in (A, +∞) \leftrightarrow (x \in ℝ \land A < x \land x < +∞))$
28	23 27	mpbid	$⊢ ((φ \land x \in (A, +∞)) \land x \leq B) \to (x \in ℝ \land A < x \land x < +∞)$
29	28	simp2d	$⊢ ((φ \land x \in (A, +∞)) \land x \leq B) \to A < x$
30		simpr	$⊢ ((φ \land x \in (A, +∞)) \land x \leq B) \to x \leq B$
31	2	ad2antrr	$⊢ ((φ \land x \in (A, +∞)) \land x \leq B) \to B \in ℝ$
32		elioc2	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (x \in (A, B] \leftrightarrow (x \in ℝ \land A < x \land x \leq B))$
33	24 31 32	syl2anc	$⊢ ((φ \land x \in (A, +∞)) \land x \leq B) \to (x \in (A, B] \leftrightarrow (x \in ℝ \land A < x \land x \leq B))$
34	22 29 30 33	mpbir3and	$⊢ ((φ \land x \in (A, +∞)) \land x \leq B) \to x \in (A, B]$
35	34	orcd	$⊢ ((φ \land x \in (A, +∞)) \land x \leq B) \to (x \in (A, B] \lor x \in (ℝ ∖ [A, B]))$
36	21	ad2antlr	$⊢ ((φ \land x \in (A, +∞)) \land \neg x \leq B) \to x \in ℝ$
37		3mix3	$⊢ \neg x \leq B \to (\neg x \in ℝ \lor \neg A \leq x \lor \neg x \leq B)$
38		3ianor	$⊢ \neg (x \in ℝ \land A \leq x \land x \leq B) \leftrightarrow (\neg x \in ℝ \lor \neg A \leq x \lor \neg x \leq B)$
39	37 38	sylibr	$⊢ \neg x \leq B \to \neg (x \in ℝ \land A \leq x \land x \leq B)$
40	39	adantl	$⊢ ((φ \land x \in (A, +∞)) \land \neg x \leq B) \to \neg (x \in ℝ \land A \leq x \land x \leq B)$
41	1	ad2antrr	$⊢ ((φ \land x \in (A, +∞)) \land \neg x \leq B) \to A \in ℝ$
42	2	ad2antrr	$⊢ ((φ \land x \in (A, +∞)) \land \neg x \leq B) \to B \in ℝ$
43		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (x \in [A, B] \leftrightarrow (x \in ℝ \land A \leq x \land x \leq B))$
44	41 42 43	syl2anc	$⊢ ((φ \land x \in (A, +∞)) \land \neg x \leq B) \to (x \in [A, B] \leftrightarrow (x \in ℝ \land A \leq x \land x \leq B))$
45	40 44	mtbird	$⊢ ((φ \land x \in (A, +∞)) \land \neg x \leq B) \to \neg x \in [A, B]$
46	36 45	eldifd	$⊢ ((φ \land x \in (A, +∞)) \land \neg x \leq B) \to x \in (ℝ ∖ [A, B])$
47	46	olcd	$⊢ ((φ \land x \in (A, +∞)) \land \neg x \leq B) \to (x \in (A, B] \lor x \in (ℝ ∖ [A, B]))$
48	35 47	pm2.61dan	$⊢ (φ \land x \in (A, +∞)) \to (x \in (A, B] \lor x \in (ℝ ∖ [A, B]))$
49		elun	$⊢ x \in ((A, B] \cup (ℝ ∖ [A, B])) \leftrightarrow (x \in (A, B] \lor x \in (ℝ ∖ [A, B]))$
50	48 49	sylibr	$⊢ (φ \land x \in (A, +∞)) \to x \in ((A, B] \cup (ℝ ∖ [A, B]))$
51	50	ralrimiva	$⊢ φ \to \forall x \in (A, +∞) x \in ((A, B] \cup (ℝ ∖ [A, B]))$
52		dfss3	$⊢ (A, +∞) \subseteq (A, B] \cup (ℝ ∖ [A, B]) \leftrightarrow \forall x \in (A, +∞) x \in ((A, B] \cup (ℝ ∖ [A, B]))$
53	51 52	sylibr	$⊢ φ \to (A, +∞) \subseteq (A, B] \cup (ℝ ∖ [A, B])$
54		eqid	$⊢ ⋃ topGen (ran (.)) = ⋃ topGen (ran (.))$
55	54	ntrss	$⊢ (topGen (ran (.)) \in Top \land (A, B] \cup (ℝ ∖ [A, B]) \subseteq ⋃ topGen (ran (.)) \land (A, +∞) \subseteq (A, B] \cup (ℝ ∖ [A, B])) \to int (topGen (ran (.))) ((A, +∞)) \subseteq int (topGen (ran (.))) ((A, B] \cup (ℝ ∖ [A, B]))$
56	13 20 53 55	syl3anc	$⊢ φ \to int (topGen (ran (.))) ((A, +∞)) \subseteq int (topGen (ran (.))) ((A, B] \cup (ℝ ∖ [A, B]))$
57	25	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
58	2	ltpnfd	$⊢ φ \to B < +∞$
59	14 57 2 3 58	eliood	$⊢ φ \to B \in (A, +∞)$
60		iooretop	$⊢ (A, +∞) \in topGen (ran (.))$
61		isopn3i	$⊢ (topGen (ran (.)) \in Top \land (A, +∞) \in topGen (ran (.))) \to int (topGen (ran (.))) ((A, +∞)) = (A, +∞)$
62	13 60 61	sylancl	$⊢ φ \to int (topGen (ran (.))) ((A, +∞)) = (A, +∞)$
63	59 62	eleqtrrd	$⊢ φ \to B \in int (topGen (ran (.))) ((A, +∞))$
64	56 63	sseldd	$⊢ φ \to B \in int (topGen (ran (.))) ((A, B] \cup (ℝ ∖ [A, B]))$
65	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
66	1 2 3	ltled	$⊢ φ \to A \leq B$
67		ubicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \in [A, B]$
68	14 65 66 67	syl3anc	$⊢ φ \to B \in [A, B]$
69	64 68	elind	$⊢ φ \to B \in (int (topGen (ran (.))) ((A, B] \cup (ℝ ∖ [A, B])) \cap [A, B])$
70		iocssicc	$⊢ (A, B] \subseteq [A, B]$
71	70	a1i	$⊢ φ \to (A, B] \subseteq [A, B]$
72		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [A, B] = topGen (ran (.)) ↾_{𝑡} [A, B]$
73	19 72	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]$
74	13 7 71 73	syl3anc	$⊢ φ \to int (topGen (ran (.)) ↾_{𝑡} [A, B]) ((A, B]) = int (topGen (ran (.))) ((A, B] \cup (ℝ ∖ [A, B])) \cap [A, B]$
75	69 74	eleqtrrd	$⊢ φ \to B \in int (topGen (ran (.)) ↾_{𝑡} [A, B]) ((A, B])$
76		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
77	10 76	rerest	$⊢ [A, B] \subseteq ℝ \to TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B] = topGen (ran (.)) ↾_{𝑡} [A, B]$
78	7 77	syl	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B] = topGen (ran (.)) ↾_{𝑡} [A, B]$
79	78	eqcomd	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [A, B] = TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]$
80	79	fveq2d	$⊢ φ \to int (topGen (ran (.)) ↾_{𝑡} [A, B]) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B])$
81	80	fveq1d	$⊢ φ \to int (topGen (ran (.)) ↾_{𝑡} [A, B]) ((A, B]) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ((A, B])$
82	75 81	eleqtrd	$⊢ φ \to B \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ((A, B])$
83	68	snssd	$⊢ φ \to \{B\} \subseteq [A, B]$
84		ssequn2	$⊢ \{B\} \subseteq [A, B] \leftrightarrow [A, B] \cup \{B\} = [A, B]$
85	83 84	sylib	$⊢ φ \to [A, B] \cup \{B\} = [A, B]$
86	85	eqcomd	$⊢ φ \to [A, B] = [A, B] \cup \{B\}$
87	86	oveq2d	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B] = TopOpen (ℂ_{fld}) ↾_{𝑡} ([A, B] \cup \{B\})$
88	87	fveq2d	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ([A, B] \cup \{B\}))$
89		ioounsn	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to (A, B) \cup \{B\} = (A, B]$
90	14 65 3 89	syl3anc	$⊢ φ \to (A, B) \cup \{B\} = (A, B]$
91	90	eqcomd	$⊢ φ \to (A, B] = (A, B) \cup \{B\}$
92	88 91	fveq12d	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} [A, B]) ((A, B]) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ([A, B] \cup \{B\})) ((A, B) \cup \{B\})$
93	82 92	eleqtrd	$⊢ φ \to B \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ([A, B] \cup \{B\})) ((A, B) \cup \{B\})$
94	4 6 9 10 11 93	limcres	$⊢ φ \to ({F ↾}_{(A, B)}) {lim}_{ℂ} B = F {lim}_{ℂ} B$

Metamath Proof Explorer

Theorem limcicciooub

Proof