# Metamath Proof Explorer

## Theorem efcvg

Description: The series that defines the exponential function converges to it. (Contributed by NM, 9-Jan-2006) (Revised by Mario Carneiro, 28-Apr-2014)

Ref Expression
Hypothesis efcvg.1
`|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )`
Assertion efcvg
`|- ( A e. CC -> seq 0 ( + , F ) ~~> ( exp ` A ) )`

### Proof

Step Hyp Ref Expression
1 efcvg.1
` |-  F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )`
2 nn0uz
` |-  NN0 = ( ZZ>= ` 0 )`
3 0zd
` |-  ( A e. CC -> 0 e. ZZ )`
4 1 eftval
` |-  ( k e. NN0 -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )`
` |-  ( ( A e. CC /\ k e. NN0 ) -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )`
` |-  ( ( A e. CC /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) e. CC )`
` |-  ( A e. CC -> seq 0 ( + , F ) e. dom ~~> )`
` |-  ( A e. CC -> seq 0 ( + , F ) ~~> sum_ k e. NN0 ( ( A ^ k ) / ( ! ` k ) ) )`
` |-  ( A e. CC -> ( exp ` A ) = sum_ k e. NN0 ( ( A ^ k ) / ( ! ` k ) ) )`
` |-  ( A e. CC -> seq 0 ( + , F ) ~~> ( exp ` A ) )`