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

Metamath Proof Explorer

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 )