Theorem expfac

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

	Ref	Expression
Hypothesis	expfac.f	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
Assertion	expfac	⊢ ( 𝐴 ∈ ℂ → 𝐹 ⇝ 0 )

Proof

Step	Hyp	Ref	Expression
1		expfac.f	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
2		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
3		0zd	⊢ ( 𝐴 ∈ ℂ → 0 ∈ ℤ )
4		nn0ex	⊢ ℕ0 ∈ V
5	4	mptex	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ∈ V
6	1 5	eqeltri	⊢ 𝐹 ∈ V
7	6	a1i	⊢ ( 𝐴 ∈ ℂ → 𝐹 ∈ V )
8	1	efcllem	⊢ ( 𝐴 ∈ ℂ → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
9		oveq2	⊢ ( 𝑛 = 𝑚 → ( 𝐴 ↑ 𝑛 ) = ( 𝐴 ↑ 𝑚 ) )
10		fveq2	⊢ ( 𝑛 = 𝑚 → ( ! ‘ 𝑛 ) = ( ! ‘ 𝑚 ) )
11	9 10	oveq12d	⊢ ( 𝑛 = 𝑚 → ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) = ( ( 𝐴 ↑ 𝑚 ) / ( ! ‘ 𝑚 ) ) )
12		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℕ0 )
13		eftcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑚 ) / ( ! ‘ 𝑚 ) ) ∈ ℂ )
14	1 11 12 13	fvmptd3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑚 ) = ( ( 𝐴 ↑ 𝑚 ) / ( ! ‘ 𝑚 ) ) )
15	14 13	eqeltrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ )
16	2 3 7 8 15	serf0	⊢ ( 𝐴 ∈ ℂ → 𝐹 ⇝ 0 )