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

Metamath Proof Explorer

Theorem itg1lea

Description: Approximate version of itg1le . If F <_ G for almost all x , then S.1 F <_ S.1 G . (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 6-Aug-2014)

Ref Expression
Hypotheses itg10a.1 ⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
itg10a.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
itg10a.3 ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
itg1lea.4 ⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 )
itg1lea.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
Assertion itg1lea ( 𝜑 → ( ∫1 ‘ 𝐹 ) ≤ ( ∫1 ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 itg10a.1 ⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
2 itg10a.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3 itg10a.3 ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
4 itg1lea.4 ⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 )
5 itg1lea.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
6 i1fsub ⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝐹 ∈ dom ∫1 ) → ( 𝐺 ∘f − 𝐹 ) ∈ dom ∫1 )
7 4 1 6 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∘f − 𝐹 ) ∈ dom ∫1 )
8 eldifi ⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → 𝑥 ∈ ℝ )
9 i1ff ⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℝ )
10 4 9 syl ⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℝ )
11 10 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
12 i1ff ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
13 1 12 syl ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
14 13 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
15 11 14 subge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 0 ≤ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) ) )
16 8 15 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 0 ≤ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) ) )
17 5 16 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → 0 ≤ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) )
18 10 ffnd ⊢ ( 𝜑 → 𝐺 Fn ℝ )
19 13 ffnd ⊢ ( 𝜑 → 𝐹 Fn ℝ )
20 reex ⊢ ℝ ∈ V
21 20 a1i ⊢ ( 𝜑 → ℝ ∈ V )
22 inidm ⊢ ( ℝ ∩ ℝ ) = ℝ
23 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
24 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
25 18 19 21 21 22 23 24 ofval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ∘f − 𝐹 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) )
26 8 25 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( ( 𝐺 ∘f − 𝐹 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) )
27 17 26 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → 0 ≤ ( ( 𝐺 ∘f − 𝐹 ) ‘ 𝑥 ) )
28 7 2 3 27 itg1ge0a ⊢ ( 𝜑 → 0 ≤ ( ∫1 ‘ ( 𝐺 ∘f − 𝐹 ) ) )
29 itg1sub ⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝐹 ∈ dom ∫1 ) → ( ∫1 ‘ ( 𝐺 ∘f − 𝐹 ) ) = ( ( ∫1 ‘ 𝐺 ) − ( ∫1 ‘ 𝐹 ) ) )
30 4 1 29 syl2anc ⊢ ( 𝜑 → ( ∫1 ‘ ( 𝐺 ∘f − 𝐹 ) ) = ( ( ∫1 ‘ 𝐺 ) − ( ∫1 ‘ 𝐹 ) ) )
31 28 30 breqtrd ⊢ ( 𝜑 → 0 ≤ ( ( ∫1 ‘ 𝐺 ) − ( ∫1 ‘ 𝐹 ) ) )
32 itg1cl ⊢ ( 𝐺 ∈ dom ∫1 → ( ∫1 ‘ 𝐺 ) ∈ ℝ )
33 4 32 syl ⊢ ( 𝜑 → ( ∫1 ‘ 𝐺 ) ∈ ℝ )
34 itg1cl ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) ∈ ℝ )
35 1 34 syl ⊢ ( 𝜑 → ( ∫1 ‘ 𝐹 ) ∈ ℝ )
36 33 35 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( ( ∫1 ‘ 𝐺 ) − ( ∫1 ‘ 𝐹 ) ) ↔ ( ∫1 ‘ 𝐹 ) ≤ ( ∫1 ‘ 𝐺 ) ) )
37 31 36 mpbid ⊢ ( 𝜑 → ( ∫1 ‘ 𝐹 ) ≤ ( ∫1 ‘ 𝐺 ) )