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→ ℂ ) )