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 )