This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 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