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

Metamath Proof Explorer

Theorem o1eq

Description: Two functions that are eventually equal to one another are eventually bounded if one of them is. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses rlimeq.1 
|- ( ( ph /\ x e. A ) -> B e. CC )
rlimeq.2 
|- ( ( ph /\ x e. A ) -> C e. CC )
rlimeq.3 
|- ( ph -> D e. RR )
rlimeq.4 
|- ( ( ph /\ ( x e. A /\ D <_ x ) ) -> B = C )
Assertion o1eq 
|- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> C ) e. O(1) ) )

Proof

Step Hyp Ref Expression
1 rlimeq.1 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
2 rlimeq.2 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
3 rlimeq.3 
 |-  ( ph -> D e. RR )
4 rlimeq.4 
 |-  ( ( ph /\ ( x e. A /\ D <_ x ) ) -> B = C )
5 1 abscld 
 |-  ( ( ph /\ x e. A ) -> ( abs ` B ) e. RR )
6 2 abscld 
 |-  ( ( ph /\ x e. A ) -> ( abs ` C ) e. RR )
7 4 fveq2d 
 |-  ( ( ph /\ ( x e. A /\ D <_ x ) ) -> ( abs ` B ) = ( abs ` C ) )
8 5 6 3 7 lo1eq 
 |-  ( ph -> ( ( x e. A |-> ( abs ` B ) ) e. <_O(1) <-> ( x e. A |-> ( abs ` C ) ) e. <_O(1) ) )
9 1 lo1o12 
 |-  ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> ( abs ` B ) ) e. <_O(1) ) )
10 2 lo1o12 
 |-  ( ph -> ( ( x e. A |-> C ) e. O(1) <-> ( x e. A |-> ( abs ` C ) ) e. <_O(1) ) )
11 8 9 10 3bitr4d 
 |-  ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> C ) e. O(1) ) )