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$$