Theorem itg2eqa

Description: Approximate equality of integrals. If F = G for almost all x , then S.2 F = S.2 G . (Contributed by Mario Carneiro, 12-Aug-2014)

	Ref	Expression
Hypotheses	itg2lea.1	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
	itg2lea.2	⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) )
	itg2lea.3	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	itg2lea.4	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
	itg2eqa.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
Assertion	itg2eqa	⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) = ( ∫2 ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		itg2lea.1	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
2		itg2lea.2	⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) )
3		itg2lea.3	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4		itg2lea.4	⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
5		itg2eqa.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
6		itg2cl	⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ* )
7	1 6	syl	⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ* )
8		itg2cl	⊢ ( 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ 𝐺 ) ∈ ℝ* )
9	2 8	syl	⊢ ( 𝜑 → ( ∫2 ‘ 𝐺 ) ∈ ℝ* )
10		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
11		eldifi	⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → 𝑥 ∈ ℝ )
12		ffvelrn	⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
13	1 11 12	syl2an	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
14	10 13	sseldi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
15	14	xrleidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
16	15 5	breqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
17	1 2 3 4 16	itg2lea	⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ≤ ( ∫2 ‘ 𝐺 ) )
18	5 15	eqbrtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
19	2 1 3 4 18	itg2lea	⊢ ( 𝜑 → ( ∫2 ‘ 𝐺 ) ≤ ( ∫2 ‘ 𝐹 ) )
20	7 9 17 19	xrletrid	⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) = ( ∫2 ‘ 𝐺 ) )