Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem mulc1cncf 7214

Description: Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.)

Hypothesis

Ref	Expression
mulc1cncf.1

Assertion

Ref	Expression
mulc1cncf

Distinct variable group:   ,,

---

Proof of Theorem mulc1cncf

Step	Hyp	Ref	Expression
1		ssid 2070	. 2
2		axmulcl 5245	. . . . . . . 8
3	2	r19.21aiva 1706	. . . . . . 7
4		mulc1cncf.1	. . . . . . . 8
5	4	fopab2 3808	. . . . . . 7
6	3, 5	sylib 198	. . . . . 6
7	6	adantr 389	. . . . 5
8		1re 5407	. . . . . . . 8
9		lt01 5653	. . . . . . . 8
10	8, 9	elrpi 6221	. . . . . . 7
11	10	a1i 8	. . . . . 6
12	11	a1i 8	. . . . 5
13		opreq1 3953	. . . . . . . . . . . . 13
14	13	fveq2d 3713	. . . . . . . . . . . 12
15	14	adantr 389	. . . . . . . . . . 11
16		subdit 5399	. . . . . . . . . . . . . . 15
17	16	3expb 832	. . . . . . . . . . . . . 14
18		opreq2 3954	. . . . . . . . . . . . . . . . . . 19
19	18, 4	fvopab4g 3764	. . . . . . . . . . . . . . . . . 18
20		axmulcl 5245	. . . . . . . . . . . . . . . . . 18
21	19, 20	sylan2 451	. . . . . . . . . . . . . . . . 17
22	21	anabss7 502	. . . . . . . . . . . . . . . 16
23	22	adantrr 395	. . . . . . . . . . . . . . 15
24		opreq2 3954	. . . . . . . . . . . . . . . . . . 19
25	24, 4	fvopab4g 3764	. . . . . . . . . . . . . . . . . 18
26		axmulcl 5245	. . . . . . . . . . . . . . . . . 18
27	25, 26	sylan2 451	. . . . . . . . . . . . . . . . 17
28	27	anabss7 502	. . . . . . . . . . . . . . . 16
29	28	adantrl 394	. . . . . . . . . . . . . . 15
30	23, 29	opreq12d 3963	. . . . . . . . . . . . . 14
31	17, 30	eqtr4d 1502	. . . . . . . . . . . . 13
32	31	fveq2d 3713	. . . . . . . . . . . 12
33		0cn 5300	. . . . . . . . . . . . 13
34		eleq1 1526	. . . . . . . . . . . . 13
35	33, 34	mpbiri 194	. . . . . . . . . . . 12
36	32, 35	sylan 448	. . . . . . . . . . 11
37		subclt 5339	. . . . . . . . . . . . . . 15
38		mul02t 5416	. . . . . . . . . . . . . . 15
39	37, 38	syl 10	. . . . . . . . . . . . . 14
40	39	fveq2d 3713	. . . . . . . . . . . . 13
41		abs0 6814	. . . . . . . . . . . . 13
42	40, 41	syl6eq 1515	. . . . . . . . . . . 12
43	42	adantl 388	. . . . . . . . . . 11
44	15, 36, 43	3eqtr3d 1507	. . . . . . . . . 10
45	44	3adant3 797	. . . . . . . . 9
46		elrp 6220	. . . . . . . . . . 11
47	46	pm3.27bi 326	. . . . . . . . . 10
48	47	3ad2ant3 800	. . . . . . . . 9
49	45, 48	eqbrtrd 2625	. . . . . . . 8
50	49	a1d 12	. . . . . . 7
51	50	3adant1l 850	. . . . . 6
52	51	3expib 834	. . . . 5
53	7, 12, 52	elcncf1d 7205	. . . 4
54	53	expcom 374	. . 3
55	6	adantr 389	. . . . 5
56		redivclt 5756	. . . . . . . . . . 11
57	56	3expb 832	. . . . . . . . . 10
58	46	pm3.26bi 322	. . . . . . . . . 10
59		absclt 6768	. . . . . . . . . . . 12
60	59	adantr 389	. . . . . . . . . . 11
61		abs00t 6788	. . . . . . . . . . . . 13
62	61	necon3bid 1593	. . . . . . . . . . . 12
63	62	biimpar 417	. . . . . . . . . . 11
64	60, 63	jca 288	. . . . . . . . . 10
65	57, 58, 64	syl2an 454	. . . . . . . . 9
66		divgt0t 5809	. . . . . . . . . . 11
67	66, 46	sylanb 449	. . . . . . . . . 10
68		absgt0t 6831	. . . . . . . . . . . . 13
69	68	biimpd 153	. . . . . . . . . . . 12
70	69	imdistani 443	. . . . . . . . . . 11
71	59	anim1i 334	. . . . . . . . . . 11
72	70, 71	syl 10	. . . . . . . . . 10