Metamath Proof Explorer

Theorem itgioo

Description: Equality of integrals on open and closed intervals. (Contributed by Mario Carneiro, 2-Sep-2014)

Ref Expression
Hypotheses itgioo.1 
|- ( ph -> A e. RR )
itgioo.2 
|- ( ph -> B e. RR )
itgioo.3 
|- ( ( ph /\ x e. ( A [,] B ) ) -> C e. CC )
Assertion itgioo 
|- ( ph -> S. ( A (,) B ) C _d x = S. ( A [,] B ) C _d x )

Proof

Step Hyp Ref Expression
1 itgioo.1 
 |-  ( ph -> A e. RR )
2 itgioo.2 
 |-  ( ph -> B e. RR )
3 itgioo.3 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> C e. CC )
4 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
5 4 a1i 
 |-  ( ph -> ( A (,) B ) C_ ( A [,] B ) )
6 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
7 1 2 6 syl2anc 
 |-  ( 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 uncom 
 |-  ( { A , B } u. ( A (,) B ) ) = ( ( A (,) B ) u. { 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 prunioo 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
23 19 20 21 22 syl3anc 
 |-  ( ( ph /\ A <_ B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
24 18 23 syl5req 
 |-  ( ( ph /\ A <_ B ) -> ( A [,] B ) = ( { A , B } u. ( A (,) B ) ) )
25 24 difeq1d 
 |-  ( ( ph /\ A <_ B ) -> ( ( A [,] B ) \ ( A (,) B ) ) = ( ( { A , B } u. ( A (,) B ) ) \ ( A (,) B ) ) )
26 difun2 
 |-  ( ( { A , B } u. ( A (,) B ) ) \ ( A (,) B ) ) = ( { A , B } \ ( A (,) B ) )
27 25 26 eqtrdi 
 |-  ( ( ph /\ A <_ B ) -> ( ( A [,] B ) \ ( A (,) B ) ) = ( { A , B } \ ( A (,) B ) ) )
28 difss 
 |-  ( { A , B } \ ( A (,) B ) ) C_ { A , B }
29 27 28 eqsstrdi 
 |-  ( ( ph /\ A <_ B ) -> ( ( A [,] B ) \ ( A (,) B ) ) C_ { A , B } )
30 17 29 2 1 ltlecasei 
 |-  ( ph -> ( ( A [,] B ) \ ( A (,) B ) ) C_ { A , B } )
31 1 2 prssd 
 |-  ( ph -> { A , B } C_ RR )
32 prfi 
 |-  { A , B } e. Fin
33 ovolfi 
 |-  ( ( { A , B } e. Fin /\ { A , B } C_ RR ) -> ( vol* ` { A , B } ) = 0 )
34 32 31 33 sylancr 
 |-  ( ph -> ( vol* ` { A , B } ) = 0 )
35 ovolssnul 
 |-  ( ( ( ( A [,] B ) \ ( A (,) B ) ) C_ { A , B } /\ { A , B } C_ RR /\ ( vol* ` { A , B } ) = 0 ) -> ( vol* ` ( ( A [,] B ) \ ( A (,) B ) ) ) = 0 )
36 30 31 34 35 syl3anc 
 |-  ( ph -> ( vol* ` ( ( A [,] B ) \ ( A (,) B ) ) ) = 0 )
37 5 7 36 3 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 ) )
38 37 simprd 
 |-  ( ph -> S. ( A (,) B ) C _d x = S. ( A [,] B ) C _d x )