expfac

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

		Ref	Expression
	Hypothesis	expfac.f	$⊢ F = (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})$
	Assertion	expfac	$⊢ A \in ℂ \to F ⇝ 0$

Step	Hyp	Ref	Expression
1		expfac.f	$⊢ F = (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})$
2		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
3		0zd	$⊢ A \in ℂ \to 0 \in ℤ$
4		nn0ex	$⊢ ℕ_{0} \in V$
5	4	mptex	$⊢ (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!}) \in V$
6	1 5	eqeltri	$⊢ F \in V$
7	6	a1i	$⊢ A \in ℂ \to F \in V$
8	1	efcllem	$⊢ A \in ℂ \to seq 0 (+ F) \in 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	$⊢ (A \in ℂ \land m \in ℕ_{0}) \to m \in ℕ_{0}$
13		eftcl	$⊢ (A \in ℂ \land m \in ℕ_{0}) \to \frac{A^{m}}{m!} \in ℂ$
14	1 11 12 13	fvmptd3	$⊢ (A \in ℂ \land m \in ℕ_{0}) \to F (m) = \frac{A^{m}}{m!}$
15	14 13	eqeltrd	$⊢ (A \in ℂ \land m \in ℕ_{0}) \to F (m) \in ℂ$
16	2 3 7 8 15	serf0	$⊢ A \in ℂ \to F ⇝ 0$

Metamath Proof Explorer