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 C_ RR /\ G : A --> RR+ /\ F : A --> RR+ ) -> ( F e. ( _O ` G ) <-> ( F /_f G ) e. <_O(1) ) )

Proof

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