Metamath Proof Explorer

Theorem o1mul

Description: The product 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 o1mul 
|- ( ( F e. O(1) /\ G e. O(1) ) -> ( F oF x. G ) e. O(1) )

Proof

Step Hyp Ref Expression
1 remulcl 
 |-  ( ( m e. RR /\ n e. RR ) -> ( m x. n ) e. RR )
2 mulcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
3 simp2l 
 |-  ( ( ( m e. RR /\ n e. RR ) /\ ( x e. CC /\ y e. CC ) /\ ( ( abs ` x ) <_ m /\ ( abs ` y ) <_ n ) ) -> x e. CC )
4 simp2r 
 |-  ( ( ( m e. RR /\ n e. RR ) /\ ( x e. CC /\ y e. CC ) /\ ( ( abs ` x ) <_ m /\ ( abs ` y ) <_ n ) ) -> y e. CC )
5 3 4 absmuld 
 |-  ( ( ( m e. RR /\ n e. RR ) /\ ( x e. CC /\ y e. CC ) /\ ( ( abs ` x ) <_ m /\ ( abs ` y ) <_ n ) ) -> ( abs ` ( x x. y ) ) = ( ( abs ` x ) x. ( abs ` y ) ) )
6 3 abscld 
 |-  ( ( ( m e. RR /\ n e. RR ) /\ ( x e. CC /\ y e. CC ) /\ ( ( abs ` x ) <_ m /\ ( abs ` y ) <_ n ) ) -> ( abs ` x ) e. RR )
7 simp1l 
 |-  ( ( ( m e. RR /\ n e. RR ) /\ ( x e. CC /\ y e. CC ) /\ ( ( abs ` x ) <_ m /\ ( abs ` y ) <_ n ) ) -> m e. RR )
8 4 abscld 
 |-  ( ( ( m e. RR /\ n e. RR ) /\ ( x e. CC /\ y e. CC ) /\ ( ( abs ` x ) <_ m /\ ( abs ` y ) <_ n ) ) -> ( abs ` y ) e. RR )
9 simp1r 
 |-  ( ( ( m e. RR /\ n e. RR ) /\ ( x e. CC /\ y e. CC ) /\ ( ( abs ` x ) <_ m /\ ( abs ` y ) <_ n ) ) -> n e. RR )
10 3 absge0d 
 |-  ( ( ( m e. RR /\ n e. RR ) /\ ( x e. CC /\ y e. CC ) /\ ( ( abs ` x ) <_ m /\ ( abs ` y ) <_ n ) ) -> 0 <_ ( abs ` x ) )
11 4 absge0d 
 |-  ( ( ( m e. RR /\ n e. RR ) /\ ( x e. CC /\ y e. CC ) /\ ( ( abs ` x ) <_ m /\ ( abs ` y ) <_ n ) ) -> 0 <_ ( abs ` y ) )
12 simp3l 
 |-  ( ( ( m e. RR /\ n e. RR ) /\ ( x e. CC /\ y e. CC ) /\ ( ( abs ` x ) <_ m /\ ( abs ` y ) <_ n ) ) -> ( abs ` x ) <_ m )
13 simp3r 
 |-  ( ( ( m e. RR /\ n e. RR ) /\ ( x e. CC /\ y e. CC ) /\ ( ( abs ` x ) <_ m /\ ( abs ` y ) <_ n ) ) -> ( abs ` y ) <_ n )
14 6 7 8 9 10 11 12 13 lemul12ad 
 |-  ( ( ( m e. RR /\ n e. RR ) /\ ( x e. CC /\ y e. CC ) /\ ( ( abs ` x ) <_ m /\ ( abs ` y ) <_ n ) ) -> ( ( abs ` x ) x. ( abs ` y ) ) <_ ( m x. n ) )
15 5 14 eqbrtrd 
 |-  ( ( ( m e. RR /\ n e. RR ) /\ ( x e. CC /\ y e. CC ) /\ ( ( abs ` x ) <_ m /\ ( abs ` y ) <_ n ) ) -> ( abs ` ( x x. y ) ) <_ ( m x. n ) )
16 15 3expia 
 |-  ( ( ( m e. RR /\ n e. RR ) /\ ( x e. CC /\ y e. CC ) ) -> ( ( ( abs ` x ) <_ m /\ ( abs ` y ) <_ n ) -> ( abs ` ( x x. y ) ) <_ ( m x. n ) ) )
17 1 2 16 o1of2 
 |-  ( ( F e. O(1) /\ G e. O(1) ) -> ( F oF x. G ) e. O(1) )