Metamath Proof Explorer


Theorem eft0val

Description: The value of the first term of the series expansion of the exponential function is 1. (Contributed by Paul Chapman, 21-Aug-2007) (Revised by Mario Carneiro, 29-Apr-2014)

Ref Expression
Assertion eft0val
|- ( A e. CC -> ( ( A ^ 0 ) / ( ! ` 0 ) ) = 1 )

Proof

Step Hyp Ref Expression
1 exp0
 |-  ( A e. CC -> ( A ^ 0 ) = 1 )
2 1 oveq1d
 |-  ( A e. CC -> ( ( A ^ 0 ) / ( ! ` 0 ) ) = ( 1 / ( ! ` 0 ) ) )
3 fac0
 |-  ( ! ` 0 ) = 1
4 3 oveq2i
 |-  ( 1 / ( ! ` 0 ) ) = ( 1 / 1 )
5 1div1e1
 |-  ( 1 / 1 ) = 1
6 4 5 eqtri
 |-  ( 1 / ( ! ` 0 ) ) = 1
7 2 6 eqtrdi
 |-  ( A e. CC -> ( ( A ^ 0 ) / ( ! ` 0 ) ) = 1 )