Theorem esum

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

	Ref	Expression
Assertion	esum	⊢ e = Σ 𝑘 ∈ ℕ0 ( 1 / ( ! ‘ 𝑘 ) )

Proof

Step	Hyp	Ref	Expression
1		df-e	⊢ e = ( exp ‘ 1 )
2		ax-1cn	⊢ 1 ∈ ℂ
3		efval	⊢ ( 1 ∈ ℂ → ( exp ‘ 1 ) = Σ 𝑘 ∈ ℕ0 ( ( 1 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
4	2 3	ax-mp	⊢ ( exp ‘ 1 ) = Σ 𝑘 ∈ ℕ0 ( ( 1 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) )
5		nn0z	⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℤ )
6		1exp	⊢ ( 𝑘 ∈ ℤ → ( 1 ↑ 𝑘 ) = 1 )
7	5 6	syl	⊢ ( 𝑘 ∈ ℕ0 → ( 1 ↑ 𝑘 ) = 1 )
8	7	oveq1d	⊢ ( 𝑘 ∈ ℕ0 → ( ( 1 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = ( 1 / ( ! ‘ 𝑘 ) ) )
9	8	sumeq2i	⊢ Σ 𝑘 ∈ ℕ0 ( ( 1 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = Σ 𝑘 ∈ ℕ0 ( 1 / ( ! ‘ 𝑘 ) )
10	1 4 9	3eqtri	⊢ e = Σ 𝑘 ∈ ℕ0 ( 1 / ( ! ‘ 𝑘 ) )