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 
|- F/ x ph
cncfiooiccre.g 
|- G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
cncfiooiccre.a 
|- ( ph -> A e. RR )
cncfiooiccre.b 
|- ( ph -> B e. RR )
cncfiooiccre.altb 
|- ( ph -> A < B )
cncfiooiccre.f 
|- ( ph -> F e. ( ( A (,) B ) -cn-> RR ) )
cncfiooiccre.l 
|- ( ph -> L e. ( F limCC B ) )
cncfiooiccre.r 
|- ( ph -> R e. ( F limCC A ) )
Assertion cncfiooiccre 
|- ( ph -> G e. ( ( A [,] B ) -cn-> RR ) )

Proof

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