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.

Step	Hyp	Ref	Expression
1		o1f 13352	. . . . 5
2	1	adantr 465	. . . 4
3		ffn 5736	. . . 4
4	2, 3	syl 16	. . 3
5		rlimf 13324	. . . . 5
6	5	adantl 466	. . . 4
7		ffn 5736	. . . 4
8	6, 7	syl 16	. . 3
9		o1dm 13353	. . . . 5
10	9	adantr 465	. . . 4
11		reex 9604	. . . 4
12		ssexg 4598	. . . 4
13	10, 11, 12	sylancl 662	. . 3
14		rlimss 13325	. . . . 5
15	14	adantl 466	. . . 4
16		ssexg 4598	. . . 4
17	15, 11, 16	sylancl 662	. . 3
18		eqid 2457	. . 3
19		eqidd 2458	. . 3
20		eqidd 2458	. . 3
21	4, 8, 13, 17, 18, 19, 20	offval 6547	. 2
22		o1bdd 13354	. . . . . . 7
23	1, 22	mpdan 668	. . . . . 6
24	23	ad2antrr 725	. . . . 5
25		fvex 5881	. . . . . . . . . 10
26	25	a1i 11	. . . . . . . . 9
27	26	ralrimiva 2871	. . . . . . . 8
28		simplr 755	. . . . . . . . 9
29		recn 9603	. . . . . . . . . . . 12
30	29	ad2antll 728	. . . . . . . . . . 11
31	30	abscld 13267	. . . . . . . . . 10
32	30	absge0d 13275	. . . . . . . . . 10
33	31, 32	ge0p1rpd 11311	. . . . . . . . 9
34	28, 33	rpdivcld 11302	. . . . . . . 8
35	6	feqmptd 5926	. . . . . . . . . 10
36		simpr 461	. . . . . . . . . 10
37	35, 36	eqbrtrrd 4474	. . . . . . . . 9
38	37	ad2antrr 725	. . . . . . . 8
39	27, 34, 38	rlimi 13336	. . . . . . 7
40		inss1 3717	. . . . . . . . . . . . . 14
41		ssralv 3563	. . . . . . . . . . . . . 14
42	40, 41	ax-mp 5	. . . . . . . . . . . . 13
43		inss2 3718	. . . . . . . . . . . . . 14
44		ssralv 3563	. . . . . . . . . . . . . 14
45	43, 44	ax-mp 5	. . . . . . . . . . . . 13
46	42, 45	anim12i 566	. . . . . . . . . . . 12
47		r19.26 2984	. . . . . . . . . . . 12
48	46, 47	sylibr 212	. . . . . . . . . . 11
49		prth 571	. . . . . . . . . . . 12
50	49	ralimi 2850	. . . . . . . . . . 11
51	48, 50	syl 16	. . . . . . . . . 10
52		simplrl 761	. . . . . . . . . . . . . . . 16
53		simprl 756	. . . . . . . . . . . . . . . 16
54	40, 10	syl5ss 3514	. . . . . . . . . . . . . . . . . 18
55	54	ad3antrrr 729	. . . . . . . . . . . . . . . . 17
56		simprr 757	. . . . . . . . . . . . . . . . 17
57	55, 56	sseldd 3504	. . . . . . . . . . . . . . . 16
58		maxle 11420	. . . . . . . . . . . . . . . 16
59	52, 53, 57, 58	syl3anc 1228	. . . . . . . . . . . . . . 15
60	59	biimpd 207	. . . . . . . . . . . . . 14
61	6	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . 21
62	43	sseli 3499	. . . . . . . . . . . . . . . . . . . . . 22
63	62	ad2antll 728	. . . . . . . . . . . . . . . . . . . . 21
64	61, 63	ffvelrnd 6032	. . . . . . . . . . . . . . . . . . . 20
65	64	subid1d 9943	. . . . . . . . . . . . . . . . . . 19
66	65	fveq2d 5875	. . . . . . . . . . . . . . . . . 18
67	66	breq1d 4462	. . . . . . . . . . . . . . . . 17
68	64	abscld 13267	. . . . . . . . . . . . . . . . . 18
69	34	adantr 465	. . . . . . . . . . . . . . . . . . 19
70	69	rpred 11285	. . . . . . . . . . . . . . . . . 18
71		ltle 9694	. . . . . . . . . . . . . . . . . 18
72	68, 70, 71	syl2anc 661	. . . . . . . . . . . . . . . . 17
73	67, 72	sylbid 215	. . . . . . . . . . . . . . . 16
74	73	anim2d 565	. . . . . . . . . . . . . . 15
75	2	ad3antrrr 729	. . . . . . . . . . . . . . . . . . 19
76	40	sseli 3499	. . . . . . . . . . . . . . . . . . . 20
77	76	ad2antll 728	. . . . . . . . . . . . . . . . . . 19
78	75, 77	ffvelrnd 6032	. . . . . . . . . . . . . . . . . 18
79	78	abscld 13267	. . . . . . . . . . . . . . . . 17
80	78	absge0d 13275	. . . . . . . . . . . . . . . . 17
81	79, 80	jca 532	. . . . . . . . . . . . . . . 16
82		simplrr 762	. . . . . . . . . . . . . . . 16
83	64	absge0d 13275	. . . . . . . . . . . . . . . . 17
84	68, 83	jca 532	. . . . . . . . . . . . . . . 16
85		lemul12a 10425	. . . . . . . . . . . . . . . 16
86	81, 82, 84, 70, 85	syl22anc 1229	. . . . . . . . . . . . . . 15
87	78, 64	absmuld 13285	. . . . . . . . . . . . . . . . 17
88	87	breq1d 4462	. . . . . . . . . . . . . . . 16
89	82	recnd 9643	. . . . . . . . . . . . . . . . . . 19
90	28	adantr 465	. . . . . . . . . . . . . . . . . . . 20
91	90	rpcnd 11287	. . . . . . . . . . . . . . . . . . 19
92	33	adantr 465	. . . . . . . . . . . . . . . . . . . 20
93	92	rpcnd 11287	. . . . . . . . . . . . . . . . . . 19
94	92	rpne0d 11290	. . . . . . . . . . . . . . . . . . 19
95	89, 91, 93, 94	divassd 10380	. . . . . . . . . . . . . . . . . 18
96		peano2re 9774	. . . . . . . . . . . . . . . . . . . . . 22
97	31, 96	syl 16	. . . . . . . . . . . . . . . . . . . . 21
98	97	adantr 465	. . . . . . . . . . . . . . . . . . . 20
99	31	adantr 465	. . . . . . . . . . . . . . . . . . . . 21
100	82	leabsd 13246	. . . . . . . . . . . . . . . . . . . . 21
101	99	ltp1d 10501	. . . . . . . . . . . . . . . . . . . . 21
102	82, 99, 98, 100, 101	lelttrd 9761	. . . . . . . . . . . . . . . . . . . 20
103	82, 98, 90, 102	ltmul1dd 11336	. . . . . . . . . . . . . . . . . . 19
104	90	rpred 11285	. . . . . . . . . . . . . . . . . . . . 21
105	82, 104	remulcld 9645	. . . . . . . . . . . . . . . . . . . 20
106	105, 104, 92	ltdivmuld 11332	. . . . . . . . . . . . . . . . . . 19
107	103, 106	mpbird 232	. . . . . . . . . . . . . . . . . 18
108	95, 107	eqbrtrrd 4474	. . . . . . . . . . . . . . . . 17
109	78, 64	mulcld 9637	. . . . . . . . . . . . . . . . . . 19
110	109	abscld 13267	. . . . . . . . . . . . . . . . . 18
111	82, 70	remulcld 9645	. . . . . . . . . . . . . . . . . 18
112		lelttr 9696	. . . . . . . . . . . . . . . . . 18
113	110, 111, 104, 112	syl3anc 1228	. . . . . . . . . . . . . . . . 17
114	108, 113	mpan2d 674	. . . . . . . . . . . . . . . 16
115	88, 114	sylbird 235	. . . . . . . . . . . . . . 15
116	74, 86, 115	3syld 55	. . . . . . . . . . . . . 14
117	60, 116	imim12d 74	. . . . . . . . . . . . 13
118	117	anassrs 648	. . . . . . . . . . . 12
119	118	ralimdva 2865	. . . . . . . . . . 11
120		simpr 461	. . . . . . . . . . . 12
121		simplrl 761	. . . . . . . . . . . 12
122	120, 121	ifcld 3984	. . . . . . . . . . 11
123	119, 122	jctild 543	. . . . . . . . . 10
124		breq1 4455	. . . . . . . . . . . . 13
125	124	imbi1d 317	. . . . . . . . . . . 12