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 ffvelrn ⊢ 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