Theorem ef0lem

Description: The series defining the exponential function converges in the (trivial) case of a zero argument. (Contributed by Steve Rodriguez, 7-Jun-2006) (Revised by Mario Carneiro, 28-Apr-2014)

	Ref	Expression
Hypothesis	eftval.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)$$
Assertion	ef0lem	$$⊢A=0\to seq0\left(+,F\right)⇝1$$

Proof

Step	Hyp	Ref	Expression
1		eftval.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)$$
2		simpr	$$⊢\left(A=0\wedge k\in {\mathbb{Z}}_{\ge 0}\right)\to k\in {\mathbb{Z}}_{\ge 0}$$
3		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
4	2 3	eleqtrrdi	$$⊢\left(A=0\wedge k\in {\mathbb{Z}}_{\ge 0}\right)\to k\in {\mathbb{N}}_0$$
5		elnn0	$$⊢k\in {\mathbb{N}}_0\leftrightarrow \left(k\in \mathbb{N}\vee k=0\right)$$
6	4 5	sylib	$$⊢\left(A=0\wedge k\in {\mathbb{Z}}_{\ge 0}\right)\to \left(k\in \mathbb{N}\vee k=0\right)$$
7		nnnn0	$$⊢k\in \mathbb{N}\to k\in {\mathbb{N}}_0$$
8	7	adantl	$$⊢\left(A=0\wedge k\in \mathbb{N}\right)\to k\in {\mathbb{N}}_0$$
9	1	eftval	$$⊢k\in {\mathbb{N}}_0\to F\left(k\right)=\frac{A^k}{k!}$$
10	8 9	syl	$$⊢\left(A=0\wedge k\in \mathbb{N}\right)\to F\left(k\right)=\frac{A^k}{k!}$$
11		oveq1	$$⊢A=0\to A^k=0^k$$
12		0exp	$$⊢k\in \mathbb{N}\to 0^k=0$$
13	11 12	sylan9eq	$$⊢\left(A=0\wedge k\in \mathbb{N}\right)\to A^k=0$$
14	13	oveq1d	$$⊢\left(A=0\wedge k\in \mathbb{N}\right)\to \frac{A^k}{k!}=\frac{0}{k!}$$
15		faccl	$$⊢k\in {\mathbb{N}}_0\to k!\in \mathbb{N}$$
16		nncn	$$⊢k!\in \mathbb{N}\to k!\in ℂ$$
17		nnne0	$$⊢k!\in \mathbb{N}\to k!\ne 0$$
18	16 17	div0d	$$⊢k!\in \mathbb{N}\to \frac{0}{k!}=0$$
19	8 15 18	3syl	$$⊢\left(A=0\wedge k\in \mathbb{N}\right)\to \frac{0}{k!}=0$$
20	10 14 19	3eqtrd	$$⊢\left(A=0\wedge k\in \mathbb{N}\right)\to F\left(k\right)=0$$
21		nnne0	$$⊢k\in \mathbb{N}\to k\ne 0$$
22		velsn	$$⊢k\in \left\{0\right\}\leftrightarrow k=0$$
23	22	necon3bbii	$$⊢\neg k\in \left\{0\right\}\leftrightarrow k\ne 0$$
24	21 23	sylibr	$$⊢k\in \mathbb{N}\to \neg k\in \left\{0\right\}$$
25	24	adantl	$$⊢\left(A=0\wedge k\in \mathbb{N}\right)\to \neg k\in \left\{0\right\}$$
26	25	iffalsed	$$⊢\left(A=0\wedge k\in \mathbb{N}\right)\to if\left(k\in \left\{0\right\},1,0\right)=0$$
27	20 26	eqtr4d	$$⊢\left(A=0\wedge k\in \mathbb{N}\right)\to F\left(k\right)=if\left(k\in \left\{0\right\},1,0\right)$$
28		fveq2	$$⊢k=0\to F\left(k\right)=F\left(0\right)$$
29		oveq1	$$⊢A=0\to A^0=0^0$$
30		0exp0e1	$$⊢0^0=1$$
31	29 30	syl6eq	$$⊢A=0\to A^0=1$$
32	31	oveq1d	$$⊢A=0\to \frac{A^0}{0!}=\frac{1}{0!}$$
33		0nn0	$$⊢0\in {\mathbb{N}}_0$$
34	1	eftval	$$⊢0\in {\mathbb{N}}_0\to F\left(0\right)=\frac{A^0}{0!}$$
35	33 34	ax-mp	$$⊢F\left(0\right)=\frac{A^0}{0!}$$
36		fac0	$$⊢0!=1$$
37	36	oveq2i	$$⊢\frac{1}{0!}=\frac{1}{1}$$
38		1div1e1	$$⊢\frac{1}{1}=1$$
39	37 38	eqtr2i	$$⊢1=\frac{1}{0!}$$
40	32 35 39	3eqtr4g	$$⊢A=0\to F\left(0\right)=1$$
41	28 40	sylan9eqr	$$⊢\left(A=0\wedge k=0\right)\to F\left(k\right)=1$$
42		simpr	$$⊢\left(A=0\wedge k=0\right)\to k=0$$
43	42 22	sylibr	$$⊢\left(A=0\wedge k=0\right)\to k\in \left\{0\right\}$$
44	43	iftrued	$$⊢\left(A=0\wedge k=0\right)\to if\left(k\in \left\{0\right\},1,0\right)=1$$
45	41 44	eqtr4d	$$⊢\left(A=0\wedge k=0\right)\to F\left(k\right)=if\left(k\in \left\{0\right\},1,0\right)$$
46	27 45	jaodan	$$⊢\left(A=0\wedge \left(k\in \mathbb{N}\vee k=0\right)\right)\to F\left(k\right)=if\left(k\in \left\{0\right\},1,0\right)$$
47	6 46	syldan	$$⊢\left(A=0\wedge k\in {\mathbb{Z}}_{\ge 0}\right)\to F\left(k\right)=if\left(k\in \left\{0\right\},1,0\right)$$
48	33 3	eleqtri	$$⊢0\in {\mathbb{Z}}_{\ge 0}$$
49	48	a1i	$$⊢A=0\to 0\in {\mathbb{Z}}_{\ge 0}$$
50		1cnd	$$⊢\left(A=0\wedge k\in \left\{0\right\}\right)\to 1\in ℂ$$
51		fz0sn	$$⊢\left(0\dots 0\right)=\left\{0\right\}$$
52	51	eqimss2i	$$⊢\left\{0\right\}\subseteq \left(0\dots 0\right)$$
53	52	a1i	$$⊢A=0\to \left\{0\right\}\subseteq \left(0\dots 0\right)$$
54	47 49 50 53	fsumcvg2	$$⊢A=0\to seq0\left(+,F\right)⇝seq0\left(+,F\right)\left(0\right)$$
55		0z	$$⊢0\in \mathbb{Z}$$
56	55 40	seq1i	$$⊢A=0\to seq0\left(+,F\right)\left(0\right)=1$$
57	54 56	breqtrd	$$⊢A=0\to seq0\left(+,F\right)⇝1$$