Metamath Proof Explorer

Theorem itg2lea

Description: Approximate version of itg2le . If F <_ G for almost all x , then S.2 F <_ S.2 G . (Contributed by Mario Carneiro, 11-Aug-2014)

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

Proof

Step Hyp Ref Expression
1 itg2lea.1 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
2 itg2lea.2 ⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) )
3 itg2lea.3 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4 itg2lea.4 ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
5 itg2lea.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
6 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) )
7 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → 𝑓 ∈ dom ∫1 )
8 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → 𝐴 ⊆ ℝ )
9 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( vol* ‘ 𝐴 ) = 0 )
10 i1ff ⊢ ( 𝑓 ∈ dom ∫1 → 𝑓 : ℝ ⟶ ℝ )
11 10 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → 𝑓 : ℝ ⟶ ℝ )
12 eldifi ⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → 𝑥 ∈ ℝ )
13 ffvelrn ⊢ ( ( 𝑓 : ℝ ⟶ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
14 11 12 13 syl2an ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
15 14 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ* )
16 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
17 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
18 ffvelrn ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
19 17 12 18 syl2an ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
20 16 19 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
21 ffvelrn ⊢ ( ( 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
22 6 12 21 syl2an ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
23 16 22 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ* )
24 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → 𝑓 ∘r ≤ 𝐹 )
25 11 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → 𝑓 Fn ℝ )
26 17 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → 𝐹 Fn ℝ )
27 reex ⊢ ℝ ∈ V
28 27 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ℝ ∈ V )
29 inidm ⊢ ( ℝ ∩ ℝ ) = ℝ
30 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) )
31 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
32 25 26 28 28 29 30 31 ofrfval ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( 𝑓 ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
33 24 32 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ∀ 𝑥 ∈ ℝ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
34 33 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑓 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
35 12 34 sylan2 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝑓 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
36 5 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
37 15 20 23 35 36 xrletrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝑓 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑥 ) )
38 6 7 8 9 37 itg2uba ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑓 ∘r ≤ 𝐹 ) ) → ( ∫1 ‘ 𝑓 ) ≤ ( ∫2 ‘ 𝐺 ) )
39 38 expr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ dom ∫1 ) → ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ ( ∫2 ‘ 𝐺 ) ) )
40 39 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ ( ∫2 ‘ 𝐺 ) ) )
41 itg2cl ⊢ ( 𝐺 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ 𝐺 ) ∈ ℝ* )
42 2 41 syl ⊢ ( 𝜑 → ( ∫2 ‘ 𝐺 ) ∈ ℝ* )
43 itg2leub ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ 𝐺 ) ∈ ℝ* ) → ( ( ∫2 ‘ 𝐹 ) ≤ ( ∫2 ‘ 𝐺 ) ↔ ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ ( ∫2 ‘ 𝐺 ) ) ) )
44 1 42 43 syl2anc ⊢ ( 𝜑 → ( ( ∫2 ‘ 𝐹 ) ≤ ( ∫2 ‘ 𝐺 ) ↔ ∀ 𝑓 ∈ dom ∫1 ( 𝑓 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑓 ) ≤ ( ∫2 ‘ 𝐺 ) ) ) )
45 40 44 mpbird ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ≤ ( ∫2 ‘ 𝐺 ) )