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) ) )