Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem efcn 7363

Description: The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.)

Assertion

Ref	Expression
efcn

---

Proof of Theorem efcn

Step	Hyp	Ref	Expression
1		ssid 2070	. . 3
2		elcncf 7200	. . 3
3	1, 1, 2	mp2an 695	. 2
4		eff 7255	. 2
5		breq2 2613	. . . . . . 7
6		imbi1 621	. . . . . . 7
7		imbi2 622	. . . . . . 7
8	5, 6, 7	3syl 20	. . . . . 6
9	8	ralbidv2 1657	. . . . 5
10	9	rcla4ev 1868	. . . 4
11		redivclt 5756	. . . . . . 7
12		pm3.27 323	. . . . . . . . 9
13		elrp 6220	. . . . . . . . 9
14	12, 13	sylib 198	. . . . . . . 8
15	14	pm3.26d 321	. . . . . . 7
16		axaddrcl 5244	. . . . . . . 8
17		efclt 7254	. . . . . . . . . 10
18		absclt 6768	. . . . . . . . . 10
19	17, 18	syl 10	. . . . . . . . 9
20	19	adantr 389	. . . . . . . 8
21	16, 20, 15	sylanc 471	. . . . . . 7
22		gt0ne0t 5592	. . . . . . . 8
23		addgt0t 5620	. . . . . . . . 9
24		efne0t 7311	. . . . . . . . . . 11
25		absgt0t 6831	. . . . . . . . . . . 12
26	17, 25	syl 10	. . . . . . . . . . 11
27	24, 26	mpbid 195	. . . . . . . . . 10
28	27	adantr 389	. . . . . . . . 9
29	14	pm3.27d 325	. . . . . . . . 9
30	23, 20, 15, 28, 29	syl2anc 472	. . . . . . . 8
31	22, 21, 30	sylanc 471	. . . . . . 7
32	11, 15, 21, 31	syl3anc 856	. . . . . 6
33		divgt0t 5809	. . . . . . 7
34	21, 30	jca 288	. . . . . . 7
35	33, 14, 34	sylanc 471	. . . . . 6
36	32, 35	jca 288	. . . . 5
37		elrp 6220	. . . . 5
38	36, 37	sylibr 200	. . . 4
39		3ancoma 780	. . . . . . . 8
40	13	3anbi3i 824	. . . . . . . 8
41		3anass 777	. . . . . . . 8
42	39, 40, 41	3bitr3 181	. . . . . . 7
43		efcnlem4 7362	. . . . . . 7
44	42, 43	sylbir 201	. . . . . 6