Metamath Proof Explorer


Theorem elbigolo1

Description: A function (into the positive reals) is of order G(x) iff the quotient of the function and G(x) (also a function into the positive reals) is an eventually upper bounded function. (Contributed by AV, 20-May-2020) (Proof shortened by II, 16-Feb-2023)

Ref Expression
Assertion elbigolo1 A G : A + F : A + F O G F / f G 𝑂1

Proof

Step Hyp Ref Expression
1 id F : A + F : A +
2 rpssre +
3 2 a1i F : A + +
4 1 3 fssd F : A + F : A
5 4 3ad2ant3 A G : A + F : A + F : A
6 5 adantr A G : A + F : A + x m F : A
7 6 ffvelrnda A G : A + F : A + x m y A F y
8 simplrr A G : A + F : A + x m y A m
9 simpl2 A G : A + F : A + x m G : A +
10 9 ffvelrnda A G : A + F : A + x m y A G y +
11 10 rpregt0d A G : A + F : A + x m y A G y 0 < G y
12 7 8 11 3jca A G : A + F : A + x m y A F y m G y 0 < G y
13 ledivmul2 F y m G y 0 < G y F y G y m F y m G y
14 13 bicomd F y m G y 0 < G y F y m G y F y G y m
15 12 14 syl A G : A + F : A + x m y A F y m G y F y G y m
16 id G : A + G : A +
17 2 a1i G : A + +
18 16 17 fssd G : A + G : A
19 18 3ad2ant2 A G : A + F : A + G : A
20 reex V
21 20 ssex A A V
22 21 3ad2ant1 A G : A + F : A + A V
23 5 19 22 3jca A G : A + F : A + F : A G : A A V
24 23 adantr A G : A + F : A + x m F : A G : A A V
25 24 adantr A G : A + F : A + x m y A F : A G : A A V
26 ffun G : A + Fun G
27 26 adantl A G : A + Fun G
28 21 anim1ci A G : A + G : A + A V
29 fex G : A + A V G V
30 28 29 syl A G : A + G V
31 0red A G : A + 0
32 frn G : A + ran G +
33 0nrp ¬ 0 +
34 id ran G + ran G +
35 34 ssneld ran G + ¬ 0 + ¬ 0 ran G
36 33 35 mpi ran G + ¬ 0 ran G
37 df-nel 0 ran G ¬ 0 ran G
38 36 37 sylibr ran G + 0 ran G
39 32 38 syl G : A + 0 ran G
40 39 adantl A G : A + 0 ran G
41 suppdm Fun G G V 0 0 ran G G supp 0 = dom G
42 27 30 31 40 41 syl31anc A G : A + G supp 0 = dom G
43 fdm G : A + dom G = A
44 43 adantl A G : A + dom G = A
45 42 44 eqtrd A G : A + G supp 0 = A
46 45 3adant3 A G : A + F : A + G supp 0 = A
47 46 eqcomd A G : A + F : A + A = G supp 0
48 47 adantr A G : A + F : A + x m A = G supp 0
49 48 eleq2d A G : A + F : A + x m y A y supp 0 G
50 49 biimpa A G : A + F : A + x m y A y supp 0 G
51 refdivmptfv F : A G : A A V y supp 0 G F / f G y = F y G y
52 25 50 51 syl2anc A G : A + F : A + x m y A F / f G y = F y G y
53 52 breq1d A G : A + F : A + x m y A F / f G y m F y G y m
54 15 53 bitr4d A G : A + F : A + x m y A F y m G y F / f G y m
55 54 imbi2d A G : A + F : A + x m y A x y F y m G y x y F / f G y m
56 55 ralbidva A G : A + F : A + x m y A x y F y m G y y A x y F / f G y m
57 56 2rexbidva A G : A + F : A + x m y A x y F y m G y x m y A x y F / f G y m
58 simp1 A G : A + F : A + A
59 ssidd A G : A + F : A + A A
60 elbigo2 G : A A F : A A A F O G x m y A x y F y m G y
61 19 58 5 59 60 syl22anc A G : A + F : A + F O G x m y A x y F y m G y
62 refdivmptf F : A G : A A V F / f G : G supp 0
63 23 62 syl A G : A + F : A + F / f G : G supp 0
64 47 feq2d A G : A + F : A + F / f G : A F / f G : G supp 0
65 63 64 mpbird A G : A + F : A + F / f G : A
66 ello12 F / f G : A A F / f G 𝑂1 x m y A x y F / f G y m
67 65 58 66 syl2anc A G : A + F : A + F / f G 𝑂1 x m y A x y F / f G y m
68 57 61 67 3bitr4d A G : A + F : A + F O G F / f G 𝑂1