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 e. CC
2 eqid 
 |-  ( n e. NN0 |-> ( ( 0 ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( 0 ^ n ) / ( ! ` n ) ) )
3 2 efcvg 
 |-  ( 0 e. CC -> seq 0 ( + , ( n e. NN0 |-> ( ( 0 ^ n ) / ( ! ` n ) ) ) ) ~~> ( exp ` 0 ) )
4 1 3 ax-mp 
 |-  seq 0 ( + , ( n e. NN0 |-> ( ( 0 ^ n ) / ( ! ` n ) ) ) ) ~~> ( exp ` 0 )
5 eqid 
 |-  0 = 0
6 2 ef0lem 
 |-  ( 0 = 0 -> seq 0 ( + , ( n e. NN0 |-> ( ( 0 ^ n ) / ( ! ` n ) ) ) ) ~~> 1 )
7 5 6 ax-mp 
 |-  seq 0 ( + , ( n e. NN0 |-> ( ( 0 ^ n ) / ( ! ` n ) ) ) ) ~~> 1
8 climuni 
 |-  ( ( seq 0 ( + , ( n e. NN0 |-> ( ( 0 ^ n ) / ( ! ` n ) ) ) ) ~~> ( exp ` 0 ) /\ seq 0 ( + , ( n e. NN0 |-> ( ( 0 ^ n ) / ( ! ` n ) ) ) ) ~~> 1 ) -> ( exp ` 0 ) = 1 )
9 4 7 8 mp2an 
 |-  ( exp ` 0 ) = 1