cncfiooiccre

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 is assumed to be real-valued. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		cncfiooiccre.x	$⊢ Ⅎ x φ$
2		cncfiooiccre.g	$⊢ G = (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x))))$
3		cncfiooiccre.a	$⊢ φ \to A \in ℝ$
4		cncfiooiccre.b	$⊢ φ \to B \in ℝ$
5		cncfiooiccre.altb	$⊢ φ \to A < B$
6		cncfiooiccre.f	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℝ$
7		cncfiooiccre.l	$⊢ φ \to L \in (F {lim}_{ℂ} B)$
8		cncfiooiccre.r	$⊢ φ \to R \in (F {lim}_{ℂ} A)$
9		iftrue	$⊢ x = A \to if (x = A, R, if (x = B, L, F (x))) = R$
10	9	adantl	$⊢ (φ \land x = A) \to if (x = A, R, if (x = B, L, F (x))) = R$
11		cncff	$⊢ F : (A, B) \underset{cn}{⟶} ℝ \to F : (A, B) ⟶ ℝ$
12	6 11	syl	$⊢ φ \to F : (A, B) ⟶ ℝ$
13		ioosscn	$⊢ (A, B) \subseteq ℂ$
14	13	a1i	$⊢ φ \to (A, B) \subseteq ℂ$
15		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
16	4	rexrd	$⊢ φ \to B \in ℝ^{*}$
17	15 16 3 5	lptioo1cn	$⊢ φ \to A \in limPt (TopOpen (ℂ_{fld})) ((A, B))$
18	12 14 17 8	limcrecl	$⊢ φ \to R \in ℝ$
19	18	adantr	$⊢ (φ \land x = A) \to R \in ℝ$
20	10 19	eqeltrd	$⊢ (φ \land x = A) \to if (x = A, R, if (x = B, L, F (x))) \in ℝ$
21	20	adantlr	$⊢ ((φ \land x \in [A, B]) \land x = A) \to if (x = A, R, if (x = B, L, F (x))) \in ℝ$
22		iffalse	$⊢ \neg x = A \to if (x = A, R, if (x = B, L, F (x))) = if (x = B, L, F (x))$
23		iftrue	$⊢ x = B \to if (x = B, L, F (x)) = L$
24	22 23	sylan9eq	$⊢ (\neg x = A \land x = B) \to if (x = A, R, if (x = B, L, F (x))) = L$
25	24	adantll	$⊢ ((φ \land \neg x = A) \land x = B) \to if (x = A, R, if (x = B, L, F (x))) = L$
26	3	rexrd	$⊢ φ \to A \in ℝ^{*}$
27	15 26 4 5	lptioo2cn	$⊢ φ \to B \in limPt (TopOpen (ℂ_{fld})) ((A, B))$
28	12 14 27 7	limcrecl	$⊢ φ \to L \in ℝ$
29	28	ad2antrr	$⊢ ((φ \land \neg x = A) \land x = B) \to L \in ℝ$
30	25 29	eqeltrd	$⊢ ((φ \land \neg x = A) \land x = B) \to if (x = A, R, if (x = B, L, F (x))) \in ℝ$
31	30	adantllr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land x = B) \to if (x = A, R, if (x = B, L, F (x))) \in ℝ$
32		iffalse	$⊢ \neg x = B \to if (x = B, L, F (x)) = F (x)$
33	22 32	sylan9eq	$⊢ (\neg x = A \land \neg x = B) \to if (x = A, R, if (x = B, L, F (x))) = F (x)$
34	33	adantll	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to if (x = A, R, if (x = B, L, F (x))) = F (x)$
35	12	ad3antrrr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to F : (A, B) ⟶ ℝ$
36	26	ad3antrrr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to A \in ℝ^{*}$
37	16	ad3antrrr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to B \in ℝ^{*}$
38	3	adantr	$⊢ (φ \land x \in [A, B]) \to A \in ℝ$
39	4	adantr	$⊢ (φ \land x \in [A, B]) \to B \in ℝ$
40		simpr	$⊢ (φ \land x \in [A, B]) \to x \in [A, B]$
41		eliccre	$⊢ (A \in ℝ \land B \in ℝ \land x \in [A, B]) \to x \in ℝ$
42	38 39 40 41	syl3anc	$⊢ (φ \land x \in [A, B]) \to x \in ℝ$
43	42	ad2antrr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to x \in ℝ$
44	3	ad2antrr	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to A \in ℝ$
45	42	adantr	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to x \in ℝ$
46	26	ad2antrr	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to A \in ℝ^{*}$
47	16	ad2antrr	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to B \in ℝ^{*}$
48	40	adantr	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to x \in [A, B]$
49		iccgelb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land x \in [A, B]) \to A \leq x$
50	46 47 48 49	syl3anc	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to A \leq x$
51		neqne	$⊢ \neg x = A \to x \neq A$
52	51	adantl	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to x \neq A$
53	44 45 50 52	leneltd	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to A < x$
54	53	adantr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to A < x$
55	42	adantr	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to x \in ℝ$
56	4	ad2antrr	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to B \in ℝ$
57	26	ad2antrr	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to A \in ℝ^{*}$
58	16	ad2antrr	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to B \in ℝ^{*}$
59	40	adantr	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to x \in [A, B]$
60		iccleub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land x \in [A, B]) \to x \leq B$
61	57 58 59 60	syl3anc	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to x \leq B$
62		neqne	$⊢ \neg x = B \to x \neq B$
63	62	necomd	$⊢ \neg x = B \to B \neq x$
64	63	adantl	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to B \neq x$
65	55 56 61 64	leneltd	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to x < B$
66	65	adantlr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to x < B$
67	36 37 43 54 66	eliood	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to x \in (A, B)$
68	35 67	ffvelrnd	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to F (x) \in ℝ$
69	34 68	eqeltrd	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to if (x = A, R, if (x = B, L, F (x))) \in ℝ$
70	31 69	pm2.61dan	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to if (x = A, R, if (x = B, L, F (x))) \in ℝ$
71	21 70	pm2.61dan	$⊢ (φ \land x \in [A, B]) \to if (x = A, R, if (x = B, L, F (x))) \in ℝ$
72	71 2	fmptd	$⊢ φ \to G : [A, B] ⟶ ℝ$
73		ax-resscn	$⊢ ℝ \subseteq ℂ$
74		ssid	$⊢ ℂ \subseteq ℂ$
75		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to (A, B) \underset{cn}{⟶} ℝ \subseteq (A, B) \underset{cn}{⟶} ℂ$
76	73 74 75	mp2an	$⊢ (A, B) \underset{cn}{⟶} ℝ \subseteq (A, B) \underset{cn}{⟶} ℂ$
77	76 6	sseldi	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
78	1 2 3 4 77 7 8	cncfiooicc	$⊢ φ \to G : [A, B] \underset{cn}{⟶} ℂ$
79		cncffvrn	$⊢ (ℝ \subseteq ℂ \land G : [A, B] \underset{cn}{⟶} ℂ) \to (G : [A, B] \underset{cn}{⟶} ℝ \leftrightarrow G : [A, B] ⟶ ℝ)$
80	73 78 79	sylancr	$⊢ φ \to (G : [A, B] \underset{cn}{⟶} ℝ \leftrightarrow G : [A, B] ⟶ ℝ)$
81	72 80	mpbird	$⊢ φ \to G : [A, B] \underset{cn}{⟶} ℝ$

Metamath Proof Explorer

Theorem cncfiooiccre

Proof