Theorem esum

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

	Ref	Expression
Assertion	esum	|- _e = sum_ k e. NN0 ( 1 / ( ! ` k ) )

Proof

Step	Hyp	Ref	Expression
1		df-e	|- _e = ( exp ` 1 )
2		ax-1cn	|- 1 e. CC
3		efval	|- ( 1 e. CC -> ( exp ` 1 ) = sum_ k e. NN0 ( ( 1 ^ k ) / ( ! ` k ) ) )
4	2 3	ax-mp	|- ( exp ` 1 ) = sum_ k e. NN0 ( ( 1 ^ k ) / ( ! ` k ) )
5		nn0z	|- ( k e. NN0 -> k e. ZZ )
6		1exp	|- ( k e. ZZ -> ( 1 ^ k ) = 1 )
7	5 6	syl	|- ( k e. NN0 -> ( 1 ^ k ) = 1 )
8	7	oveq1d	|- ( k e. NN0 -> ( ( 1 ^ k ) / ( ! ` k ) ) = ( 1 / ( ! ` k ) ) )
9	8	sumeq2i	|- sum_ k e. NN0 ( ( 1 ^ k ) / ( ! ` k ) ) = sum_ k e. NN0 ( 1 / ( ! ` k ) )
10	1 4 9	3eqtri	|- _e = sum_ k e. NN0 ( 1 / ( ! ` k ) )