Theorem ef0

Description: Value of the exponential function at 0. Equation 2 of Gleason p. 308. (Contributed by Steve Rodriguez, 27-Jun-2006) (Revised by Mario Carneiro, 28-Apr-2014)

	Ref	Expression
Assertion	ef0	$$⊢{\mathrm{e}}^0=1$$

Proof

Step	Hyp	Ref	Expression
1		0cn	$$⊢0\in ℂ$$
2		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼\frac{0^n}{n!}\right)=\left(n\in {\mathbb{N}}_0⟼\frac{0^n}{n!}\right)$$
3	2	efcvg	$$⊢0\in ℂ\to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{0^n}{n!}\right)\right)⇝{\mathrm{e}}^0$$
4	1 3	ax-mp	$$⊢seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{0^n}{n!}\right)\right)⇝{\mathrm{e}}^0$$
5		eqid	$$⊢0=0$$
6	2	ef0lem	$$⊢0=0\to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{0^n}{n!}\right)\right)⇝1$$
7	5 6	ax-mp	$$⊢seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{0^n}{n!}\right)\right)⇝1$$
8		climuni	$$⊢\left(seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{0^n}{n!}\right)\right)⇝{\mathrm{e}}^0\wedge seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{0^n}{n!}\right)\right)⇝1\right)\to {\mathrm{e}}^0=1$$
9	4 7 8	mp2an	$$⊢{\mathrm{e}}^0=1$$