MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  o1rlimmul Unicode version

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

Proof of Theorem o1rlimmul
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 o1f 13352 . . . . 5
21adantr 465 . . . 4
3 ffn 5736 . . . 4
42, 3syl 16 . . 3
5 rlimf 13324 . . . . 5
65adantl 466 . . . 4
7 ffn 5736 . . . 4
86, 7syl 16 . . 3
9 o1dm 13353 . . . . 5
109adantr 465 . . . 4
11 reex 9604 . . . 4
12 ssexg 4598 . . . 4
1310, 11, 12sylancl 662 . . 3
14 rlimss 13325 . . . . 5
1514adantl 466 . . . 4
16 ssexg 4598 . . . 4
1715, 11, 16sylancl 662 . . 3
18 eqid 2457 . . 3
19 eqidd 2458 . . 3
20 eqidd 2458 . . 3
214, 8, 13, 17, 18, 19, 20offval 6547 . 2
22 o1bdd 13354 . . . . . . 7
231, 22mpdan 668 . . . . . 6
2423ad2antrr 725 . . . . 5
25 fvex 5881 . . . . . . . . . 10
2625a1i 11 . . . . . . . . 9
2726ralrimiva 2871 . . . . . . . 8
28 simplr 755 . . . . . . . . 9
29 recn 9603 . . . . . . . . . . . 12
3029ad2antll 728 . . . . . . . . . . 11
3130abscld 13267 . . . . . . . . . 10
3230absge0d 13275 . . . . . . . . . 10
3331, 32ge0p1rpd 11311 . . . . . . . . 9
3428, 33rpdivcld 11302 . . . . . . . 8
356feqmptd 5926 . . . . . . . . . 10
36 simpr 461 . . . . . . . . . 10
3735, 36eqbrtrrd 4474 . . . . . . . . 9
3837ad2antrr 725 . . . . . . . 8
3927, 34, 38rlimi 13336 . . . . . . 7
40 inss1 3717 . . . . . . . . . . . . . 14
41 ssralv 3563 . . . . . . . . . . . . . 14
4240, 41ax-mp 5 . . . . . . . . . . . . 13
43 inss2 3718 . . . . . . . . . . . . . 14
44 ssralv 3563 . . . . . . . . . . . . . 14
4543, 44ax-mp 5 . . . . . . . . . . . . 13
4642, 45anim12i 566 . . . . . . . . . . . 12
47 r19.26 2984 . . . . . . . . . . . 12
4846, 47sylibr 212 . . . . . . . . . . 11
49 prth 571 . . . . . . . . . . . 12
5049ralimi 2850 . . . . . . . . . . 11
5148, 50syl 16 . . . . . . . . . 10
52 simplrl 761 . . . . . . . . . . . . . . . 16
53 simprl 756 . . . . . . . . . . . . . . . 16
5440, 10syl5ss 3514 . . . . . . . . . . . . . . . . . 18
5554ad3antrrr 729 . . . . . . . . . . . . . . . . 17
56 simprr 757 . . . . . . . . . . . . . . . . 17
5755, 56sseldd 3504 . . . . . . . . . . . . . . . 16
58 maxle 11420 . . . . . . . . . . . . . . . 16
5952, 53, 57, 58syl3anc 1228 . . . . . . . . . . . . . . 15
6059biimpd 207 . . . . . . . . . . . . . 14
616ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21
6243sseli 3499 . . . . . . . . . . . . . . . . . . . . . 22
6362ad2antll 728 . . . . . . . . . . . . . . . . . . . . 21
6461, 63ffvelrnd 6032 . . . . . . . . . . . . . . . . . . . 20
6564subid1d 9943 . . . . . . . . . . . . . . . . . . 19
6665fveq2d 5875 . . . . . . . . . . . . . . . . . 18
6766breq1d 4462 . . . . . . . . . . . . . . . . 17
6864abscld 13267 . . . . . . . . . . . . . . . . . 18
6934adantr 465 . . . . . . . . . . . . . . . . . . 19
7069rpred 11285 . . . . . . . . . . . . . . . . . 18
71 ltle 9694 . . . . . . . . . . . . . . . . . 18
7268, 70, 71syl2anc 661 . . . . . . . . . . . . . . . . 17
7367, 72sylbid 215 . . . . . . . . . . . . . . . 16
7473anim2d 565 . . . . . . . . . . . . . . 15
752ad3antrrr 729 . . . . . . . . . . . . . . . . . . 19
7640sseli 3499 . . . . . . . . . . . . . . . . . . . 20
7776ad2antll 728 . . . . . . . . . . . . . . . . . . 19
7875, 77ffvelrnd 6032 . . . . . . . . . . . . . . . . . 18
7978abscld 13267 . . . . . . . . . . . . . . . . 17
8078absge0d 13275 . . . . . . . . . . . . . . . . 17
8179, 80jca 532 . . . . . . . . . . . . . . . 16
82 simplrr 762 . . . . . . . . . . . . . . . 16
8364absge0d 13275 . . . . . . . . . . . . . . . . 17
8468, 83jca 532 . . . . . . . . . . . . . . . 16
85 lemul12a 10425 . . . . . . . . . . . . . . . 16
8681, 82, 84, 70, 85syl22anc 1229 . . . . . . . . . . . . . . 15
8778, 64absmuld 13285 . . . . . . . . . . . . . . . . 17
8887breq1d 4462 . . . . . . . . . . . . . . . 16
8982recnd 9643 . . . . . . . . . . . . . . . . . . 19
9028adantr 465 . . . . . . . . . . . . . . . . . . . 20
9190rpcnd 11287 . . . . . . . . . . . . . . . . . . 19
9233adantr 465 . . . . . . . . . . . . . . . . . . . 20
9392rpcnd 11287 . . . . . . . . . . . . . . . . . . 19
9492rpne0d 11290 . . . . . . . . . . . . . . . . . . 19
9589, 91, 93, 94divassd 10380 . . . . . . . . . . . . . . . . . 18
96 peano2re 9774 . . . . . . . . . . . . . . . . . . . . . 22
9731, 96syl 16 . . . . . . . . . . . . . . . . . . . . 21
9897adantr 465 . . . . . . . . . . . . . . . . . . . 20
9931adantr 465 . . . . . . . . . . . . . . . . . . . . 21
10082leabsd 13246 . . . . . . . . . . . . . . . . . . . . 21
10199ltp1d 10501 . . . . . . . . . . . . . . . . . . . . 21
10282, 99, 98, 100, 101lelttrd 9761 . . . . . . . . . . . . . . . . . . . 20
10382, 98, 90, 102ltmul1dd 11336 . . . . . . . . . . . . . . . . . . 19
10490rpred 11285 . . . . . . . . . . . . . . . . . . . . 21
10582, 104remulcld 9645 . . . . . . . . . . . . . . . . . . . 20
106105, 104, 92ltdivmuld 11332 . . . . . . . . . . . . . . . . . . 19
107103, 106mpbird 232 . . . . . . . . . . . . . . . . . 18
10895, 107eqbrtrrd 4474 . . . . . . . . . . . . . . . . 17
10978, 64mulcld 9637 . . . . . . . . . . . . . . . . . . 19
110109abscld 13267 . . . . . . . . . . . . . . . . . 18
11182, 70remulcld 9645 . . . . . . . . . . . . . . . . . 18
112 lelttr 9696 . . . . . . . . . . . . . . . . . 18
113110, 111, 104, 112syl3anc 1228 . . . . . . . . . . . . . . . . 17
114108, 113mpan2d 674 . . . . . . . . . . . . . . . 16
11588, 114sylbird 235 . . . . . . . . . . . . . . 15
11674, 86, 1153syld 55 . . . . . . . . . . . . . 14
11760, 116imim12d 74 . . . . . . . . . . . . 13
118117anassrs 648 . . . . . . . . . . . 12
119118ralimdva 2865 . . . . . . . . . . 11
120 simpr 461 . . . . . . . . . . . 12
121 simplrl 761 . . . . . . . . . . . 12
122120, 121ifcld 3984 . . . . . . . . . . 11
123119, 122jctild 543 . . . . . . . . . 10
124 breq1 4455 . . . . . . . . . . . . 13
125124imbi1d 317 . . . . . . . . . . . 12