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	syl5req	⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 [,] 𝐵 ) = ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) )
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 𝑥 )