TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

$(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$

Statement

Let $n, k \in N$ with $k \leq n$ . Then, in $N$ ,

$(\binom{n}{k}) \cdot k! \cdot (n - k)! = n!,$

and consequently:

$(\binom{n}{k}) \cdot k! = n^{\underline{k}}$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ );
integrality: in $R$ , $ι (\binom{n}{k}) = \frac{ι (n!)}{ι (k!) ι ((n - k)!)}$ , so the familiar quotient $n! / (k! (n - k)!)$ is the canonical natural of a natural number, namely of the count $(\binom{n}{k})$ ;
symmetry: $(\binom{n}{k}) = (\binom{n}{n - k})$ .

Here $ι$ is the canonical natural of The canonical natural $ι (n) = n \cdot 1_{F}$ of a field and $n - k$ the truncated difference, which for $k \leq n$ is the ordinary one.

Facts & Assumptions

Given: Naturals $n, k$ with $k \leq n$ ; the initial segment $k = {i : i < k}$ , which satisfies $k \subseteq n$ ; and $Bij (X, Y)$ for the set of bijections $X \to Y$ .

[L1]

$(\binom{m}{j}) = ∣ [X]^{j} ∣$ for every finite $X$ with $∣ X ∣ = m$ ; $[X]^{j}$ is finite (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ).

[L2]

$∣ Bij (X, Y) ∣ = m!$ when $∣ X ∣ = ∣ Y ∣ = m$ , and such a set is finite (A finite set $A$ with $∣ A ∣ = n$ has exactly $n!$ bijections onto itself, and $n!$ bijections onto any set of the same cardinality).

[L3]

The sum rule (The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition) and $\sum_{i \in S} c = ∣ S ∣ \cdot c$ (The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form).

[L4]

The product rule $∣ X \times Y ∣ = ∣ X ∣ ∣ Y ∣$ (The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ ).

[L5]

Factorials (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ): $m! \neq 0$ for every $m$ ; $n^{\underline{k}} (n - k)! = n!$ for $k \leq n$ .

[L6]

Cardinality and subsets (The cardinality $∣ A ∣$ of a finite set, A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ ): transport along a bijection; $∣ m ∣ = m$ ; a subset of a finite set is finite.

[L7]

Arithmetic of $N$ : multiplication is associative and commutative, and $x \cdot c = y \cdot c$ with $c \neq 0$ gives $x = y$ (Multiplication is associative, Multiplication is commutative, Cancellation for multiplication by a nonzero factor); $k + t = n$ determines $t = n - k$ (Order on the natural numbers, Addition is cancellative).

[L8]

The embedding $ι$ is multiplicative and injective, and $ι (m) \neq 0$ for $m \neq 0$ (clauses 0 and 7 of Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ , The canonical natural $ι (n) = n \cdot 1_{F}$ of a field); a nonzero element of a field has a unique inverse, so division by it is legitimate (Identities and inverses in a field are unique, Field).

[L9]

Maps (Injection, surjection, bijection, Equinumerous sets, $A \approx B$ and $A ⪯ B$ ): a map with a two-sided inverse is a bijection; a bijection of $n$ carries a subset onto a subset and the complement onto the complement.

Proof

technique · direct

1.1

The set to be counted twice is $Bij (n)$ , of cardinality $n!$ by [L2]. For $S \in [n]^{k}$ put ${Bij}_{S} : = {f \in Bij (n) : f [k] = S}$ . These sets are pairwise disjoint, since $f$ determines $f [k]$ , and their union over $S \in [n]^{k}$ is all of $Bij (n)$ , because $f [k]$ is a subset of $n$ of cardinality $k$ for every bijection $f$ of $n$ .

L1L2L6L9construct

1.2

For any $X \subseteq n$ with $∣ X ∣ = k$ one has $∣ n ∖ X ∣ = n - k$ : the sets $X$ and $n ∖ X$ are disjoint with union $n$ , so $n = k + ∣ n ∖ X ∣$ by [L3], and [L7] identifies the second summand as $n - k$ .

L3L6L7

2.1

