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

Metamath Proof Explorer

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