Metamath Proof Explorer

Theorem 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 sseldi ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
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 syl5eq ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐺 = ( 𝑥 ∈ { 𝐴 } ↦ 𝑅 ) )
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 sseldi ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → 𝐺 ∈ ( ∅ –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→ ℂ ) )