Description: Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | zfallfaccl | |- ( ( A e. ZZ /\ N e. NN0 ) -> ( A FallFac 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 | zsubcl | |- ( ( 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 | fallfaccllem | |- ( ( A e. ZZ /\ N e. NN0 ) -> ( A FallFac N ) e. ZZ ) |