Metamath Proof Explorer

Theorem ibliooicc

Description: If a function is integrable on an open interval, it is integrable on the corresponding closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses ibliooicc.1 
|- ( ph -> A e. RR )
ibliooicc.2 
|- ( ph -> B e. RR )
ibliooicc.3 
|- ( ph -> ( x e. ( A (,) B ) |-> C ) e. L^1 )
ibliooicc.4 
|- ( ( ph /\ x e. ( A [,] B ) ) -> C e. CC )
Assertion ibliooicc 
|- ( ph -> ( x e. ( A [,] B ) |-> C ) e. L^1 )

Proof

Step Hyp Ref Expression
1 ibliooicc.1 
 |-  ( ph -> A e. RR )
2 ibliooicc.2 
 |-  ( ph -> B e. RR )
3 ibliooicc.3 
 |-  ( ph -> ( x e. ( A (,) B ) |-> C ) e. L^1 )
4 ibliooicc.4 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> C e. CC )
5 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
6 5 a1i 
 |-  ( ph -> ( A (,) B ) C_ ( A [,] B ) )
7 1 2 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
8 1 rexrd 
 |-  ( ph -> A e. RR* )
9 2 rexrd 
 |-  ( ph -> B e. RR* )
10 icc0 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,] B ) = (/) <-> B < A ) )
11 8 9 10 syl2anc 
 |-  ( ph -> ( ( A [,] B ) = (/) <-> B < A ) )
12 11 biimpar 
 |-  ( ( ph /\ B < A ) -> ( A [,] B ) = (/) )
13 12 difeq1d 
 |-  ( ( ph /\ B < A ) -> ( ( A [,] B ) \ ( A (,) B ) ) = ( (/) \ ( A (,) B ) ) )
14 0dif 
 |-  ( (/) \ ( A (,) B ) ) = (/)
15 0ss 
 |-  (/) C_ { A , B }
16 14 15 eqsstri 
 |-  ( (/) \ ( A (,) B ) ) C_ { A , B }
17 13 16 eqsstrdi 
 |-  ( ( ph /\ B < A ) -> ( ( A [,] B ) \ ( A (,) B ) ) C_ { A , B } )
18 ssid 
 |-  ( ( A [,] B ) \ ( A (,) B ) ) C_ ( ( A [,] B ) \ ( A (,) B ) )
19 8 adantr 
 |-  ( ( ph /\ A <_ B ) -> A e. RR* )
20 9 adantr 
 |-  ( ( ph /\ A <_ B ) -> B e. RR* )
21 simpr 
 |-  ( ( ph /\ A <_ B ) -> A <_ B )
22 iccdifioo 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A [,] B ) \ ( A (,) B ) ) = { A , B } )
23 19 20 21 22 syl3anc 
 |-  ( ( ph /\ A <_ B ) -> ( ( A [,] B ) \ ( A (,) B ) ) = { A , B } )
24 18 23 sseqtrid 
 |-  ( ( ph /\ A <_ B ) -> ( ( A [,] B ) \ ( A (,) B ) ) C_ { A , B } )
25 17 24 2 1 ltlecasei 
 |-  ( ph -> ( ( A [,] B ) \ ( A (,) B ) ) C_ { A , B } )
26 prssi 
 |-  ( ( A e. RR /\ B e. RR ) -> { A , B } C_ RR )
27 1 2 26 syl2anc 
 |-  ( ph -> { A , B } C_ RR )
28 prfi 
 |-  { A , B } e. Fin
29 ovolfi 
 |-  ( ( { A , B } e. Fin /\ { A , B } C_ RR ) -> ( vol* ` { A , B } ) = 0 )
30 28 27 29 sylancr 
 |-  ( ph -> ( vol* ` { A , B } ) = 0 )
31 ovolssnul 
 |-  ( ( ( ( A [,] B ) \ ( A (,) B ) ) C_ { A , B } /\ { A , B } C_ RR /\ ( vol* ` { A , B } ) = 0 ) -> ( vol* ` ( ( A [,] B ) \ ( A (,) B ) ) ) = 0 )
32 25 27 30 31 syl3anc 
 |-  ( ph -> ( vol* ` ( ( A [,] B ) \ ( A (,) B ) ) ) = 0 )
33 6 7 32 4 itgss3 
 |-  ( ph -> ( ( ( x e. ( A (,) B ) |-> C ) e. L^1 <-> ( x e. ( A [,] B ) |-> C ) e. L^1 ) /\ S. ( A (,) B ) C _d x = S. ( A [,] B ) C _d x ) )
34 33 simpld 
 |-  ( ph -> ( ( x e. ( A (,) B ) |-> C ) e. L^1 <-> ( x e. ( A [,] B ) |-> C ) e. L^1 ) )
35 3 34 mpbid 
 |-  ( ph -> ( x e. ( A [,] B ) |-> C ) e. L^1 )