Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 cncfiooiccre.x ⊢ Ⅎ 𝑥 𝜑
2 cncfiooiccre.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) )
3 cncfiooiccre.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4 cncfiooiccre.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5 cncfiooiccre.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
6 cncfiooiccre.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) )
7 cncfiooiccre.l ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 limℂ 𝐵 ) )
8 cncfiooiccre.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 limℂ 𝐴 ) )
9 iftrue ⊢ ( 𝑥 = 𝐴 → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝑅 )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝑅 )
11 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
12 6 11 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
13 ioosscn ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℂ
14 13 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℂ )
15 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
16 4 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
17 15 16 3 5 lptioo1cn ⊢ ( 𝜑 → 𝐴 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 (,) 𝐵 ) ) )
18 12 14 17 8 limcrecl ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝑅 ∈ ℝ )
20 10 19 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℝ )
21 20 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℝ )
22 iffalse ⊢ ( ¬ 𝑥 = 𝐴 → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) )
23 iftrue ⊢ ( 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = 𝐿 )
24 22 23 sylan9eq ⊢ ( ( ¬ 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝐿 )
25 24 adantll ⊢ ( ( ( 𝜑 ∧ ¬ 𝑥 = 𝐴 ) ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = 𝐿 )
26 3 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
27 15 26 4 5 lptioo2cn ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 (,) 𝐵 ) ) )
28 12 14 27 7 limcrecl ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
29 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑥 = 𝐴 ) ∧ 𝑥 = 𝐵 ) → 𝐿 ∈ ℝ )
30 25 29 eqeltrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑥 = 𝐴 ) ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℝ )
31 30 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℝ )
32 iffalse ⊢ ( ¬ 𝑥 = 𝐵 → if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
33 22 32 sylan9eq ⊢ ( ( ¬ 𝑥 = 𝐴 ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
34 33 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
35 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
36 26 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐴 ∈ ℝ* )
37 16 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐵 ∈ ℝ* )
38 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ∈ ℝ )
39 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ )
40 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
41 eliccre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℝ )
42 38 39 40 41 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℝ )
43 42 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ∈ ℝ )
44 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝐴 ∈ ℝ )
45 42 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝑥 ∈ ℝ )
46 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝐴 ∈ ℝ* )
47 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝐵 ∈ ℝ* )
48 40 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
49 iccgelb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ 𝑥 )
50 46 47 48 49 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝐴 ≤ 𝑥 )
51 neqne ⊢ ( ¬ 𝑥 = 𝐴 → 𝑥 ≠ 𝐴 )
52 51 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝑥 ≠ 𝐴 )
53 44 45 50 52 leneltd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → 𝐴 < 𝑥 )
54 53 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐴 < 𝑥 )
55 42 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ∈ ℝ )
56 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐵 ∈ ℝ )
57 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐴 ∈ ℝ* )
58 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐵 ∈ ℝ* )
59 40 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
60 iccleub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ≤ 𝐵 )
61 57 58 59 60 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ≤ 𝐵 )
62 neqne ⊢ ( ¬ 𝑥 = 𝐵 → 𝑥 ≠ 𝐵 )
63 62 necomd ⊢ ( ¬ 𝑥 = 𝐵 → 𝐵 ≠ 𝑥 )
64 63 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝐵 ≠ 𝑥 )
65 55 56 61 64 leneltd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 < 𝐵 )
66 65 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 < 𝐵 )
67 36 37 43 54 66 eliood ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
68 35 67 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
69 34 68 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) ∧ ¬ 𝑥 = 𝐵 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℝ )
70 31 69 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑥 = 𝐴 ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℝ )
71 21 70 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → if ( 𝑥 = 𝐴 , 𝑅 , if ( 𝑥 = 𝐵 , 𝐿 , ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℝ )
72 71 2 fmptd ⊢ ( 𝜑 → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
73 ax-resscn ⊢ ℝ ⊆ ℂ
74 ssid ⊢ ℂ ⊆ ℂ
75 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ⊆ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
76 73 74 75 mp2an ⊢ ( ( 𝐴 (,) 𝐵 ) –cn→ ℝ ) ⊆ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ )
77 76 6 sselid ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
78 1 2 3 4 77 7 8 cncfiooicc ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
79 cncffvrn ⊢ ( ( ℝ ⊆ ℂ ∧ 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ↔ 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ ) )
80 73 78 79 sylancr ⊢ ( 𝜑 → ( 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ↔ 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ ) )
81 72 80 mpbird ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )