Metamath Proof Explorer

Theorem o1rlimmul

Description: The product of an eventually bounded function and a function of limit zero has limit zero. (Contributed by Mario Carneiro, 18-Sep-2014)

Ref Expression
Assertion o1rlimmul 
|- ( ( F e. O(1) /\ G ~~>r 0 ) -> ( F oF x. G ) ~~>r 0 )

Proof

Step Hyp Ref Expression
1 o1f 
 |-  ( F e. O(1) -> F : dom F --> CC )
2 1 adantr 
 |-  ( ( F e. O(1) /\ G ~~>r 0 ) -> F : dom F --> CC )
3 2 ffnd 
 |-  ( ( F e. O(1) /\ G ~~>r 0 ) -> F Fn dom F )
4 rlimf 
 |-  ( G ~~>r 0 -> G : dom G --> CC )
5 4 adantl 
 |-  ( ( F e. O(1) /\ G ~~>r 0 ) -> G : dom G --> CC )
6 5 ffnd 
 |-  ( ( F e. O(1) /\ G ~~>r 0 ) -> G Fn dom G )
7 o1dm 
 |-  ( F e. O(1) -> dom F C_ RR )
8 7 adantr 
 |-  ( ( F e. O(1) /\ G ~~>r 0 ) -> dom F C_ RR )
9 reex 
 |-  RR e. _V
10 ssexg 
 |-  ( ( dom F C_ RR /\ RR e. _V ) -> dom F e. _V )
11 8 9 10 sylancl 
 |-  ( ( F e. O(1) /\ G ~~>r 0 ) -> dom F e. _V )
12 rlimss 
 |-  ( G ~~>r 0 -> dom G C_ RR )
13 12 adantl 
 |-  ( ( F e. O(1) /\ G ~~>r 0 ) -> dom G C_ RR )
14 ssexg 
 |-  ( ( dom G C_ RR /\ RR e. _V ) -> dom G e. _V )
15 13 9 14 sylancl 
 |-  ( ( F e. O(1) /\ G ~~>r 0 ) -> dom G e. _V )
16 eqid 
 |-  ( dom F i^i dom G ) = ( dom F i^i dom G )
17 eqidd 
 |-  ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ x e. dom F ) -> ( F ` x ) = ( F ` x ) )
18 eqidd 
 |-  ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ x e. dom G ) -> ( G ` x ) = ( G ` x ) )
19 3 6 11 15 16 17 18 offval 
 |-  ( ( F e. O(1) /\ G ~~>r 0 ) -> ( F oF x. G ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) x. ( G ` x ) ) ) )
20 o1bdd 
 |-  ( ( F e. O(1) /\ F : dom F --> CC ) -> E. a e. RR E. m e. RR A. x e. dom F ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) )
21 1 20 mpdan 
 |-  ( F e. O(1) -> E. a e. RR E. m e. RR A. x e. dom F ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) )
22 21 ad2antrr 
 |-  ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) -> E. a e. RR E. m e. RR A. x e. dom F ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) )
23 fvexd 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ x e. dom G ) -> ( G ` x ) e. _V )
24 23 ralrimiva 
 |-  ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) -> A. x e. dom G ( G ` x ) e. _V )
25 simplr 
 |-  ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) -> y e. RR+ )
26 recn 
 |-  ( m e. RR -> m e. CC )
27 26 ad2antll 
 |-  ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) -> m e. CC )
28 27 abscld 
 |-  ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) -> ( abs ` m ) e. RR )
29 27 absge0d 
 |-  ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) -> 0 <_ ( abs ` m ) )
30 28 29 ge0p1rpd 
 |-  ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) -> ( ( abs ` m ) + 1 ) e. RR+ )
31 25 30 rpdivcld 
 |-  ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) -> ( y / ( ( abs ` m ) + 1 ) ) e. RR+ )
32 5 feqmptd 
 |-  ( ( F e. O(1) /\ G ~~>r 0 ) -> G = ( x e. dom G |-> ( G ` x ) ) )
33 simpr 
 |-  ( ( F e. O(1) /\ G ~~>r 0 ) -> G ~~>r 0 )
34 32 33 eqbrtrrd 
 |-  ( ( F e. O(1) /\ G ~~>r 0 ) -> ( x e. dom G |-> ( G ` x ) ) ~~>r 0 )
35 34 ad2antrr 
 |-  ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) -> ( x e. dom G |-> ( G ` x ) ) ~~>r 0 )
36 24 31 35 rlimi 
 |-  ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) -> E. b e. RR A. x e. dom G ( b <_ x -> ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) )
37 inss1 
 |-  ( dom F i^i dom G ) C_ dom F
38 ssralv 
 |-  ( ( dom F i^i dom G ) C_ dom F -> ( A. x e. dom F ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) -> A. x e. ( dom F i^i dom G ) ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) ) )
39 37 38 ax-mp 
 |-  ( A. x e. dom F ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) -> A. x e. ( dom F i^i dom G ) ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) )
40 inss2 
 |-  ( dom F i^i dom G ) C_ dom G
41 ssralv 
 |-  ( ( dom F i^i dom G ) C_ dom G -> ( A. x e. dom G ( b <_ x -> ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) -> A. x e. ( dom F i^i dom G ) ( b <_ x -> ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) ) )
42 40 41 ax-mp 
 |-  ( A. x e. dom G ( b <_ x -> ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) -> A. x e. ( dom F i^i dom G ) ( b <_ x -> ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) )
43 39 42 anim12i 
 |-  ( ( A. x e. dom F ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) /\ A. x e. dom G ( b <_ x -> ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) ) -> ( A. x e. ( dom F i^i dom G ) ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) /\ A. x e. ( dom F i^i dom G ) ( b <_ x -> ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) ) )
44 r19.26 
 |-  ( A. x e. ( dom F i^i dom G ) ( ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) /\ ( b <_ x -> ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) ) <-> ( A. x e. ( dom F i^i dom G ) ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) /\ A. x e. ( dom F i^i dom G ) ( b <_ x -> ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) ) )
45 43 44 sylibr 
 |-  ( ( A. x e. dom F ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) /\ A. x e. dom G ( b <_ x -> ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) ) -> A. x e. ( dom F i^i dom G ) ( ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) /\ ( b <_ x -> ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) ) )
46 anim12 
 |-  ( ( ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) /\ ( b <_ x -> ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) ) -> ( ( a <_ x /\ b <_ x ) -> ( ( abs ` ( F ` x ) ) <_ m /\ ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) ) )
47 46 ralimi 
 |-  ( A. x e. ( dom F i^i dom G ) ( ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) /\ ( b <_ x -> ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) ) -> A. x e. ( dom F i^i dom G ) ( ( a <_ x /\ b <_ x ) -> ( ( abs ` ( F ` x ) ) <_ m /\ ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) ) )
48 45 47 syl 
 |-  ( ( A. x e. dom F ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) /\ A. x e. dom G ( b <_ x -> ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) ) -> A. x e. ( dom F i^i dom G ) ( ( a <_ x /\ b <_ x ) -> ( ( abs ` ( F ` x ) ) <_ m /\ ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) ) )
49 simplrl 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> a e. RR )
50 simprl 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> b e. RR )
51 37 8 sstrid 
 |-  ( ( F e. O(1) /\ G ~~>r 0 ) -> ( dom F i^i dom G ) C_ RR )
52 51 ad3antrrr 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( dom F i^i dom G ) C_ RR )
53 simprr 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> x e. ( dom F i^i dom G ) )
54 52 53 sseldd 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> x e. RR )
55 maxle 
 |-  ( ( a e. RR /\ b e. RR /\ x e. RR ) -> ( if ( a <_ b , b , a ) <_ x <-> ( a <_ x /\ b <_ x ) ) )
56 49 50 54 55 syl3anc 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( if ( a <_ b , b , a ) <_ x <-> ( a <_ x /\ b <_ x ) ) )
57 56 biimpd 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( if ( a <_ b , b , a ) <_ x -> ( a <_ x /\ b <_ x ) ) )
58 5 ad3antrrr 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> G : dom G --> CC )
59 40 sseli 
 |-  ( x e. ( dom F i^i dom G ) -> x e. dom G )
60 59 ad2antll 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> x e. dom G )
61 58 60 ffvelrnd 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( G ` x ) e. CC )
62 61 subid1d 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( G ` x ) - 0 ) = ( G ` x ) )
63 62 fveq2d 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( abs ` ( ( G ` x ) - 0 ) ) = ( abs ` ( G ` x ) ) )
64 63 breq1d 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) <-> ( abs ` ( G ` x ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) )
65 61 abscld 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( abs ` ( G ` x ) ) e. RR )
66 31 adantr 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( y / ( ( abs ` m ) + 1 ) ) e. RR+ )
67 66 rpred 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( y / ( ( abs ` m ) + 1 ) ) e. RR )
68 ltle 
 |-  ( ( ( abs ` ( G ` x ) ) e. RR /\ ( y / ( ( abs ` m ) + 1 ) ) e. RR ) -> ( ( abs ` ( G ` x ) ) < ( y / ( ( abs ` m ) + 1 ) ) -> ( abs ` ( G ` x ) ) <_ ( y / ( ( abs ` m ) + 1 ) ) ) )
69 65 67 68 syl2anc 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( abs ` ( G ` x ) ) < ( y / ( ( abs ` m ) + 1 ) ) -> ( abs ` ( G ` x ) ) <_ ( y / ( ( abs ` m ) + 1 ) ) ) )
70 64 69 sylbid 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) -> ( abs ` ( G ` x ) ) <_ ( y / ( ( abs ` m ) + 1 ) ) ) )
71 70 anim2d 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( ( abs ` ( F ` x ) ) <_ m /\ ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) -> ( ( abs ` ( F ` x ) ) <_ m /\ ( abs ` ( G ` x ) ) <_ ( y / ( ( abs ` m ) + 1 ) ) ) ) )
72 2 ad3antrrr 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> F : dom F --> CC )
73 37 sseli 
 |-  ( x e. ( dom F i^i dom G ) -> x e. dom F )
