Theorem efcn 7423

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

Assertion

Ref	Expression
efcn	|- exp e. (CC-cn->CC)

Proof of Theorem efcn

Step	Hyp	Ref	Expression
1		ssid 2083	. . 3 |- CC (_ CC
2		elcncf 7265	. . 3 |- ((CC (_ CC /\ CC (_ CC) -> (exp e. (CC-cn->CC) <-> (exp:CC-->CC /\ A.x e. CC A.y e. RR+ E.z e. RR+ A.w e. CC ((abs` (x - w)) < z -> (abs` ((exp` x) - (exp` w))) < y))))
3	1, 1, 2	mp2an 699	. 2 |- (exp e. (CC-cn->CC) <-> (exp:CC-->CC /\ A.x e. CC A.y e. RR+ E.z e. RR+ A.w e. CC ((abs` (x - w)) < z -> (abs` ((exp` x) - (exp` w))) < y)))
4		eff 7313	. 2 |- exp:CC-->CC
5		breq2 2628	. . . . . . 7 |- (z = (y / ((abs` (exp` x)) + y)) -> ((abs` (x - w)) < z <-> (abs` (x - w)) < (y / ((abs` (exp` x)) + y))))
6		imbi1 625	. . . . . . 7 |- (((abs` (x - w)) < z <-> (abs` (x - w)) < (y / ((abs` (exp` x)) + y))) -> (((abs` (x - w)) < z -> (abs` ((exp` x) - (exp` w))) < y) <-> ((abs` (x - w)) < (y / ((abs` (exp` x)) + y)) -> (abs` ((exp` x) - (exp` w))) < y)))
7		imbi2 626	. . . . . . 7 |- ((((abs` (x - w)) < z -> (abs` ((exp` x) - (exp` w))) < y) <-> ((abs` (x - w)) < (y / ((abs` (exp` x)) + y)) -> (abs` ((exp` x) - (exp` w))) < y)) -> ((w e. CC -> ((abs` (x - w)) < z -> (abs` ((exp` x) - (exp` w))) < y)) <-> (w e. CC -> ((abs` (x - w)) < (y / ((abs` (exp` x)) + y)) -> (abs` ((exp` x) - (exp` w))) < y))))
8	5, 6, 7	3syl 20	. . . . . 6 |- (z = (y / ((abs` (exp` x)) + y)) -> ((w e. CC -> ((abs` (x - w)) < z -> (abs` ((exp` x) - (exp` w))) < y)) <-> (w e. CC -> ((abs` (x - w)) < (y / ((abs` (exp` x)) + y)) -> (abs` ((exp` x) - (exp` w))) < y))))
9	8	ralbidv2 1668	. . . . 5 |- (z = (y / ((abs` (exp` x)) + y)) -> (A.w e. CC ((abs` (x - w)) < z -> (abs` ((exp` x) - (exp` w))) < y) <-> A.w e. CC ((abs` (x - w)) < (y / ((abs` (exp` x)) + y)) -> (abs` ((exp` x) - (exp` w))) < y)))
10	9	rcla4ev 1880	. . . 4 |- (((y / ((abs` (exp` x)) + y)) e. RR+ /\ A.w e. CC ((abs` (x - w)) < (y / ((abs` (exp` x)) + y)) -> (abs` ((exp` x) - (exp` w))) < y)) -> E.z e. RR+ A.w e. CC ((abs` (x - w)) < z -> (abs` ((exp` x) - (exp` w))) < y))
11		redivclt 5802	. . . . . . 7 |- ((y e. RR /\ ((abs` (exp` x)) + y) e. RR /\ ((abs` (exp` x)) + y) =/= 0) -> (y / ((abs` (exp` x)) + y)) e. RR)
12		pm3.27 323	. . . . . . . . 9 |- ((x e. CC /\ y e. RR+) -> y e. RR+)
13		elrp 6283	. . . . . . . . 9 |- (y e. RR+ <-> (y e. RR /\ 0 < y))
14	12, 13	sylib 198	. . . . . . . 8 |- ((x e. CC /\ y e. RR+) -> (y e. RR /\ 0 < y))
15	14	pm3.26d 321	. . . . . . 7 |- ((x e. CC /\ y e. RR+) -> y e. RR)
16		axaddrcl 5284	. . . . . . . 8 |- (((abs` (exp` x)) e. RR /\ y e. RR) -> ((abs` (exp` x)) + y) e. RR)
17		efclt 7312	. . . . . . . . . 10 |- (x e. CC -> (exp` x) e. CC)
18		absclt 6833	. . . . . . . . . 10 |- ((exp` x) e. CC -> (abs` (exp` x)) e. RR)
19	17, 18	syl 10	. . . . . . . . 9 |- (x e. CC -> (abs` (exp` x)) e. RR)
20	19	adantr 391	. . . . . . . 8 |- ((x e. CC /\ y e. RR+) -> (abs` (exp` x)) e. RR)
21	16, 20, 15	sylanc 473	. . . . . . 7 |- ((x e. CC /\ y e. RR+) -> ((abs` (exp` x)) + y) e. RR)
22		gt0ne0t 5630	. . . . . . . 8 |- ((((abs` (exp` x)) + y) e. RR /\ 0 < ((abs` (exp` x)) + y)) -> ((abs` (exp` x)) + y) =/= 0)
23		addgt0t 5659	. . . . . . . . 9 |- ((((abs` (exp` x)) e. RR /\ y e. RR) /\ (0 < (abs` (exp` x)) /\ 0 < y)) -> 0 < ((abs` (exp` x)) + y))
24		efne0t 7369	. . . . . . . . . . 11 |- (x e. CC -> (exp` x) =/= 0)
25		absgt0t 6893	. . . . . . . . . . . 12 |- ((exp` x) e. CC -> ((exp` x) =/= 0 <-> 0 < (abs` (exp` x))))
26	17, 25	syl 10	. . . . . . . . . . 11 |- (x e. CC -> ((exp` x) =/= 0 <-> 0 < (abs` (exp` x))))
27	24, 26	mpbid 195	. . . . . . . . . 10 |- (x e. CC -> 0 < (abs` (exp` x)))
28	27	adantr 391	. . . . . . . . 9 |- ((x e. CC /\ y e. RR+) -> 0 < (abs` (exp` x)))
29	14	pm3.27d 325	. . . . . . . . 9 |- ((x e. CC /\ y e. RR+) -> 0 < y)
30	23, 20, 15, 28, 29	syl2anc 474	. . . . . . . 8 |- ((x e. CC /\ y e. RR+) -> 0 < ((abs` (exp` x)) + y))
31	22, 21, 30	sylanc 473	. . . . . . 7 |- ((x e. CC /\ y e. RR+) -> ((abs` (exp` x)) + y) =/= 0)
32	11, 15, 21, 31	syl3anc 860	. . . . . 6 |- ((x e. CC /\ y e. RR+) -> (y / ((abs` (exp` x)) + y)) e. RR)
33		divgt0t 5857	. . . . . . 7 |- (((y e. RR /\ 0 < y) /\ (((abs` (exp` x)) + y) e. RR /\ 0 < ((abs` (exp` x)) + y))) -> 0 < (y / ((abs` (exp` x)) + y)))
34	21, 30	jca 288	. . . . . . 7 |- ((x e. CC /\ y e. RR+) -> (((abs` (exp` x)) + y) e. RR /\ 0 < ((abs` (exp` x)) + y)))
35	33, 14, 34	sylanc 473	. . . . . 6 |- ((x e. CC /\ y e. RR+) -> 0 < (y / ((abs` (exp` x)) + y)))
36	32, 35	jca 288	. . . . 5 |- ((x e. CC /\ y e. RR+) -> ((y / ((abs` (exp` x)) + y)) e. RR /\ 0 < (y / ((abs` (exp` x)) + y))))
37		elrp 6283	. . . . 5 |- ((y / ((abs` (exp` x)) + y)) e. RR+ <-> ((y / ((abs` (exp` x)) + y)) e. RR /\ 0 < (y / ((abs` (exp` x)) + y))))
38	36, 37	sylibr 200	. . . 4 |- ((x e. CC /\ y e. RR+) -> (y / ((abs` (exp` x)) + y)) e. RR+)
39		3ancoma 784	. . . . . . . 8 |- ((x e. CC /\ w e. CC /\ y e. RR+) <-> (w e. CC /\ x e. CC /\ y e. RR+))
40	13	3anbi3i 828	. . . . . . . 8 |- ((x e. CC /\ w e. CC /\ y e. RR+) <-> (x e. CC /\ w e. CC /\ (y e. RR /\ 0 < y)))
41		3anass 781	. . . . . . . 8 |- ((w e. CC /\ x e. CC /\ y e. RR+) <-> (w e. CC /\ (x e. CC /\ y e. RR+)))
42	39, 40, 41	3bitr3 181	. . . . . . 7 |- ((x e. CC /\ w e. CC /\ (y e. RR /\ 0 < y)) <-> (w e. CC /\ (x e. CC /\ y e. RR+)))
43		efcnlem4 7422	. . . . . . 7 |- ((x e. CC /\ w e. CC /\ (y e. RR /\ 0 < y)) -> ((abs` (x - w)) < (y / ((abs` (exp` x)) + y)) -> (abs` ((exp` x) - (exp` w))) < y))
44	42, 43	sylbir 201	. . . . . 6 |- ((w e. CC /\ (x e. CC /\ y e. RR+)) -> ((abs` (x - w)) < (y / ((abs` (exp` x)) + y)) -> (abs` ((exp` x) - (exp` w)))