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 ( 𝜑𝐴 ∈ ℝ )
itgioo.2 ( 𝜑𝐵 ∈ ℝ )
itgioo.3 ( ( 𝜑𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐶 ∈ ℂ )
Assertion itgioo ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) 𝐶 d 𝑥 )

Proof

Step Hyp Ref Expression
1 itgioo.1 ( 𝜑𝐴 ∈ ℝ )
2 itgioo.2 ( 𝜑𝐵 ∈ ℝ )
3 itgioo.3 ( ( 𝜑𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐶 ∈ ℂ )
4 ioossicc ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
5 4 a1i ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
6 iccssre ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
7 1 2 6 syl2anc ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
8 1 rexrd ( 𝜑𝐴 ∈ ℝ* )
9 2 rexrd ( 𝜑𝐵 ∈ ℝ* )
10 icc0 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
11 8 9 10 syl2anc ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
12 11 biimpar ( ( 𝜑𝐵 < 𝐴 ) → ( 𝐴 [,] 𝐵 ) = ∅ )
13 12 difeq1d ( ( 𝜑𝐵 < 𝐴 ) → ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) = ( ∅ ∖ ( 𝐴 (,) 𝐵 ) ) )
14 0dif ( ∅ ∖ ( 𝐴 (,) 𝐵 ) ) = ∅
15 0ss ∅ ⊆ { 𝐴 , 𝐵 }
16 14 15 eqsstri ( ∅ ∖ ( 𝐴 (,) 𝐵 ) ) ⊆ { 𝐴 , 𝐵 }
17 13 16 eqsstrdi ( ( 𝜑𝐵 < 𝐴 ) → ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) ⊆ { 𝐴 , 𝐵 } )
18 uncom ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) = ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } )
19 8 adantr ( ( 𝜑𝐴𝐵 ) → 𝐴 ∈ ℝ* )
20 9 adantr ( ( 𝜑𝐴𝐵 ) → 𝐵 ∈ ℝ* )
21 simpr ( ( 𝜑𝐴𝐵 ) → 𝐴𝐵 )
22 prunioo ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) )
23 19 20 21 22 syl3anc ( ( 𝜑𝐴𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) )
24 18 23 eqtr2id ( ( 𝜑𝐴𝐵 ) → ( 𝐴 [,] 𝐵 ) = ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) )
25 24 difeq1d ( ( 𝜑𝐴𝐵 ) → ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) = ( ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) ∖ ( 𝐴 (,) 𝐵 ) ) )
26 difun2 ( ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) ∖ ( 𝐴 (,) 𝐵 ) ) = ( { 𝐴 , 𝐵 } ∖ ( 𝐴 (,) 𝐵 ) )
27 25 26 eqtrdi ( ( 𝜑𝐴𝐵 ) → ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) = ( { 𝐴 , 𝐵 } ∖ ( 𝐴 (,) 𝐵 ) ) )
28 difss ( { 𝐴 , 𝐵 } ∖ ( 𝐴 (,) 𝐵 ) ) ⊆ { 𝐴 , 𝐵 }
29 27 28 eqsstrdi ( ( 𝜑𝐴𝐵 ) → ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) ⊆ { 𝐴 , 𝐵 } )
30 17 29 2 1 ltlecasei ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) ⊆ { 𝐴 , 𝐵 } )
31 1 2 prssd ( 𝜑 → { 𝐴 , 𝐵 } ⊆ ℝ )
32 prfi { 𝐴 , 𝐵 } ∈ Fin
33 ovolfi ( ( { 𝐴 , 𝐵 } ∈ Fin ∧ { 𝐴 , 𝐵 } ⊆ ℝ ) → ( vol* ‘ { 𝐴 , 𝐵 } ) = 0 )
34 32 31 33 sylancr ( 𝜑 → ( vol* ‘ { 𝐴 , 𝐵 } ) = 0 )
35 ovolssnul ( ( ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) ⊆ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝐵 } ⊆ ℝ ∧ ( vol* ‘ { 𝐴 , 𝐵 } ) = 0 ) → ( vol* ‘ ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) ) = 0 )
36 30 31 34 35 syl3anc ( 𝜑 → ( vol* ‘ ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) ) = 0 )
37 5 7 36 3 itgss3 ( 𝜑 → ( ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) ∈ 𝐿1 ↔ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐶 ) ∈ 𝐿1 ) ∧ ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) 𝐶 d 𝑥 ) )
38 37 simprd ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) 𝐶 d 𝑥 )