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 eqtr2id
 |-  ( ( 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 )