Metamath Proof Explorer

Theorem iblcncfioo

Description: A continuous function F on an open interval ( A (,) B ) with a finite right limit R in A and a finite left limit L in B is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses iblcncfioo.a 
|- ( ph -> A e. RR )
iblcncfioo.b 
|- ( ph -> B e. RR )
iblcncfioo.f 
|- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
iblcncfioo.l 
|- ( ph -> L e. ( F limCC B ) )
iblcncfioo.r 
|- ( ph -> R e. ( F limCC A ) )
Assertion iblcncfioo 
|- ( ph -> F e. L^1 )

Proof

Step Hyp Ref Expression
1 iblcncfioo.a 
 |-  ( ph -> A e. RR )
2 iblcncfioo.b 
 |-  ( ph -> B e. RR )
3 iblcncfioo.f 
 |-  ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
4 iblcncfioo.l 
 |-  ( ph -> L e. ( F limCC B ) )
5 iblcncfioo.r 
 |-  ( ph -> R e. ( F limCC A ) )
6 cncff 
 |-  ( F e. ( ( A (,) B ) -cn-> CC ) -> F : ( A (,) B ) --> CC )
7 3 6 syl 
 |-  ( ph -> F : ( A (,) B ) --> CC )
8 7 feqmptd 
 |-  ( ph -> F = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
9 1 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> A e. RR )
10 eliooord 
 |-  ( x e. ( A (,) B ) -> ( A < x /\ x < B ) )
11 10 simpld 
 |-  ( x e. ( A (,) B ) -> A < x )
12 11 adantl 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> A < x )
13 9 12 gtned 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x =/= A )
14 13 neneqd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> -. x = A )
15 14 iffalsed 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
16 elioore 
 |-  ( x e. ( A (,) B ) -> x e. RR )
17 16 adantl 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. RR )
18 10 simprd 
 |-  ( x e. ( A (,) B ) -> x < B )
19 18 adantl 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x < B )
20 17 19 ltned 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x =/= B )
21 20 neneqd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> -. x = B )
22 21 iffalsed 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
23 15 22 eqtrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = ( F ` x ) )
24 23 eqcomd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
25 24 mpteq2dva 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( F ` x ) ) = ( x e. ( A (,) B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) )
26 8 25 eqtrd 
 |-  ( ph -> F = ( x e. ( A (,) B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) )
27 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
28 27 a1i 
 |-  ( ph -> ( A (,) B ) C_ ( A [,] B ) )
29 ioombl 
 |-  ( A (,) B ) e. dom vol
30 29 a1i 
 |-  ( ph -> ( A (,) B ) e. dom vol )
31 iftrue 
 |-  ( x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
32 31 adantl 
 |-  ( ( ph /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
33 limccl 
 |-  ( F limCC A ) C_ CC
34 33 5 sselid 
 |-  ( ph -> R e. CC )
35 34 adantr 
 |-  ( ( ph /\ x = A ) -> R e. CC )
36 32 35 eqeltrd 
 |-  ( ( ph /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
37 36 adantlr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
38 iffalse 
 |-  ( -. x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
39 38 ad2antlr 
 |-  ( ( ( ph /\ -. x = A ) /\ x = B ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
40 iftrue 
 |-  ( x = B -> if ( x = B , L , ( F ` x ) ) = L )
41 40 adantl 
 |-  ( ( ( ph /\ -. x = A ) /\ x = B ) -> if ( x = B , L , ( F ` x ) ) = L )
42 39 41 eqtrd 
 |-  ( ( ( ph /\ -. x = A ) /\ x = B ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = L )
43 limccl 
 |-  ( F limCC B ) C_ CC
44 43 4 sselid 
 |-  ( ph -> L e. CC )
45 44 ad2antrr 
 |-  ( ( ( ph /\ -. x = A ) /\ x = B ) -> L e. CC )
46 42 45 eqeltrd 
 |-  ( ( ( ph /\ -. x = A ) /\ x = B ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
47 46 adantllr 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ x = B ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
48 simplll 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ph )
49 1 rexrd 
 |-  ( ph -> A e. RR* )
50 48 49 syl 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> A e. RR* )
51 2 rexrd 
 |-  ( ph -> B e. RR* )
52 48 51 syl 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> B e. RR* )
53 eliccxr 
 |-  ( x e. ( A [,] B ) -> x e. RR* )
54 53 ad3antlr 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. RR* )
55 50 52 54 3jca 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( A e. RR* /\ B e. RR* /\ x e. RR* ) )
56 1 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> A e. RR )
57 1 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> A e. RR )
58 2 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR )
59 simpr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. ( A [,] B ) )
60 eliccre 
 |-  ( ( A e. RR /\ B e. RR /\ x e. ( A [,] B ) ) -> x e. RR )
61 57 58 59 60 syl3anc 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. RR )
62 61 adantr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> x e. RR )
63 1 2 jca 
 |-  ( ph -> ( A e. RR /\ B e. RR ) )
64 63 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( A e. RR /\ B e. RR ) )
65 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
66 64 65 syl 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
67 59 66 mpbid 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( x e. RR /\ A <_ x /\ x <_ B ) )
68 67 simp2d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> A <_ x )
69 68 adantr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> A <_ x )
70 df-ne 
 |-  ( x =/= A <-> -. x = A )
71 70 biimpri 
 |-  ( -. x = A -> x =/= A )
72 71 adantl 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> x =/= A )
73 56 62 69 72 leneltd 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> A < x )
74 73 adantr 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> A < x )
75 nesym 
 |-  ( B =/= x <-> -. x = B )
76 75 biimpri 
 |-  ( -. x = B -> B =/= x )
77 76 adantl 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = B ) -> B =/= x )
78 67 simp3d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x <_ B )
79 61 58 78 3jca 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( x e. RR /\ B e. RR /\ x <_ B ) )
80 79 adantr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = B ) -> ( x e. RR /\ B e. RR /\ x <_ B ) )
81 leltne 
 |-  ( ( x e. RR /\ B e. RR /\ x <_ B ) -> ( x < B <-> B =/= x ) )
82 80 81 syl 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = B ) -> ( x < B <-> B =/= x ) )
83 77 82 mpbird 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = B ) -> x < B )
84 83 adantlr 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x < B )
85 74 84 jca 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( A < x /\ x < B ) )
86 elioo3g 
 |-  ( x e. ( A (,) B ) <-> ( ( A e. RR* /\ B e. RR* /\ x e. RR* ) /\ ( A < x /\ x < B ) ) )
87 55 85 86 sylanbrc 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. ( A (,) B ) )
88 48 87 jca 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( ph /\ x e. ( A (,) B ) ) )
89 7 ffvelcdmda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) e. CC )
90 23 89 eqeltrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
91 88 90 syl 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
92 47 91 pm2.61dan 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
93 37 92 pm2.61dan 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
94 nfv 
 |-  F/ x ph
95 eqid 
 |-  ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
96 94 95 1 2 3 4 5 cncfiooicc 
 |-  ( ph -> ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
97 cniccibl 
 |-  ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) e. L^1 )
98 1 2 96 97 syl3anc 
 |-  ( ph -> ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) e. L^1 )
99 28 30 93 98 iblss 
 |-  ( ph -> ( x e. ( A (,) B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) e. L^1 )
100 26 99 eqeltrd 
 |-  ( ph -> F e. L^1 )