Theorem esum

Description: Value of Euler's constant _e = 2.71828.... (Contributed by Steve Rodriguez, 5-Mar-2006)

	Ref	Expression
Assertion	esum	$$⊢\mathrm{e}=\sum _{k\in {\mathbb{N}}_0}\left(\frac{1}{k!}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-e	$$⊢\mathrm{e}={\mathrm{e}}^1$$
2		ax-1cn	$$⊢1\in ℂ$$
3		efval	$$⊢1\in ℂ\to {\mathrm{e}}^1=\sum _{k\in {\mathbb{N}}_0}\left(\frac{1^k}{k!}\right)$$
4	2 3	ax-mp	$$⊢{\mathrm{e}}^1=\sum _{k\in {\mathbb{N}}_0}\left(\frac{1^k}{k!}\right)$$
5		nn0z	$$⊢k\in {\mathbb{N}}_0\to k\in \mathbb{Z}$$
6		1exp	$$⊢k\in \mathbb{Z}\to 1^k=1$$
7	5 6	syl	$$⊢k\in {\mathbb{N}}_0\to 1^k=1$$
8	7	oveq1d	$$⊢k\in {\mathbb{N}}_0\to \frac{1^k}{k!}=\frac{1}{k!}$$
9	8	sumeq2i	$$⊢\sum _{k\in {\mathbb{N}}_0}\left(\frac{1^k}{k!}\right)=\sum _{k\in {\mathbb{N}}_0}\left(\frac{1}{k!}\right)$$
10	1 4 9	3eqtri	$$⊢\mathrm{e}=\sum _{k\in {\mathbb{N}}_0}\left(\frac{1}{k!}\right)$$