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	⊢ ( exp ‘ 0 ) = 1

Proof

Step	Hyp	Ref	Expression
1		0cn	⊢ 0 ∈ ℂ
2		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 0 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 0 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
3	2	efcvg	⊢ ( 0 ∈ ℂ → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 0 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ⇝ ( exp ‘ 0 ) )
4	1 3	ax-mp	⊢ seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 0 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ⇝ ( exp ‘ 0 )
5		eqid	⊢ 0 = 0
6	2	ef0lem	⊢ ( 0 = 0 → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 0 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ⇝ 1 )
7	5 6	ax-mp	⊢ seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 0 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ⇝ 1
8		climuni	⊢ ( ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 0 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ⇝ ( exp ‘ 0 ) ∧ seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 0 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ⇝ 1 ) → ( exp ‘ 0 ) = 1 )
9	4 7 8	mp2an	⊢ ( exp ‘ 0 ) = 1