# Metamath Proof Explorer

## 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 {ℕ}_{0}⟼\frac{{0}^{{n}}}{{n}!}\right)=\left({n}\in {ℕ}_{0}⟼\frac{{0}^{{n}}}{{n}!}\right)$
3 2 efcvg ${⊢}0\in ℂ\to seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{0}^{{n}}}{{n}!}\right)\right)⇝{\mathrm{e}}^{0}$
4 1 3 ax-mp ${⊢}seq0\left(+,\left({n}\in {ℕ}_{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 {ℕ}_{0}⟼\frac{{0}^{{n}}}{{n}!}\right)\right)⇝1$
7 5 6 ax-mp ${⊢}seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{0}^{{n}}}{{n}!}\right)\right)⇝1$
8 climuni ${⊢}\left(seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{0}^{{n}}}{{n}!}\right)\right)⇝{\mathrm{e}}^{0}\wedge seq0\left(+,\left({n}\in {ℕ}_{0}⟼\frac{{0}^{{n}}}{{n}!}\right)\right)⇝1\right)\to {\mathrm{e}}^{0}=1$
9 4 7 8 mp2an ${⊢}{\mathrm{e}}^{0}=1$