Description: Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | rerisefaccl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-resscn | ||
2 | 1re | ||
3 | remulcl | ||
4 | nn0re | ||
5 | readdcl | ||
6 | 4 5 | sylan2 | |
7 | 1 2 3 6 | risefaccllem |