Definition·D032
Factorial
The product of all numbers from one up to n.
for
; by the recursion theorem these equations determine a unique function
from
to
.
In words
The factorial of zero is one, and the factorial of the successor of n is the factorial of n times that successor.
Rests onno axioms yet
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Remarks
This is T07 with start value
and step rule
, a function on
built from multiplication and the successor by Separation; the parameter
in the step rule is exactly the feature the parameterized recursion theorem provides. Values:
The factorial's role here is strategic:
is divisible by every number from
to
(L21), which makes
divisible by none of
(the divisor
is unavoidable, since it divides everything), the engine of Euclid's theorem.