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 φGdom1
itg2uba.3 φA
itg2uba.4 φvol*A=0
itg2uba.5 φxAGxFx
Assertion itg2uba φ1G2F

Proof

Step Hyp Ref Expression
1 itg2uba.1 φF:0+∞
2 itg2uba.2 φGdom1
3 itg2uba.3 φA
4 itg2uba.4 φvol*A=0
5 itg2uba.5 φxAGxFx
6 itg1cl Gdom11G
7 2 6 syl φ1G
8 7 rexrd φ1G*
9 nulmbl Avol*A=0Adomvol
10 3 4 9 syl2anc φAdomvol
11 cmmbl AdomvolAdomvol
12 10 11 syl φAdomvol
13 ifnot if¬xAGx0=ifxA0Gx
14 eldif xAx¬xA
15 14 baibr x¬xAxA
16 15 ifbid xif¬xAGx0=ifxAGx0
17 13 16 eqtr3id xifxA0Gx=ifxAGx0
18 17 mpteq2ia xifxA0Gx=xifxAGx0
19 18 i1fres Gdom1AdomvolxifxA0Gxdom1
20 2 12 19 syl2anc φxifxA0Gxdom1
21 itg1cl xifxA0Gxdom11xifxA0Gx
22 20 21 syl φ1xifxA0Gx
23 22 rexrd φ1xifxA0Gx*
24 itg2cl F:0+∞2F*
25 1 24 syl φ2F*
26 i1ff Gdom1G:
27 2 26 syl φG:
28 eldifi yAy
29 ffvelrn G:yGy
30 27 28 29 syl2an φyAGy
31 30 leidd φyAGyGy
32 eldif yAy¬yA
33 eleq1w x=yxAyA
34 fveq2 x=yGx=Gy
35 33 34 ifbieq2d x=yifxA0Gx=ifyA0Gy
36 eqid xifxA0Gx=xifxA0Gx
37 c0ex 0V
38 fvex GyV
39 37 38 ifex ifyA0GyV
40 35 36 39 fvmpt yxifxA0Gxy=ifyA0Gy
41 iffalse ¬yAifyA0Gy=Gy
42 40 41 sylan9eq y¬yAxifxA0Gxy=Gy
43 32 42 sylbi yAxifxA0Gxy=Gy
44 43 adantl φyAxifxA0Gxy=Gy
45 31 44 breqtrrd φyAGyxifxA0Gxy
46 2 3 4 20 45 itg1lea φ1G1xifxA0Gx
47 iftrue xAifxA0Gx=0
48 47 adantl φxxAifxA0Gx=0
49 1 ffvelrnda φxFx0+∞
50 elxrge0 Fx0+∞Fx*0Fx
51 49 50 sylib φxFx*0Fx
52 51 simprd φx0Fx
53 52 adantr φxxA0Fx
54 48 53 eqbrtrd φxxAifxA0GxFx
55 iffalse ¬xAifxA0Gx=Gx
56 55 adantl φx¬xAifxA0Gx=Gx
57 14 5 sylan2br φx¬xAGxFx
58 57 anassrs φx¬xAGxFx
59 56 58 eqbrtrd φx¬xAifxA0GxFx
60 54 59 pm2.61dan φxifxA0GxFx
61 60 ralrimiva φxifxA0GxFx
62 reex V
63 62 a1i φV
64 fvex GxV
65 37 64 ifex ifxA0GxV
66 65 a1i φxifxA0GxV
67 fvexd φxFxV
68 eqidd φxifxA0Gx=xifxA0Gx
69 1 feqmptd φF=xFx
70 63 66 67 68 69 ofrfval2 φxifxA0GxfFxifxA0GxFx
71 61 70 mpbird φxifxA0GxfF
72 itg2ub F:0+∞xifxA0Gxdom1xifxA0GxfF1xifxA0Gx2F
73 1 20 71 72 syl3anc φ1xifxA0Gx2F
74 8 23 25 46 73 xrletrd φ1G2F