Description: Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | zrisefaccl | |- ( ( A e. ZZ /\ N e. NN0 ) -> ( A RiseFac N ) e. ZZ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zsscn | |- ZZ C_ CC |
|
2 | 1z | |- 1 e. ZZ |
|
3 | zmulcl | |- ( ( x e. ZZ /\ y e. ZZ ) -> ( x x. y ) e. ZZ ) |
|
4 | nn0z | |- ( k e. NN0 -> k e. ZZ ) |
|
5 | zaddcl | |- ( ( A e. ZZ /\ k e. ZZ ) -> ( A + k ) e. ZZ ) |
|
6 | 4 5 | sylan2 | |- ( ( A e. ZZ /\ k e. NN0 ) -> ( A + k ) e. ZZ ) |
7 | 1 2 3 6 | risefaccllem | |- ( ( A e. ZZ /\ N e. NN0 ) -> ( A RiseFac N ) e. ZZ ) |