Theorem fallfaccl

Description: Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018)

	Ref	Expression
Assertion	fallfaccl	|- ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac N ) e. CC )

Proof

Step	Hyp	Ref	Expression
1		ssid	|- CC C_ CC
2		ax-1cn	|- 1 e. CC
3		mulcl	|- ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
4		nn0cn	|- ( k e. NN0 -> k e. CC )
5		subcl	|- ( ( A e. CC /\ k e. CC ) -> ( A - k ) e. CC )
6	4 5	sylan2	|- ( ( A e. CC /\ k e. NN0 ) -> ( A - k ) e. CC )
7	1 2 3 6	fallfaccllem	|- ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac N ) e. CC )