74 73 ad2antll 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> x e. dom F )
75 72 74 ffvelrnd 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( F ` x ) e. CC )
76 75 abscld 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( abs ` ( F ` x ) ) e. RR )
77 75 absge0d 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> 0 <_ ( abs ` ( F ` x ) ) )
78 76 77 jca 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( abs ` ( F ` x ) ) e. RR /\ 0 <_ ( abs ` ( F ` x ) ) ) )
79 simplrr 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> m e. RR )
80 61 absge0d 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> 0 <_ ( abs ` ( G ` x ) ) )
81 65 80 jca 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( abs ` ( G ` x ) ) e. RR /\ 0 <_ ( abs ` ( G ` x ) ) ) )
82 lemul12a 
 |-  ( ( ( ( ( abs ` ( F ` x ) ) e. RR /\ 0 <_ ( abs ` ( F ` x ) ) ) /\ m e. RR ) /\ ( ( ( abs ` ( G ` x ) ) e. RR /\ 0 <_ ( abs ` ( G ` x ) ) ) /\ ( y / ( ( abs ` m ) + 1 ) ) e. RR ) ) -> ( ( ( abs ` ( F ` x ) ) <_ m /\ ( abs ` ( G ` x ) ) <_ ( y / ( ( abs ` m ) + 1 ) ) ) -> ( ( abs ` ( F ` x ) ) x. ( abs ` ( G ` x ) ) ) <_ ( m x. ( y / ( ( abs ` m ) + 1 ) ) ) ) )
83 78 79 81 67 82 syl22anc 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( ( abs ` ( F ` x ) ) <_ m /\ ( abs ` ( G ` x ) ) <_ ( y / ( ( abs ` m ) + 1 ) ) ) -> ( ( abs ` ( F ` x ) ) x. ( abs ` ( G ` x ) ) ) <_ ( m x. ( y / ( ( abs ` m ) + 1 ) ) ) ) )
84 75 61 absmuld 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) = ( ( abs ` ( F ` x ) ) x. ( abs ` ( G ` x ) ) ) )
85 84 breq1d 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) <_ ( m x. ( y / ( ( abs ` m ) + 1 ) ) ) <-> ( ( abs ` ( F ` x ) ) x. ( abs ` ( G ` x ) ) ) <_ ( m x. ( y / ( ( abs ` m ) + 1 ) ) ) ) )
86 79 recnd 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> m e. CC )
87 25 adantr 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> y e. RR+ )
88 87 rpcnd 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> y e. CC )
89 30 adantr 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( abs ` m ) + 1 ) e. RR+ )
90 89 rpcnd 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( abs ` m ) + 1 ) e. CC )
91 89 rpne0d 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( abs ` m ) + 1 ) =/= 0 )
92 86 88 90 91 divassd 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( m x. y ) / ( ( abs ` m ) + 1 ) ) = ( m x. ( y / ( ( abs ` m ) + 1 ) ) ) )
93 peano2re 
 |-  ( ( abs ` m ) e. RR -> ( ( abs ` m ) + 1 ) e. RR )
94 28 93 syl 
 |-  ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) -> ( ( abs ` m ) + 1 ) e. RR )
95 94 adantr 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( abs ` m ) + 1 ) e. RR )
96 28 adantr 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( abs ` m ) e. RR )
97 79 leabsd 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> m <_ ( abs ` m ) )
98 96 ltp1d 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( abs ` m ) < ( ( abs ` m ) + 1 ) )
99 79 96 95 97 98 lelttrd 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> m < ( ( abs ` m ) + 1 ) )
100 79 95 87 99 ltmul1dd 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( m x. y ) < ( ( ( abs ` m ) + 1 ) x. y ) )
101 87 rpred 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> y e. RR )
102 79 101 remulcld 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( m x. y ) e. RR )
103 102 101 89 ltdivmuld 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( ( m x. y ) / ( ( abs ` m ) + 1 ) ) < y <-> ( m x. y ) < ( ( ( abs ` m ) + 1 ) x. y ) ) )
104 100 103 mpbird 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( m x. y ) / ( ( abs ` m ) + 1 ) ) < y )
105 92 104 eqbrtrrd 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( m x. ( y / ( ( abs ` m ) + 1 ) ) ) < y )
106 75 61 mulcld 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( F ` x ) x. ( G ` x ) ) e. CC )
107 106 abscld 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) e. RR )
108 79 67 remulcld 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( m x. ( y / ( ( abs ` m ) + 1 ) ) ) e. RR )
109 lelttr 
 |-  ( ( ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) e. RR /\ ( m x. ( y / ( ( abs ` m ) + 1 ) ) ) e. RR /\ y e. RR ) -> ( ( ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) <_ ( m x. ( y / ( ( abs ` m ) + 1 ) ) ) /\ ( m x. ( y / ( ( abs ` m ) + 1 ) ) ) < y ) -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) )
110 107 108 101 109 syl3anc 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) <_ ( m x. ( y / ( ( abs ` m ) + 1 ) ) ) /\ ( m x. ( y / ( ( abs ` m ) + 1 ) ) ) < y ) -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) )
111 105 110 mpan2d 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) <_ ( m x. ( y / ( ( abs ` m ) + 1 ) ) ) -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) )
112 85 111 sylbird 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( ( abs ` ( F ` x ) ) x. ( abs ` ( G ` x ) ) ) <_ ( m x. ( y / ( ( abs ` m ) + 1 ) ) ) -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) )
113 71 83 112 3syld 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( ( abs ` ( F ` x ) ) <_ m /\ ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) )
114 57 113 imim12d 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ ( b e. RR /\ x e. ( dom F i^i dom G ) ) ) -> ( ( ( a <_ x /\ b <_ x ) -> ( ( abs ` ( F ` x ) ) <_ m /\ ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) ) -> ( if ( a <_ b , b , a ) <_ x -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) ) )
115 114 anassrs 
 |-  ( ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ b e. RR ) /\ x e. ( dom F i^i dom G ) ) -> ( ( ( a <_ x /\ b <_ x ) -> ( ( abs ` ( F ` x ) ) <_ m /\ ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) ) -> ( if ( a <_ b , b , a ) <_ x -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) ) )
116 115 ralimdva 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ b e. RR ) -> ( A. x e. ( dom F i^i dom G ) ( ( a <_ x /\ b <_ x ) -> ( ( abs ` ( F ` x ) ) <_ m /\ ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) ) -> A. x e. ( dom F i^i dom G ) ( if ( a <_ b , b , a ) <_ x -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) ) )
117 simpr 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ b e. RR ) -> b e. RR )
118 simplrl 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ b e. RR ) -> a e. RR )
119 117 118 ifcld 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ b e. RR ) -> if ( a <_ b , b , a ) e. RR )
120 116 119 jctild 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ b e. RR ) -> ( A. x e. ( dom F i^i dom G ) ( ( a <_ x /\ b <_ x ) -> ( ( abs ` ( F ` x ) ) <_ m /\ ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) ) -> ( if ( a <_ b , b , a ) e. RR /\ A. x e. ( dom F i^i dom G ) ( if ( a <_ b , b , a ) <_ x -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) ) ) )
121 breq1 
 |-  ( z = if ( a <_ b , b , a ) -> ( z <_ x <-> if ( a <_ b , b , a ) <_ x ) )
122 121 rspceaimv 
 |-  ( ( if ( a <_ b , b , a ) e. RR /\ A. x e. ( dom F i^i dom G ) ( if ( a <_ b , b , a ) <_ x -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) ) -> E. z e. RR A. x e. ( dom F i^i dom G ) ( z <_ x -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) )
123 48 120 122 syl56 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ b e. RR ) -> ( ( A. x e. dom F ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) /\ A. x e. dom G ( b <_ x -> ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) ) -> E. z e. RR A. x e. ( dom F i^i dom G ) ( z <_ x -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) ) )
124 123 expcomd 
 |-  ( ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) /\ b e. RR ) -> ( A. x e. dom G ( b <_ x -> ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) -> ( A. x e. dom F ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) -> E. z e. RR A. x e. ( dom F i^i dom G ) ( z <_ x -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) ) ) )
125 124 rexlimdva 
 |-  ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) -> ( E. b e. RR A. x e. dom G ( b <_ x -> ( abs ` ( ( G ` x ) - 0 ) ) < ( y / ( ( abs ` m ) + 1 ) ) ) -> ( A. x e. dom F ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) -> E. z e. RR A. x e. ( dom F i^i dom G ) ( z <_ x -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) ) ) )
126 36 125 mpd 
 |-  ( ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) /\ ( a e. RR /\ m e. RR ) ) -> ( A. x e. dom F ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) -> E. z e. RR A. x e. ( dom F i^i dom G ) ( z <_ x -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) ) )
127 126 rexlimdvva 
 |-  ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) -> ( E. a e. RR E. m e. RR A. x e. dom F ( a <_ x -> ( abs ` ( F ` x ) ) <_ m ) -> E. z e. RR A. x e. ( dom F i^i dom G ) ( z <_ x -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) ) )
