This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elo12r

Description: Sufficient condition for elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion elo12r 
|- ( ( ( F : A --> CC /\ A C_ RR ) /\ ( C e. RR /\ M e. RR ) /\ A. x e. A ( C <_ x -> ( abs ` ( F ` x ) ) <_ M ) ) -> F e. O(1) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( y = C -> ( y <_ x <-> C <_ x ) )
2 1 imbi1d 
 |-  ( y = C -> ( ( y <_ x -> ( abs ` ( F ` x ) ) <_ m ) <-> ( C <_ x -> ( abs ` ( F ` x ) ) <_ m ) ) )
3 2 ralbidv 
 |-  ( y = C -> ( A. x e. A ( y <_ x -> ( abs ` ( F ` x ) ) <_ m ) <-> A. x e. A ( C <_ x -> ( abs ` ( F ` x ) ) <_ m ) ) )
4 breq2 
 |-  ( m = M -> ( ( abs ` ( F ` x ) ) <_ m <-> ( abs ` ( F ` x ) ) <_ M ) )
5 4 imbi2d 
 |-  ( m = M -> ( ( C <_ x -> ( abs ` ( F ` x ) ) <_ m ) <-> ( C <_ x -> ( abs ` ( F ` x ) ) <_ M ) ) )
6 5 ralbidv 
 |-  ( m = M -> ( A. x e. A ( C <_ x -> ( abs ` ( F ` x ) ) <_ m ) <-> A. x e. A ( C <_ x -> ( abs ` ( F ` x ) ) <_ M ) ) )
7 3 6 rspc2ev 
 |-  ( ( C e. RR /\ M e. RR /\ A. x e. A ( C <_ x -> ( abs ` ( F ` x ) ) <_ M ) ) -> E. y e. RR E. m e. RR A. x e. A ( y <_ x -> ( abs ` ( F ` x ) ) <_ m ) )
8 7 3expa 
 |-  ( ( ( C e. RR /\ M e. RR ) /\ A. x e. A ( C <_ x -> ( abs ` ( F ` x ) ) <_ M ) ) -> E. y e. RR E. m e. RR A. x e. A ( y <_ x -> ( abs ` ( F ` x ) ) <_ m ) )
9 8 3adant1 
 |-  ( ( ( F : A --> CC /\ A C_ RR ) /\ ( C e. RR /\ M e. RR ) /\ A. x e. A ( C <_ x -> ( abs ` ( F ` x ) ) <_ M ) ) -> E. y e. RR E. m e. RR A. x e. A ( y <_ x -> ( abs ` ( F ` x ) ) <_ m ) )
10 elo12 
 |-  ( ( F : A --> CC /\ A C_ RR ) -> ( F e. O(1) <-> E. y e. RR E. m e. RR A. x e. A ( y <_ x -> ( abs ` ( F ` x ) ) <_ m ) ) )
11 10 3ad2ant1 
 |-  ( ( ( F : A --> CC /\ A C_ RR ) /\ ( C e. RR /\ M e. RR ) /\ A. x e. A ( C <_ x -> ( abs ` ( F ` x ) ) <_ M ) ) -> ( F e. O(1) <-> E. y e. RR E. m e. RR A. x e. A ( y <_ x -> ( abs ` ( F ` x ) ) <_ m ) ) )
12 9 11 mpbird 
 |-  ( ( ( F : A --> CC /\ A C_ RR ) /\ ( C e. RR /\ M e. RR ) /\ A. x e. A ( C <_ x -> ( abs ` ( F ` x ) ) <_ M ) ) -> F e. O(1) )