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 )