Description: Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | fallfaccl | โข ( ( ๐ด โ โ โง ๐ โ โ0 ) โ ( ๐ด FallFac ๐ ) โ โ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid | โข โ โ โ | |
2 | ax-1cn | โข 1 โ โ | |
3 | mulcl | โข ( ( ๐ฅ โ โ โง ๐ฆ โ โ ) โ ( ๐ฅ ยท ๐ฆ ) โ โ ) | |
4 | nn0cn | โข ( ๐ โ โ0 โ ๐ โ โ ) | |
5 | subcl | โข ( ( ๐ด โ โ โง ๐ โ โ ) โ ( ๐ด โ ๐ ) โ โ ) | |
6 | 4 5 | sylan2 | โข ( ( ๐ด โ โ โง ๐ โ โ0 ) โ ( ๐ด โ ๐ ) โ โ ) |
7 | 1 2 3 6 | fallfaccllem | โข ( ( ๐ด โ โ โง ๐ โ โ0 ) โ ( ๐ด FallFac ๐ ) โ โ ) |