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 ⊢φ→F:ℝ⟶0+∞
itg2lea.2 ⊢φ→G:ℝ⟶0+∞
itg2lea.3 ⊢φ→A⊆ℝ
itg2lea.4 ⊢φ→vol*⁡A=0
itg2eqa.5 ⊢φ∧x∈ℝ∖A→F⁡x=G⁡x
Assertion itg2eqa ⊢φ→∫2⁡F=∫2⁡G

Proof

Step Hyp Ref Expression
1 itg2lea.1 ⊢φ→F:ℝ⟶0+∞
2 itg2lea.2 ⊢φ→G:ℝ⟶0+∞
3 itg2lea.3 ⊢φ→A⊆ℝ
4 itg2lea.4 ⊢φ→vol*⁡A=0
5 itg2eqa.5 ⊢φ∧x∈ℝ∖A→F⁡x=G⁡x
6 itg2cl ⊢F:ℝ⟶0+∞→∫2⁡F∈ℝ*
7 1 6 syl ⊢φ→∫2⁡F∈ℝ*
8 itg2cl ⊢G:ℝ⟶0+∞→∫2⁡G∈ℝ*
9 2 8 syl ⊢φ→∫2⁡G∈ℝ*
10 iccssxr ⊢0+∞⊆ℝ*
11 eldifi ⊢x∈ℝ∖A→x∈ℝ
12 ffvelcdm ⊢F:ℝ⟶0+∞∧x∈ℝ→F⁡x∈0+∞
13 1 11 12 syl2an ⊢φ∧x∈ℝ∖A→F⁡x∈0+∞
14 10 13 sselid ⊢φ∧x∈ℝ∖A→F⁡x∈ℝ*
15 14 xrleidd ⊢φ∧x∈ℝ∖A→F⁡x≤F⁡x
16 15 5 breqtrd ⊢φ∧x∈ℝ∖A→F⁡x≤G⁡x
17 1 2 3 4 16 itg2lea ⊢φ→∫2⁡F≤∫2⁡G
18 5 15 eqbrtrrd ⊢φ∧x∈ℝ∖A→G⁡x≤F⁡x
19 2 1 3 4 18 itg2lea ⊢φ→∫2⁡G≤∫2⁡F
20 7 9 17 19 xrletrid ⊢φ→∫2⁡F=∫2⁡G