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

Metamath Proof Explorer

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 ffvelcdm ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
13 1 11 12 syl2an ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
14 10 13 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
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 ‘ 𝐺 ) )