$∣ {Bij}_{S} ∣ = k! (n - k)!$ for every $S \in [n]^{k}$ . Indeed $f \mapsto (f ↾ k, f ↾ (n ∖ k))$ maps ${Bij}_{S}$ to $Bij (k, S) \times Bij (n ∖ k, n ∖ S)$ : if $f [k] = S$ then $f$ restricted to $k$ is a bijection onto $S$ , and, $f$ being a bijection of $n$ , it carries $n ∖ k$ onto $n ∖ S$ . The map $(u, v) \mapsto u \cup v$ is a two-sided inverse, the union of the two functions being a function on $k \cup (n ∖ k) = n$ and a bijection onto $S \cup (n ∖ S) = n$ . Since $∣ k ∣ = ∣ S ∣ = k$ and $∣ n ∖ k ∣ = ∣ n ∖ S ∣ = n - k$ by step 1.2, [L2] and [L4] give the cardinality $k! (n - k)!$ .

step 1.1step 1.2L2L4L6L9

2.2

Symmetry. The map $S \mapsto n ∖ S$ sends $[n]^{k}$ into $[n]^{n - k}$ by step 1.2, and $T \mapsto n ∖ T$ sends $[n]^{n - k}$ into $[n]^{k}$ , again by step 1.2 together with $n - (n - k) = k$ , which holds because $(n - k) + k = n$ . The two are mutually inverse, since $n ∖ (n ∖ S) = S$ for $S \subseteq n$ . Hence $(\binom{n}{k}) = (\binom{n}{n - k})$ .

step 1.2L1L6L7L9construct

3.1

Counting $Bij (n)$ by the blocks of step 1.1 and using [L3], $n! = ∣ Bij (n) ∣ = \sum_{S \in [n]^{k}} ∣ {Bij}_{S} ∣ = \sum_{S \in [n]^{k}} k! (n - k)! = ∣ [n]^{k} ∣ \cdot k! (n - k)! = (\binom{n}{k}) k! (n - k)!$ , the summand being constant.

step 1.1step 2.1L1L3

4.1

Clause 1. By [L5], $n^{\underline{k}} (n - k)! = n!$ , so $((\binom{n}{k}) k!) (n - k)! = n^{\underline{k}} (n - k)!$ by step 3.1 and associativity; since $(n - k)! \neq 0$ , cancellation gives $(\binom{n}{k}) k! = n^{\underline{k}}$ .

step 3.1L5L7

4.2

Clause 2. Applying $ι$ to step 3.1 and using multiplicativity, $ι (n!) = ι (\binom{n}{k}) ι (k!) ι ((n - k)!)$ . Both $ι (k!)$ and $ι ((n - k)!)$ are nonzero by [L5] and [L8], so their product is invertible in $R$ and $ι (\binom{n}{k}) = ι (n!) / (ι (k!) ι ((n - k)!))$ . The left-hand side is the canonical natural of the count $(\binom{n}{k})$ , which is what the word integrality means here.

step 3.1L5L8

5.1

The displayed identity is step 3.1, clause 1 is step 4.1, clause 2 is step 4.2 and clause 3 is step 2.2.

step 2.2step 3.1step 4.1step 4.2∎

Remarks

Why the symmetry is proved by a bijection. Complementation is shorter than manipulating the closed formula, it needs no hypothesis beyond $k \leq n$ , and it is the argument that survives to the multinomial coefficient, where no single closed formula is available until the analogous count has been made.
Where $k \leq n$ is used. In step 1.1, so that $k$ is a subset of $n$ of cardinality $k$ and $[n]^{k}$ is nonempty; and in step 1.2, so that $n - k$ is a genuine difference. For $k > n$ both sides of the displayed identity are still defined, but the left-hand side is $0$ while $n!$ is not, so the hypothesis is not removable.
The quotient formula is a theorem about a natural number. A reader who starts from $n! / (k! (n - k)!)$ has to prove that the division comes out exact. Starting from the count, the exactness is what step 3.1 says, and the quotient is a consequence.

Depends on

Used by

…and 7 more results.

Dependency tree · two levels

50 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Binomial coefficient (Wikipedia) (standard reference, not scraped)
Double counting (proof technique) (Wikipedia) (standard reference, not scraped)
R. Stanley, Enumerative Combinatorics, Vol. 1, Ch. 1 (standard reference, not scraped)

(nk) k! (n−k)!=n!(kn​)k!(n−k)!=n! for k≤nk≤n; hence (nk) k!=nk‾(kn​)k!=nk​, the quotient n!/(k!(n−k)!)n!/(k!(n−k)!) is a natural number, and (nk)=(nn−k)(kn​)=(n−kn​)