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	⊢ Ⅎ 𝑥 𝜑
	cncfiooicc.g	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
	cncfiooicc.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	cncfiooicc.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	cncfiooicc.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
	cncfiooicc.l	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 lim_ℂ 𝐵 ) )
	cncfiooicc.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 lim_ℂ 𝐴 ) )
Assertion	cncfiooicc	⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		cncfiooicc.x	⊢ Ⅎ 𝑥 𝜑
2		cncfiooicc.g	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
3		cncfiooicc.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4		cncfiooicc.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5		cncfiooicc.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
6		cncfiooicc.l	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 lim_ℂ 𝐵 ) )
7		cncfiooicc.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 lim_ℂ 𝐴 ) )
8		nfv	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝐴 < 𝐵 )
9	3	adantr	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ )
10	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ )
11		simpr	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐴 < 𝐵 )
12	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
13	6	adantr	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐿 ∈ ( 𝐹 lim_ℂ 𝐵 ) )
14	7	adantr	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝑅 ∈ ( 𝐹 lim_ℂ 𝐴 ) )
15	8 2 9 10 11 12 13 14	cncfiooicclem1	⊢ ( ( 𝜑 ∧ 𝐴 < 𝐵 ) → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
16		limccl	⊢ ( 𝐹 lim_ℂ 𝐴 ) ⊆ ℂ
17	16 7	sselid	⊢ ( 𝜑 → 𝑅 ∈ ℂ )
18	17	snssd	⊢ ( 𝜑 → { 𝑅 } ⊆ ℂ )
19		ssid	⊢ ℂ ⊆ ℂ
20	19	a1i	⊢ ( 𝜑 → ℂ ⊆ ℂ )
21		cncfss	⊢ ( ( { 𝑅 } ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( { 𝐴 } –cn→ { 𝑅 } ) ⊆ ( { 𝐴 } –cn→ ℂ ) )
22	18 20 21	syl2anc	⊢ ( 𝜑 → ( { 𝐴 } –cn→ { 𝑅 } ) ⊆ ( { 𝐴 } –cn→ ℂ ) )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( { 𝐴 } –cn→ { 𝑅 } ) ⊆ ( { 𝐴 } –cn→ ℂ ) )
24	3	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ^* )
25		iccid	⊢ ( 𝐴 ∈ ℝ^* → ( 𝐴 [,] 𝐴 ) = { 𝐴 } )
26	24 25	syl	⊢ ( 𝜑 → ( 𝐴 [,] 𝐴 ) = { 𝐴 } )
27		oveq2	⊢ ( 𝐴 = 𝐵 → ( 𝐴 [,] 𝐴 ) = ( 𝐴 [,] 𝐵 ) )
28	26 27	sylan9req	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → { 𝐴 } = ( 𝐴 [,] 𝐵 ) )
29	28	eqcomd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝐴 [,] 𝐵 ) = { 𝐴 } )
30		simpr	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
31	29	adantr	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 [,] 𝐵 ) = { 𝐴 } )
32	30 31	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ { 𝐴 } )
33		elsni	⊢ ( 𝑥 ∈ { 𝐴 } → 𝑥 = 𝐴 )
34	32 33	syl	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 = 𝐴 )
35	34	iftrued	⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝑅 )
36	29 35	mpteq12dva	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝐴 } ↦ 𝑅 ) )
37	2 36	eqtrid	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐺 = ( 𝑥 ∈ { 𝐴 } ↦ 𝑅 ) )
38	3	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
39	38	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ ℂ )
40	17	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝑅 ∈ ℂ )
41		cncfdmsn	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( 𝑥 ∈ { 𝐴 } ↦ 𝑅 ) ∈ ( { 𝐴 } –cn→ { 𝑅 } ) )
42	39 40 41	syl2anc	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( 𝑥 ∈ { 𝐴 } ↦ 𝑅 ) ∈ ( { 𝐴 } –cn→ { 𝑅 } ) )
43	37 42	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐺 ∈ ( { 𝐴 } –cn→ { 𝑅 } ) )
44	23 43	sseldd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐺 ∈ ( { 𝐴 } –cn→ ℂ ) )
45	28	oveq1d	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( { 𝐴 } –cn→ ℂ ) = ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
46	44 45	eleqtrd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
47	46	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) ∧ 𝐴 = 𝐵 ) → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
48		simpll	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) → 𝜑 )
49		eqcom	⊢ ( 𝐵 = 𝐴 ↔ 𝐴 = 𝐵 )
50	49	biimpi	⊢ ( 𝐵 = 𝐴 → 𝐴 = 𝐵 )
51	50	con3i	⊢ ( ¬ 𝐴 = 𝐵 → ¬ 𝐵 = 𝐴 )
52	51	adantl	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) → ¬ 𝐵 = 𝐴 )
53		simplr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) → ¬ 𝐴 < 𝐵 )
54		pm4.56	⊢ ( ( ¬ 𝐵 = 𝐴 ∧ ¬ 𝐴 < 𝐵 ) ↔ ¬ ( 𝐵 = 𝐴 ∨ 𝐴 < 𝐵 ) )
55	54	biimpi	⊢ ( ( ¬ 𝐵 = 𝐴 ∧ ¬ 𝐴 < 𝐵 ) → ¬ ( 𝐵 = 𝐴 ∨ 𝐴 < 𝐵 ) )
56	52 53 55	syl2anc	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) → ¬ ( 𝐵 = 𝐴 ∨ 𝐴 < 𝐵 ) )
57	48 4	syl	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) → 𝐵 ∈ ℝ )
58	48 3	syl	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) → 𝐴 ∈ ℝ )
59	57 58	lttrid	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) → ( 𝐵 < 𝐴 ↔ ¬ ( 𝐵 = 𝐴 ∨ 𝐴 < 𝐵 ) ) )
60	56 59	mpbird	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) → 𝐵 < 𝐴 )
61		0ss	⊢ ∅ ⊆ ℂ
62		eqid	⊢ ( TopOpen ‘ ℂ_fld ) = ( TopOpen ‘ ℂ_fld )
63	62	cnfldtop	⊢ ( TopOpen ‘ ℂ_fld ) ∈ Top
64		rest0	⊢ ( ( TopOpen ‘ ℂ_fld ) ∈ Top → ( ( TopOpen ‘ ℂ_fld ) ↾_t ∅ ) = { ∅ } )
65	63 64	ax-mp	⊢ ( ( TopOpen ‘ ℂ_fld ) ↾_t ∅ ) = { ∅ }
66	65	eqcomi	⊢ { ∅ } = ( ( TopOpen ‘ ℂ_fld ) ↾_t ∅ )
67	62 66 66	cncfcn	⊢ ( ( ∅ ⊆ ℂ ∧ ∅ ⊆ ℂ ) → ( ∅ –cn→ ∅ ) = ( { ∅ } Cn { ∅ } ) )
68	61 61 67	mp2an	⊢ ( ∅ –cn→ ∅ ) = ( { ∅ } Cn { ∅ } )
69		cncfss	⊢ ( ( ∅ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ∅ –cn→ ∅ ) ⊆ ( ∅ –cn→ ℂ ) )
70	61 19 69	mp2an	⊢ ( ∅ –cn→ ∅ ) ⊆ ( ∅ –cn→ ℂ )
71	68 70	eqsstrri	⊢ ( { ∅ } Cn { ∅ } ) ⊆ ( ∅ –cn→ ℂ )
72	2	a1i	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ) )
73		simpr	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → 𝐵 < 𝐴 )
74	24	adantr	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → 𝐴 ∈ ℝ^* )
75	4	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ^* )
76	75	adantr	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → 𝐵 ∈ ℝ^* )
77		icc0	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
78	74 76 77	syl2anc	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
79	73 78	mpbird	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ( 𝐴 [,] 𝐵 ) = ∅ )
80	79	mpteq1d	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ∅ ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ) )
81		mpt0	⊢ ( 𝑥 ∈ ∅ ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ) = ∅
82	81	a1i	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ( 𝑥 ∈ ∅ ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ) = ∅ )
83	72 80 82	3eqtrd	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → 𝐺 = ∅ )
84		0cnf	⊢ ∅ ∈ ( { ∅ } Cn { ∅ } )
85	83 84	eqeltrdi	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → 𝐺 ∈ ( { ∅ } Cn { ∅ } ) )
86	71 85	sselid	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → 𝐺 ∈ ( ∅ –cn→ ℂ ) )
87	79	eqcomd	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ∅ = ( 𝐴 [,] 𝐵 ) )
88	87	oveq1d	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ( ∅ –cn→ ℂ ) = ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
89	86 88	eleqtrd	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
90	48 60 89	syl2anc	⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
91	47 90	pm2.61dan	⊢ ( ( 𝜑 ∧ ¬ 𝐴 < 𝐵 ) → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
92	15 91	pm2.61dan	⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )

Metamath Proof Explorer

Theorem cncfiooicc

Proof