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 ) |
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 ) |