Metamath Proof Explorer

Theorem itg2uba

Description: Approximate version of itg2ub . If F approximately dominates G , then S.1 G <_ S.2 F . (Contributed by Mario Carneiro, 11-Aug-2014)

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

Proof

Step Hyp Ref Expression
1 itg2uba.1 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
2 itg2uba.2 ⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 )
3 itg2uba.3 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4 itg2uba.4 ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
5 itg2uba.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
6 itg1cl ⊢ ( 𝐺 ∈ dom ∫1 → ( ∫1 ‘ 𝐺 ) ∈ ℝ )
7 2 6 syl ⊢ ( 𝜑 → ( ∫1 ‘ 𝐺 ) ∈ ℝ )
8 7 rexrd ⊢ ( 𝜑 → ( ∫1 ‘ 𝐺 ) ∈ ℝ* )
9 nulmbl ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) = 0 ) → 𝐴 ∈ dom vol )
10 3 4 9 syl2anc ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
11 cmmbl ⊢ ( 𝐴 ∈ dom vol → ( ℝ ∖ 𝐴 ) ∈ dom vol )
12 10 11 syl ⊢ ( 𝜑 → ( ℝ ∖ 𝐴 ) ∈ dom vol )
13 ifnot ⊢ if ( ¬ 𝑥 ∈ 𝐴 , ( 𝐺 ‘ 𝑥 ) , 0 ) = if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) )
14 eldif ⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) ↔ ( 𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ 𝐴 ) )
15 14 baibr ⊢ ( 𝑥 ∈ ℝ → ( ¬ 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) )
16 15 ifbid ⊢ ( 𝑥 ∈ ℝ → if ( ¬ 𝑥 ∈ 𝐴 , ( 𝐺 ‘ 𝑥 ) , 0 ) = if ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) , ( 𝐺 ‘ 𝑥 ) , 0 ) )
17 13 16 eqtr3id ⊢ ( 𝑥 ∈ ℝ → if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) = if ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) , ( 𝐺 ‘ 𝑥 ) , 0 ) )
18 17 mpteq2ia ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) , ( 𝐺 ‘ 𝑥 ) , 0 ) )
19 18 i1fres ⊢ ( ( 𝐺 ∈ dom ∫1 ∧ ( ℝ ∖ 𝐴 ) ∈ dom vol ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) ∈ dom ∫1 )
20 2 12 19 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) ∈ dom ∫1 )
21 itg1cl ⊢ ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) ∈ dom ∫1 → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ℝ )
22 20 21 syl ⊢ ( 𝜑 → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ℝ )
23 22 rexrd ⊢ ( 𝜑 → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ ℝ* )
24 itg2cl ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ* )
25 1 24 syl ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ* )
26 i1ff ⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℝ )
27 2 26 syl ⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℝ )
28 eldifi ⊢ ( 𝑦 ∈ ( ℝ ∖ 𝐴 ) → 𝑦 ∈ ℝ )
29 ffvelrn ⊢ ( ( 𝐺 : ℝ ⟶ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐺 ‘ 𝑦 ) ∈ ℝ )
30 27 28 29 syl2an ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ℝ )
31 30 leidd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐺 ‘ 𝑦 ) ≤ ( 𝐺 ‘ 𝑦 ) )
32 eldif ⊢ ( 𝑦 ∈ ( ℝ ∖ 𝐴 ) ↔ ( 𝑦 ∈ ℝ ∧ ¬ 𝑦 ∈ 𝐴 ) )
33 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
34 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) )
35 33 34 ifbieq2d ⊢ ( 𝑥 = 𝑦 → if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) = if ( 𝑦 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑦 ) ) )
36 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) )
37 c0ex ⊢ 0 ∈ V
38 fvex ⊢ ( 𝐺 ‘ 𝑦 ) ∈ V
39 37 38 ifex ⊢ if ( 𝑦 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑦 ) ) ∈ V
40 35 36 39 fvmpt ⊢ ( 𝑦 ∈ ℝ → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝑦 ) = if ( 𝑦 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑦 ) ) )
41 iffalse ⊢ ( ¬ 𝑦 ∈ 𝐴 → if ( 𝑦 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑦 ) ) = ( 𝐺 ‘ 𝑦 ) )
42 40 41 sylan9eq ⊢ ( ( 𝑦 ∈ ℝ ∧ ¬ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
43 32 42 sylbi ⊢ ( 𝑦 ∈ ( ℝ ∖ 𝐴 ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
44 43 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℝ ∖ 𝐴 ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
45 31 44 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℝ ∖ 𝐴 ) ) → ( 𝐺 ‘ 𝑦 ) ≤ ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝑦 ) )
46 2 3 4 20 45 itg1lea ⊢ ( 𝜑 → ( ∫1 ‘ 𝐺 ) ≤ ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) ) )
47 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) = 0 )
48 47 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) = 0 )
49 1 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
50 elxrge0 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
51 49 50 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
52 51 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) )
53 52 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) )
54 48 53 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝐹 ‘ 𝑥 ) )
55 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) = ( 𝐺 ‘ 𝑥 ) )
56 55 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) = ( 𝐺 ‘ 𝑥 ) )
57 14 5 sylan2br ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ 𝐴 ) ) → ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
58 57 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
59 56 58 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝐹 ‘ 𝑥 ) )
60 54 59 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝐹 ‘ 𝑥 ) )
61 60 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝐹 ‘ 𝑥 ) )
62 reex ⊢ ℝ ∈ V
63 62 a1i ⊢ ( 𝜑 → ℝ ∈ V )
64 fvex ⊢ ( 𝐺 ‘ 𝑥 ) ∈ V
65 37 64 ifex ⊢ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ∈ V
66 65 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ∈ V )
67 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ V )
68 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) )
69 1 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) )
70 63 66 67 68 69 ofrfval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
71 61 70 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) ∘r ≤ 𝐹 )
72 itg2ub ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) ∈ dom ∫1 ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) ∘r ≤ 𝐹 ) → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) ) ≤ ( ∫2 ‘ 𝐹 ) )
73 1 20 71 72 syl3anc ⊢ ( 𝜑 → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 0 , ( 𝐺 ‘ 𝑥 ) ) ) ) ≤ ( ∫2 ‘ 𝐹 ) )
74 8 23 25 46 73 xrletrd ⊢ ( 𝜑 → ( ∫1 ‘ 𝐺 ) ≤ ( ∫2 ‘ 𝐹 ) )