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 φ F : 0 +∞
itg2uba.2 φ G dom 1
itg2uba.3 φ A
itg2uba.4 φ vol * A = 0
itg2uba.5 φ x A G x F x
Assertion itg2uba φ 1 G 2 F

Proof

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