ioccncflimc

Description: Limit at the upper bound of a continuous function defined on a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	ioccncflimc.a	$⊢ φ \to A \in ℝ^{*}$
	ioccncflimc.b	$⊢ φ \to B \in ℝ$
	ioccncflimc.altb	$⊢ φ \to A < B$
	ioccncflimc.f	$⊢ φ \to F : (A, B] \underset{cn}{⟶} ℂ$
Assertion	ioccncflimc	$⊢ φ \to F (B) \in (({F ↾}_{(A, B)}) {lim}_{ℂ} B)$

Proof

Step	Hyp	Ref	Expression
1		ioccncflimc.a	$⊢ φ \to A \in ℝ^{*}$
2		ioccncflimc.b	$⊢ φ \to B \in ℝ$
3		ioccncflimc.altb	$⊢ φ \to A < B$
4		ioccncflimc.f	$⊢ φ \to F : (A, B] \underset{cn}{⟶} ℂ$
5	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
6	2	leidd	$⊢ φ \to B \leq B$
7	1 5 5 3 6	eliocd	$⊢ φ \to B \in (A, B]$
8	4 7	cnlimci	$⊢ φ \to F (B) \in (F {lim}_{ℂ} B)$
9		cncfrss	$⊢ F : (A, B] \underset{cn}{⟶} ℂ \to (A, B] \subseteq ℂ$
10	4 9	syl	$⊢ φ \to (A, B] \subseteq ℂ$
11		ssid	$⊢ ℂ \subseteq ℂ$
12		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
13		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B] = TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B]$
14		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
15	12 13 14	cncfcn	$⊢ ((A, B] \subseteq ℂ \land ℂ \subseteq ℂ) \to (A, B] \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)$
16	10 11 15	sylancl	$⊢ φ \to (A, B] \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)$
17	4 16	eleqtrd	$⊢ φ \to F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ))$
18	12	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
19		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land (A, B] \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B] \in TopOn ((A, B])$
20	18 10 19	sylancr	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B] \in TopOn ((A, B])$
21	12	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
22		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
23	22	restid	$⊢ TopOpen (ℂ_{fld}) \in Top \to TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
24	21 23	ax-mp	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
25	24	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ \in TopOn (ℂ)$
26		cncnp	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B] \in TopOn ((A, B]) \land TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ \in TopOn (ℂ)) \to (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)) \leftrightarrow (F : (A, B] ⟶ ℂ \land \forall x \in (A, B] F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B]) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)) (x)))$
27	20 25 26	sylancl	$⊢ φ \to (F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B]) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)) \leftrightarrow (F : (A, B] ⟶ ℂ \land \forall x \in (A, B] F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B]) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)) (x)))$
28	17 27	mpbid	$⊢ φ \to (F : (A, B] ⟶ ℂ \land \forall x \in (A, B] F \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B]) CnP (TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ)) (x))$
29	28	simpld	$⊢ φ \to F : (A, B] ⟶ ℂ$
30		ioossioc	$⊢ (A, B) \subseteq (A, B]$
31	30	a1i	$⊢ φ \to (A, B) \subseteq (A, B]$
32		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B] \cup \{B\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B] \cup \{B\})$
33	2	recnd	$⊢ φ \to B \in ℂ$
34	22	ntrtop	$⊢ TopOpen (ℂ_{fld}) \in Top \to int (TopOpen (ℂ_{fld})) (ℂ) = ℂ$
35	21 34	ax-mp	$⊢ int (TopOpen (ℂ_{fld})) (ℂ) = ℂ$
36		undif	$⊢ (A, B] \subseteq ℂ \leftrightarrow (A, B] \cup (ℂ ∖ (A, B]) = ℂ$
37	10 36	sylib	$⊢ φ \to (A, B] \cup (ℂ ∖ (A, B]) = ℂ$
38	37	eqcomd	$⊢ φ \to ℂ = (A, B] \cup (ℂ ∖ (A, B])$
39	38	fveq2d	$⊢ φ \to int (TopOpen (ℂ_{fld})) (ℂ) = int (TopOpen (ℂ_{fld})) ((A, B] \cup (ℂ ∖ (A, B]))$
40	35 39	eqtr3id	$⊢ φ \to ℂ = int (TopOpen (ℂ_{fld})) ((A, B] \cup (ℂ ∖ (A, B]))$
41	33 40	eleqtrd	$⊢ φ \to B \in int (TopOpen (ℂ_{fld})) ((A, B] \cup (ℂ ∖ (A, B]))$
42	41 7	elind	$⊢ φ \to B \in (int (TopOpen (ℂ_{fld})) ((A, B] \cup (ℂ ∖ (A, B])) \cap (A, B])$
43	21	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in Top$
44		ssid	$⊢ (A, B] \subseteq (A, B]$
45	44	a1i	$⊢ φ \to (A, B] \subseteq (A, B]$
46	22 13	restntr	$⊢ (TopOpen (ℂ_{fld}) \in Top \land (A, B] \subseteq ℂ \land (A, B] \subseteq (A, B]) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B]) ((A, B]) = int (TopOpen (ℂ_{fld})) ((A, B] \cup (ℂ ∖ (A, B])) \cap (A, B]$
47	43 10 45 46	syl3anc	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B]) ((A, B]) = int (TopOpen (ℂ_{fld})) ((A, B] \cup (ℂ ∖ (A, B])) \cap (A, B]$
48	42 47	eleqtrrd	$⊢ φ \to B \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B]) ((A, B])$
49	7	snssd	$⊢ φ \to \{B\} \subseteq (A, B]$
50		ssequn2	$⊢ \{B\} \subseteq (A, B] \leftrightarrow (A, B] \cup \{B\} = (A, B]$
51	49 50	sylib	$⊢ φ \to (A, B] \cup \{B\} = (A, B]$
52	51	eqcomd	$⊢ φ \to (A, B] = (A, B] \cup \{B\}$
53	52	oveq2d	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B] = TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B] \cup \{B\})$
54	53	fveq2d	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B]) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B] \cup \{B\}))$
55		ioounsn	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to (A, B) \cup \{B\} = (A, B]$
56	1 5 3 55	syl3anc	$⊢ φ \to (A, B) \cup \{B\} = (A, B]$
57	56	eqcomd	$⊢ φ \to (A, B] = (A, B) \cup \{B\}$
58	54 57	fveq12d	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} (A, B]) ((A, B]) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B] \cup \{B\})) ((A, B) \cup \{B\})$
59	48 58	eleqtrd	$⊢ φ \to B \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((A, B] \cup \{B\})) ((A, B) \cup \{B\})$
60	29 31 10 12 32 59	limcres	$⊢ φ \to ({F ↾}_{(A, B)}) {lim}_{ℂ} B = F {lim}_{ℂ} B$
61	8 60	eleqtrrd	$⊢ φ \to F (B) \in (({F ↾}_{(A, B)}) {lim}_{ℂ} B)$

Metamath Proof Explorer

Theorem ioccncflimc

Proof