Metamath Proof Explorer


Theorem o1dif

Description: If the difference of two functions is eventually bounded, eventual boundedness of either one implies the other. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses o1dif.1
|- ( ( ph /\ x e. A ) -> B e. CC )
o1dif.2
|- ( ( ph /\ x e. A ) -> C e. CC )
o1dif.3
|- ( ph -> ( x e. A |-> ( B - C ) ) e. O(1) )
Assertion o1dif
|- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> C ) e. O(1) ) )

Proof

Step Hyp Ref Expression
1 o1dif.1
 |-  ( ( ph /\ x e. A ) -> B e. CC )
2 o1dif.2
 |-  ( ( ph /\ x e. A ) -> C e. CC )
3 o1dif.3
 |-  ( ph -> ( x e. A |-> ( B - C ) ) e. O(1) )
4 o1sub
 |-  ( ( ( x e. A |-> B ) e. O(1) /\ ( x e. A |-> ( B - C ) ) e. O(1) ) -> ( ( x e. A |-> B ) oF - ( x e. A |-> ( B - C ) ) ) e. O(1) )
5 4 expcom
 |-  ( ( x e. A |-> ( B - C ) ) e. O(1) -> ( ( x e. A |-> B ) e. O(1) -> ( ( x e. A |-> B ) oF - ( x e. A |-> ( B - C ) ) ) e. O(1) ) )
6 3 5 syl
 |-  ( ph -> ( ( x e. A |-> B ) e. O(1) -> ( ( x e. A |-> B ) oF - ( x e. A |-> ( B - C ) ) ) e. O(1) ) )
7 1 2 subcld
 |-  ( ( ph /\ x e. A ) -> ( B - C ) e. CC )
8 7 ralrimiva
 |-  ( ph -> A. x e. A ( B - C ) e. CC )
9 dmmptg
 |-  ( A. x e. A ( B - C ) e. CC -> dom ( x e. A |-> ( B - C ) ) = A )
10 8 9 syl
 |-  ( ph -> dom ( x e. A |-> ( B - C ) ) = A )
11 o1dm
 |-  ( ( x e. A |-> ( B - C ) ) e. O(1) -> dom ( x e. A |-> ( B - C ) ) C_ RR )
12 3 11 syl
 |-  ( ph -> dom ( x e. A |-> ( B - C ) ) C_ RR )
13 10 12 eqsstrrd
 |-  ( ph -> A C_ RR )
14 reex
 |-  RR e. _V
15 14 ssex
 |-  ( A C_ RR -> A e. _V )
16 13 15 syl
 |-  ( ph -> A e. _V )
17 eqidd
 |-  ( ph -> ( x e. A |-> B ) = ( x e. A |-> B ) )
18 eqidd
 |-  ( ph -> ( x e. A |-> ( B - C ) ) = ( x e. A |-> ( B - C ) ) )
19 16 1 7 17 18 offval2
 |-  ( ph -> ( ( x e. A |-> B ) oF - ( x e. A |-> ( B - C ) ) ) = ( x e. A |-> ( B - ( B - C ) ) ) )
20 1 2 nncand
 |-  ( ( ph /\ x e. A ) -> ( B - ( B - C ) ) = C )
21 20 mpteq2dva
 |-  ( ph -> ( x e. A |-> ( B - ( B - C ) ) ) = ( x e. A |-> C ) )
22 19 21 eqtrd
 |-  ( ph -> ( ( x e. A |-> B ) oF - ( x e. A |-> ( B - C ) ) ) = ( x e. A |-> C ) )
23 22 eleq1d
 |-  ( ph -> ( ( ( x e. A |-> B ) oF - ( x e. A |-> ( B - C ) ) ) e. O(1) <-> ( x e. A |-> C ) e. O(1) ) )
24 6 23 sylibd
 |-  ( ph -> ( ( x e. A |-> B ) e. O(1) -> ( x e. A |-> C ) e. O(1) ) )
25 o1add
 |-  ( ( ( x e. A |-> ( B - C ) ) e. O(1) /\ ( x e. A |-> C ) e. O(1) ) -> ( ( x e. A |-> ( B - C ) ) oF + ( x e. A |-> C ) ) e. O(1) )
26 25 ex
 |-  ( ( x e. A |-> ( B - C ) ) e. O(1) -> ( ( x e. A |-> C ) e. O(1) -> ( ( x e. A |-> ( B - C ) ) oF + ( x e. A |-> C ) ) e. O(1) ) )
27 3 26 syl
 |-  ( ph -> ( ( x e. A |-> C ) e. O(1) -> ( ( x e. A |-> ( B - C ) ) oF + ( x e. A |-> C ) ) e. O(1) ) )
28 eqidd
 |-  ( ph -> ( x e. A |-> C ) = ( x e. A |-> C ) )
29 16 7 2 18 28 offval2
 |-  ( ph -> ( ( x e. A |-> ( B - C ) ) oF + ( x e. A |-> C ) ) = ( x e. A |-> ( ( B - C ) + C ) ) )
30 1 2 npcand
 |-  ( ( ph /\ x e. A ) -> ( ( B - C ) + C ) = B )
31 30 mpteq2dva
 |-  ( ph -> ( x e. A |-> ( ( B - C ) + C ) ) = ( x e. A |-> B ) )
32 29 31 eqtrd
 |-  ( ph -> ( ( x e. A |-> ( B - C ) ) oF + ( x e. A |-> C ) ) = ( x e. A |-> B ) )
33 32 eleq1d
 |-  ( ph -> ( ( ( x e. A |-> ( B - C ) ) oF + ( x e. A |-> C ) ) e. O(1) <-> ( x e. A |-> B ) e. O(1) ) )
34 27 33 sylibd
 |-  ( ph -> ( ( x e. A |-> C ) e. O(1) -> ( x e. A |-> B ) e. O(1) ) )
35 24 34 impbid
 |-  ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> C ) e. O(1) ) )