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 
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
Assertion expfac 
|- ( A e. CC -> F ~~> 0 )

Proof

Step Hyp Ref Expression
1 expfac.f 
 |-  F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
2 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
3 0zd 
 |-  ( A e. CC -> 0 e. ZZ )
4 nn0ex 
 |-  NN0 e. _V
5 4 mptex 
 |-  ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) e. _V
6 1 5 eqeltri 
 |-  F e. _V
7 6 a1i 
 |-  ( A e. CC -> F e. _V )
8 1 efcllem 
 |-  ( A e. CC -> seq 0 ( + , F ) e. dom ~~> )
9 oveq2 
 |-  ( n = m -> ( A ^ n ) = ( A ^ m ) )
10 fveq2 
 |-  ( n = m -> ( ! ` n ) = ( ! ` m ) )
11 9 10 oveq12d 
 |-  ( n = m -> ( ( A ^ n ) / ( ! ` n ) ) = ( ( A ^ m ) / ( ! ` m ) ) )
12 simpr 
 |-  ( ( A e. CC /\ m e. NN0 ) -> m e. NN0 )
13 eftcl 
 |-  ( ( A e. CC /\ m e. NN0 ) -> ( ( A ^ m ) / ( ! ` m ) ) e. CC )
14 1 11 12 13 fvmptd3 
 |-  ( ( A e. CC /\ m e. NN0 ) -> ( F ` m ) = ( ( A ^ m ) / ( ! ` m ) ) )
15 14 13 eqeltrd 
 |-  ( ( A e. CC /\ m e. NN0 ) -> ( F ` m ) e. CC )
16 2 3 7 8 15 serf0 
 |-  ( A e. CC -> F ~~> 0 )