Metamath Proof Explorer

Theorem o1sub

Description: The difference of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014) (Proof shortened by Fan Zheng, 14-Jul-2016)

Ref Expression
Assertion o1sub 
|- ( ( F e. O(1) /\ G e. O(1) ) -> ( F oF - G ) e. O(1) )

Proof

Step Hyp Ref Expression
1 readdcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x + y ) e. RR )
2 subcl 
 |-  ( ( m e. CC /\ n e. CC ) -> ( m - n ) e. CC )
3 simp2l 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( m e. CC /\ n e. CC ) /\ ( ( abs ` m ) <_ x /\ ( abs ` n ) <_ y ) ) -> m e. CC )
4 simp2r 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( m e. CC /\ n e. CC ) /\ ( ( abs ` m ) <_ x /\ ( abs ` n ) <_ y ) ) -> n e. CC )
5 3 4 subcld 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( m e. CC /\ n e. CC ) /\ ( ( abs ` m ) <_ x /\ ( abs ` n ) <_ y ) ) -> ( m - n ) e. CC )
6 5 abscld 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( m e. CC /\ n e. CC ) /\ ( ( abs ` m ) <_ x /\ ( abs ` n ) <_ y ) ) -> ( abs ` ( m - n ) ) e. RR )
7 3 abscld 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( m e. CC /\ n e. CC ) /\ ( ( abs ` m ) <_ x /\ ( abs ` n ) <_ y ) ) -> ( abs ` m ) e. RR )
8 4 abscld 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( m e. CC /\ n e. CC ) /\ ( ( abs ` m ) <_ x /\ ( abs ` n ) <_ y ) ) -> ( abs ` n ) e. RR )
9 7 8 readdcld 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( m e. CC /\ n e. CC ) /\ ( ( abs ` m ) <_ x /\ ( abs ` n ) <_ y ) ) -> ( ( abs ` m ) + ( abs ` n ) ) e. RR )
10 simp1l 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( m e. CC /\ n e. CC ) /\ ( ( abs ` m ) <_ x /\ ( abs ` n ) <_ y ) ) -> x e. RR )
11 simp1r 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( m e. CC /\ n e. CC ) /\ ( ( abs ` m ) <_ x /\ ( abs ` n ) <_ y ) ) -> y e. RR )
12 10 11 readdcld 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( m e. CC /\ n e. CC ) /\ ( ( abs ` m ) <_ x /\ ( abs ` n ) <_ y ) ) -> ( x + y ) e. RR )
13 3 4 abs2dif2d 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( m e. CC /\ n e. CC ) /\ ( ( abs ` m ) <_ x /\ ( abs ` n ) <_ y ) ) -> ( abs ` ( m - n ) ) <_ ( ( abs ` m ) + ( abs ` n ) ) )
14 simp3l 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( m e. CC /\ n e. CC ) /\ ( ( abs ` m ) <_ x /\ ( abs ` n ) <_ y ) ) -> ( abs ` m ) <_ x )
15 simp3r 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( m e. CC /\ n e. CC ) /\ ( ( abs ` m ) <_ x /\ ( abs ` n ) <_ y ) ) -> ( abs ` n ) <_ y )
16 7 8 10 11 14 15 le2addd 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( m e. CC /\ n e. CC ) /\ ( ( abs ` m ) <_ x /\ ( abs ` n ) <_ y ) ) -> ( ( abs ` m ) + ( abs ` n ) ) <_ ( x + y ) )
17 6 9 12 13 16 letrd 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( m e. CC /\ n e. CC ) /\ ( ( abs ` m ) <_ x /\ ( abs ` n ) <_ y ) ) -> ( abs ` ( m - n ) ) <_ ( x + y ) )
18 17 3expia 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( m e. CC /\ n e. CC ) ) -> ( ( ( abs ` m ) <_ x /\ ( abs ` n ) <_ y ) -> ( abs ` ( m - n ) ) <_ ( x + y ) ) )
19 1 2 18 o1of2 
 |-  ( ( F e. O(1) /\ G e. O(1) ) -> ( F oF - G ) e. O(1) )