cncfiooicc

Description: A continuous function F on an open interval ( A (,) B ) can be extended to a continuous function G on the corresponding closed interval, if it has a finite right limit R in A and a finite left limit L in B . F can be complex-valued. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	cncfiooicc.x	$⊢ Ⅎ x φ$
	cncfiooicc.g	$⊢ G = (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x))))$
	cncfiooicc.a	$⊢ φ \to A \in ℝ$
	cncfiooicc.b	$⊢ φ \to B \in ℝ$
	cncfiooicc.f	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
	cncfiooicc.l	$⊢ φ \to L \in (F {lim}_{ℂ} B)$
	cncfiooicc.r	$⊢ φ \to R \in (F {lim}_{ℂ} A)$
Assertion	cncfiooicc	$⊢ φ \to G : [A, B] \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		cncfiooicc.x	$⊢ Ⅎ x φ$
2		cncfiooicc.g	$⊢ G = (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x))))$
3		cncfiooicc.a	$⊢ φ \to A \in ℝ$
4		cncfiooicc.b	$⊢ φ \to B \in ℝ$
5		cncfiooicc.f	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
6		cncfiooicc.l	$⊢ φ \to L \in (F {lim}_{ℂ} B)$
7		cncfiooicc.r	$⊢ φ \to R \in (F {lim}_{ℂ} A)$
8		nfv	$⊢ Ⅎ x (φ \land A < B)$
9	3	adantr	$⊢ (φ \land A < B) \to A \in ℝ$
10	4	adantr	$⊢ (φ \land A < B) \to B \in ℝ$
11		simpr	$⊢ (φ \land A < B) \to A < B$
12	5	adantr	$⊢ (φ \land A < B) \to F : (A, B) \underset{cn}{⟶} ℂ$
13	6	adantr	$⊢ (φ \land A < B) \to L \in (F {lim}_{ℂ} B)$
14	7	adantr	$⊢ (φ \land A < B) \to R \in (F {lim}_{ℂ} A)$
15	8 2 9 10 11 12 13 14	cncfiooicclem1	$⊢ (φ \land A < B) \to G : [A, B] \underset{cn}{⟶} ℂ$
16		limccl	$⊢ F {lim}_{ℂ} A \subseteq ℂ$
17	16 7	sselid	$⊢ φ \to R \in ℂ$
18	17	snssd	$⊢ φ \to \{R\} \subseteq ℂ$
19		ssid	$⊢ ℂ \subseteq ℂ$
20	19	a1i	$⊢ φ \to ℂ \subseteq ℂ$
21		cncfss	$⊢ (\{R\} \subseteq ℂ \land ℂ \subseteq ℂ) \to \{A\} \underset{cn}{⟶} \{R\} \subseteq \{A\} \underset{cn}{⟶} ℂ$
22	18 20 21	syl2anc	$⊢ φ \to \{A\} \underset{cn}{⟶} \{R\} \subseteq \{A\} \underset{cn}{⟶} ℂ$
23	22	adantr	$⊢ (φ \land A = B) \to \{A\} \underset{cn}{⟶} \{R\} \subseteq \{A\} \underset{cn}{⟶} ℂ$
24	3	rexrd	$⊢ φ \to A \in ℝ^{*}$
25		iccid	$⊢ A \in ℝ^{*} \to [A, A] = \{A\}$
26	24 25	syl	$⊢ φ \to [A, A] = \{A\}$
27		oveq2	$⊢ A = B \to [A, A] = [A, B]$
28	26 27	sylan9req	$⊢ (φ \land A = B) \to \{A\} = [A, B]$
29	28	eqcomd	$⊢ (φ \land A = B) \to [A, B] = \{A\}$
30		simpr	$⊢ ((φ \land A = B) \land x \in [A, B]) \to x \in [A, B]$
31	29	adantr	$⊢ ((φ \land A = B) \land x \in [A, B]) \to [A, B] = \{A\}$
32	30 31	eleqtrd	$⊢ ((φ \land A = B) \land x \in [A, B]) \to x \in \{A\}$
33		elsni	$⊢ x \in \{A\} \to x = A$
34	32 33	syl	$⊢ ((φ \land A = B) \land x \in [A, B]) \to x = A$
35	34	iftrued	$⊢ ((φ \land A = B) \land x \in [A, B]) \to if (x = A, R, if (x = B, L, F (x))) = R$
36	29 35	mpteq12dva	$⊢ (φ \land A = B) \to (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x)))) = (x \in \{A\} ⟼ R)$
37	2 36	syl5eq	$⊢ (φ \land A = B) \to G = (x \in \{A\} ⟼ R)$
38	3	recnd	$⊢ φ \to A \in ℂ$
39	38	adantr	$⊢ (φ \land A = B) \to A \in ℂ$
40	17	adantr	$⊢ (φ \land A = B) \to R \in ℂ$
41		cncfdmsn	$⊢ (A \in ℂ \land R \in ℂ) \to (x \in \{A\} ⟼ R) : \{A\} \underset{cn}{⟶} \{R\}$
42	39 40 41	syl2anc	$⊢ (φ \land A = B) \to (x \in \{A\} ⟼ R) : \{A\} \underset{cn}{⟶} \{R\}$
43	37 42	eqeltrd	$⊢ (φ \land A = B) \to G : \{A\} \underset{cn}{⟶} \{R\}$
44	23 43	sseldd	$⊢ (φ \land A = B) \to G : \{A\} \underset{cn}{⟶} ℂ$
45	28	oveq1d	$⊢ (φ \land A = B) \to \{A\} \underset{cn}{⟶} ℂ = [A, B] \underset{cn}{⟶} ℂ$
46	44 45	eleqtrd	$⊢ (φ \land A = B) \to G : [A, B] \underset{cn}{⟶} ℂ$
47	46	adantlr	$⊢ ((φ \land \neg A < B) \land A = B) \to G : [A, B] \underset{cn}{⟶} ℂ$
48		simpll	$⊢ ((φ \land \neg A < B) \land \neg A = B) \to φ$
49		eqcom	$⊢ B = A \leftrightarrow A = B$
50	49	biimpi	$⊢ B = A \to A = B$
51	50	con3i	$⊢ \neg A = B \to \neg B = A$
52	51	adantl	$⊢ ((φ \land \neg A < B) \land \neg A = B) \to \neg B = A$
53		simplr	$⊢ ((φ \land \neg A < B) \land \neg A = B) \to \neg A < B$
54		pm4.56	$⊢ (\neg B = A \land \neg A < B) \leftrightarrow \neg (B = A \lor A < B)$
55	54	biimpi	$⊢ (\neg B = A \land \neg A < B) \to \neg (B = A \lor A < B)$
56	52 53 55	syl2anc	$⊢ ((φ \land \neg A < B) \land \neg A = B) \to \neg (B = A \lor A < B)$
57	48 4	syl	$⊢ ((φ \land \neg A < B) \land \neg A = B) \to B \in ℝ$
58	48 3	syl	$⊢ ((φ \land \neg A < B) \land \neg A = B) \to A \in ℝ$
59	57 58	lttrid	$⊢ ((φ \land \neg A < B) \land \neg A = B) \to (B < A \leftrightarrow \neg (B = A \lor A < B))$
60	56 59	mpbird	$⊢ ((φ \land \neg A < B) \land \neg A = B) \to B < A$
61		0ss	$⊢ \emptyset \subseteq ℂ$
62		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
63	62	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
64		rest0	$⊢ TopOpen (ℂ_{fld}) \in Top \to TopOpen (ℂ_{fld}) ↾_{𝑡} \emptyset = \{\emptyset\}$
65	63 64	ax-mp	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} \emptyset = \{\emptyset\}$
66	65	eqcomi	$⊢ \{\emptyset\} = TopOpen (ℂ_{fld}) ↾_{𝑡} \emptyset$
67	62 66 66	cncfcn	$⊢ (\emptyset \subseteq ℂ \land \emptyset \subseteq ℂ) \to \emptyset \underset{cn}{⟶} \emptyset = \{\emptyset\} Cn \{\emptyset\}$
68	61 61 67	mp2an	$⊢ \emptyset \underset{cn}{⟶} \emptyset = \{\emptyset\} Cn \{\emptyset\}$
69		cncfss	$⊢ (\emptyset \subseteq ℂ \land ℂ \subseteq ℂ) \to \emptyset \underset{cn}{⟶} \emptyset \subseteq \emptyset \underset{cn}{⟶} ℂ$
70	61 19 69	mp2an	$⊢ \emptyset \underset{cn}{⟶} \emptyset \subseteq \emptyset \underset{cn}{⟶} ℂ$
71	68 70	eqsstrri	$⊢ \{\emptyset\} Cn \{\emptyset\} \subseteq \emptyset \underset{cn}{⟶} ℂ$
72	2	a1i	$⊢ (φ \land B < A) \to G = (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x))))$
73		simpr	$⊢ (φ \land B < A) \to B < A$
74	24	adantr	$⊢ (φ \land B < A) \to A \in ℝ^{*}$
75	4	rexrd	$⊢ φ \to B \in ℝ^{*}$
76	75	adantr	$⊢ (φ \land B < A) \to B \in ℝ^{*}$
77		icc0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ([A, B] = \emptyset \leftrightarrow B < A)$
78	74 76 77	syl2anc	$⊢ (φ \land B < A) \to ([A, B] = \emptyset \leftrightarrow B < A)$
79	73 78	mpbird	$⊢ (φ \land B < A) \to [A, B] = \emptyset$
80	79	mpteq1d	$⊢ (φ \land B < A) \to (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x)))) = (x \in \emptyset ⟼ if (x = A, R, if (x = B, L, F (x))))$
81		mpt0	$⊢ (x \in \emptyset ⟼ if (x = A, R, if (x = B, L, F (x)))) = \emptyset$
82	81	a1i	$⊢ (φ \land B < A) \to (x \in \emptyset ⟼ if (x = A, R, if (x = B, L, F (x)))) = \emptyset$
83	72 80 82	3eqtrd	$⊢ (φ \land B < A) \to G = \emptyset$
84		0cnf	$⊢ \emptyset \in (\{\emptyset\} Cn \{\emptyset\})$
85	83 84	eqeltrdi	$⊢ (φ \land B < A) \to G \in (\{\emptyset\} Cn \{\emptyset\})$
86	71 85	sselid	$⊢ (φ \land B < A) \to G : \emptyset \underset{cn}{⟶} ℂ$
87	79	eqcomd	$⊢ (φ \land B < A) \to \emptyset = [A, B]$
88	87	oveq1d	$⊢ (φ \land B < A) \to \emptyset \underset{cn}{⟶} ℂ = [A, B] \underset{cn}{⟶} ℂ$
89	86 88	eleqtrd	$⊢ (φ \land B < A) \to G : [A, B] \underset{cn}{⟶} ℂ$
90	48 60 89	syl2anc	$⊢ ((φ \land \neg A < B) \land \neg A = B) \to G : [A, B] \underset{cn}{⟶} ℂ$
91	47 90	pm2.61dan	$⊢ (φ \land \neg A < B) \to G : [A, B] \underset{cn}{⟶} ℂ$
92	15 91	pm2.61dan	$⊢ φ \to G : [A, B] \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem cncfiooicc

Proof