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

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 \in ℂ \to \frac{A^{0}}{0!} = 1$

Proof

Step	Hyp	Ref	Expression
1		exp0	$⊢ A \in ℂ \to A^{0} = 1$
2	1	oveq1d	$⊢ A \in ℂ \to \frac{A^{0}}{0!} = \frac{1}{0!}$
3		fac0	$⊢ 0! = 1$
4	3	oveq2i	$⊢ \frac{1}{0!} = \frac{1}{1}$
5		1div1e1	$⊢ \frac{1}{1} = 1$
6	4 5	eqtri	$⊢ \frac{1}{0!} = 1$
7	2 6	eqtrdi	$⊢ A \in ℂ \to \frac{A^{0}}{0!} = 1$