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 | |
|
itg2uba.2 | |
||
itg2uba.3 | |
||
itg2uba.4 | |
||
itg2uba.5 | |
||
Assertion | itg2uba | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | itg2uba.1 | |
|
2 | itg2uba.2 | |
|
3 | itg2uba.3 | |
|
4 | itg2uba.4 | |
|
5 | itg2uba.5 | |
|
6 | itg1cl | |
|
7 | 2 6 | syl | |
8 | 7 | rexrd | |
9 | nulmbl | |
|
10 | 3 4 9 | syl2anc | |
11 | cmmbl | |
|
12 | 10 11 | syl | |
13 | ifnot | |
|
14 | eldif | |
|
15 | 14 | baibr | |
16 | 15 | ifbid | |
17 | 13 16 | eqtr3id | |
18 | 17 | mpteq2ia | |
19 | 18 | i1fres | |
20 | 2 12 19 | syl2anc | |
21 | itg1cl | |
|
22 | 20 21 | syl | |
23 | 22 | rexrd | |
24 | itg2cl | |
|
25 | 1 24 | syl | |
26 | i1ff | |
|
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 | |
36 | eqid | |
|
37 | c0ex | |
|
38 | fvex | |
|
39 | 37 38 | ifex | |
40 | 35 36 39 | fvmpt | |
41 | iffalse | |
|
42 | 40 41 | sylan9eq | |
43 | 32 42 | sylbi | |
44 | 43 | adantl | |
45 | 31 44 | breqtrrd | |
46 | 2 3 4 20 45 | itg1lea | |
47 | iftrue | |
|
48 | 47 | adantl | |
49 | 1 | ffvelrnda | |
50 | elxrge0 | |
|
51 | 49 50 | sylib | |
52 | 51 | simprd | |
53 | 52 | adantr | |
54 | 48 53 | eqbrtrd | |
55 | iffalse | |
|
56 | 55 | adantl | |
57 | 14 5 | sylan2br | |
58 | 57 | anassrs | |
59 | 56 58 | eqbrtrd | |
60 | 54 59 | pm2.61dan | |
61 | 60 | ralrimiva | |
62 | reex | |
|
63 | 62 | a1i | |
64 | fvex | |
|
65 | 37 64 | ifex | |
66 | 65 | a1i | |
67 | fvexd | |
|
68 | eqidd | |
|
69 | 1 | feqmptd | |
70 | 63 66 67 68 69 | ofrfval2 | |
71 | 61 70 | mpbird | |
72 | itg2ub | |
|
73 | 1 20 71 72 | syl3anc | |
74 | 8 23 25 46 73 | xrletrd | |