Theorem risefaccl

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

	Ref	Expression
Assertion	risefaccl	|- ( ( A e. CC /\ N e. NN0 ) -> ( A RiseFac 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		addcl	|- ( ( 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	risefaccllem	|- ( ( A e. CC /\ N e. NN0 ) -> ( A RiseFac N ) e. CC )