This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑥 )