Skip to content
Axiomatic Wiki
Lemma·L21

Factorials are positive and richly divisible

n! is never zero, and every number up to n divides it.

For all : (i) ; (ii) , with from D032, from D030, and the order from D029.
In words
Every factorial is positive, and the factorial of n is divisible by each number from one up to n.
Rests onF02F03F04F06F08F09F11F12F14A01A06A08
Never needed: F05 · F10 · F13 · A02 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    (i) By induction on (T05, Separation). Base: and (L15 (vi) at ). Step: assume , so (irreflexivity, L15 (i)). Also by (P3). Then by L18 (i), and with gives (L15 (iv), D029).
  2. 2
    (ii) By induction on , with quantified inside: . Base: there is no with : forces (as , i.e. , is impossible by D002 and D029), and then gives or , the first impossible again, the second contradicting (P3). So vacuously.
  3. 3
    Step: let and . By L15 (iii), splits as or .
  4. 4
    If : the hypothesis gives . Also , since (D032) exhibits the witness (D030). Transitivity (L19 (iv)) gives .
  5. 5
    If : then by commutativity, so with witness . Either way , and T05 finishes.
∎

Remarks

Both halves feed directly into Euclid's theorem: positivity makes at least , so it has a prime divisor at all, and the divisibility clause is what expels that prime beyond . The pattern of (ii), "a product is divisible by each of its factors", is the elementary core of the fundamental theorem of arithmetic.
Wikipedia ↗Nat.dvd_factorial ↗

Used by

T11
Propose an edit1 published revision