This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Elementary trigonometry The exponential, sine, and cosine functions 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 ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 0 ) / ( ! ‘ 0 ) ) = 1 )
Proof
Step
Hyp
Ref
Expression
1
exp0 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 )
2
1
oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 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 ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 0 ) / ( ! ‘ 0 ) ) = 1 )