Theorem expfac

Description: Factorial grows faster than exponential. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypothesis	expfac.f	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)$$
Assertion	expfac	$$⊢A\in ℂ\to F⇝0$$

Proof

Step	Hyp	Ref	Expression
1		expfac.f	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)$$
2		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
3		0zd	$$⊢A\in ℂ\to 0\in \mathbb{Z}$$
4		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
5	4	mptex	$$⊢\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\in \mathrm{V}$$
6	1 5	eqeltri	$$⊢F\in \mathrm{V}$$
7	6	a1i	$$⊢A\in ℂ\to F\in \mathrm{V}$$
8	1	efcllem	$$⊢A\in ℂ\to seq0\left(+,F\right)\in \mathrm{dom}⇝$$
9		oveq2	$$⊢n=m\to A^n=A^m$$
10		fveq2	$$⊢n=m\to n!=m!$$
11	9 10	oveq12d	$$⊢n=m\to \frac{A^n}{n!}=\frac{A^m}{m!}$$
12		simpr	$$⊢\left(A\in ℂ\wedge m\in {\mathbb{N}}_0\right)\to m\in {\mathbb{N}}_0$$
13		eftcl	$$⊢\left(A\in ℂ\wedge m\in {\mathbb{N}}_0\right)\to \frac{A^m}{m!}\in ℂ$$
14	1 11 12 13	fvmptd3	$$⊢\left(A\in ℂ\wedge m\in {\mathbb{N}}_0\right)\to F\left(m\right)=\frac{A^m}{m!}$$
15	14 13	eqeltrd	$$⊢\left(A\in ℂ\wedge m\in {\mathbb{N}}_0\right)\to F\left(m\right)\in ℂ$$
16	2 3 7 8 15	serf0	$$⊢A\in ℂ\to F⇝0$$