128 22 127 mpd 
 |-  ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ y e. RR+ ) -> E. z e. RR A. x e. ( dom F i^i dom G ) ( z <_ x -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) )
129 128 ralrimiva 
 |-  ( ( F e. O(1) /\ G ~~>r 0 ) -> A. y e. RR+ E. z e. RR A. x e. ( dom F i^i dom G ) ( z <_ x -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) )
130 ffvelrn 
 |-  ( ( F : dom F --> CC /\ x e. dom F ) -> ( F ` x ) e. CC )
131 2 73 130 syl2an 
 |-  ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ x e. ( dom F i^i dom G ) ) -> ( F ` x ) e. CC )
132 ffvelrn 
 |-  ( ( G : dom G --> CC /\ x e. dom G ) -> ( G ` x ) e. CC )
133 5 59 132 syl2an 
 |-  ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ x e. ( dom F i^i dom G ) ) -> ( G ` x ) e. CC )
134 131 133 mulcld 
 |-  ( ( ( F e. O(1) /\ G ~~>r 0 ) /\ x e. ( dom F i^i dom G ) ) -> ( ( F ` x ) x. ( G ` x ) ) e. CC )
135 134 ralrimiva 
 |-  ( ( F e. O(1) /\ G ~~>r 0 ) -> A. x e. ( dom F i^i dom G ) ( ( F ` x ) x. ( G ` x ) ) e. CC )
136 135 51 rlim0 
 |-  ( ( F e. O(1) /\ G ~~>r 0 ) -> ( ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) x. ( G ` x ) ) ) ~~>r 0 <-> A. y e. RR+ E. z e. RR A. x e. ( dom F i^i dom G ) ( z <_ x -> ( abs ` ( ( F ` x ) x. ( G ` x ) ) ) < y ) ) )
137 129 136 mpbird 
 |-  ( ( F e. O(1) /\ G ~~>r 0 ) -> ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) x. ( G ` x ) ) ) ~~>r 0 )
138 19 137 eqbrtrd 
 |-  ( ( F e. O(1) /\ G ~~>r 0 ) -> ( F oF x. G ) ~~>r 0 )