TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)

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.

$ι (D_{n}) = ι (n!) \sum_{i < n + 1} (- 1)^{i} / ι (i!)$ , with the term at $i = 0$ equal to $1$ and $D_{0} = 1$

Statement

For every $n \in N$ , in $R$ ,

$ι (D_{n}) = ι (n!) \sum_{i < n + 1} \frac{(- 1)^{i}}{ι (i!)},$

where $D_{n}$ is the derangement number (The derangement number $D_{n}$ : the number of bijections of an $n$ -element set with no fixed point), $n!$ the factorial (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ) and $ι$ the canonical natural (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field). Each division is legitimate because $i! \neq 0$ , hence $ι (i!) \neq 0$ .

The index runs from $0$ , and the term at $i = 0$ is $(- 1)^{0} / ι (0!) = 1$ . At $n = 0$ the identity reads $ι (D_{0}) = ι (0!) \cdot 1 = 1$ , which agrees with $D_{0} = 1$ ; at $n = 1$ it reads $ι (D_{1}) = 1 \cdot (1 - 1) = 0$ ; and at $n = 2$ it reads $ι (D_{2}) = 2 \cdot (1 - 1 + 1 / 2) = 1$ .

Since $ι$ is injective, the identity determines $D_{n}$ as a natural number (Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ , clause 7).

Facts & Assumptions

Given: A natural number $n$ , the set $X : = Bij (n)$ of bijections of $n$ onto itself, and, for $a \in n$ , the set $A_{a} : = {f \in X : f (a) = a}$ of bijections fixing $a$ .

[L1]

$Bij (S)$ is finite with $∣ Bij (S) ∣ = ∣ S ∣!$ for every finite $S$ (A finite set $A$ with $∣ A ∣ = n$ has exactly $n!$ bijections onto itself, and $n!$ bijections onto any set of the same cardinality, The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ); in particular $∣ X ∣ = n!$ and $∣ n ∣ = n$ (The cardinality $∣ A ∣$ of a finite set).

[L2]

$(A_{a})_{a \in n}$ is a family of subsets of the finite set $X$ indexed by the finite set $n$ , hence a sieve family with ambient set $X$ , and $A_{\emptyset} = X$ (A finite family $(A_{i})_{i \in I}$ of subsets of a finite set $X$ , the intersections $A_{J}$ for $J \subseteq I$ , and the convention $A_{\emptyset} = X$ , A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ ).

[L3]

$Der (n) = X ∖ ⋃_{a \in n} A_{a}$ , since a bijection of $n$ is a derangement exactly when it fixes no point (The derangement number $D_{n}$ : the number of bijections of an $n$ -element set with no fixed point, Injection, surjection, bijection).

[L4]

For a finite sieve family $(A_{a})_{a \in n}$ in $X$ with $A_{\emptyset} = X$ , the complementary identity is $ι ∣ X ∖ ⋃_{a \in n} A_{a} ∣ = \sum_{J \in P (n)} (- 1)^{∣ J ∣} ι ∣ A_{J} ∣$ (Inclusion and exclusion: $ι ∣ ⋃_{i \in I} A_{i} ∣ = \sum_{\emptyset \neq J \subseteq I} (- 1)^{∣ J ∣ + 1} ι ∣ A_{J} ∣$ , together with the complementary form counting the elements in none of the $A_{i}$ , clause 2).

[L5]

Partition of a power set by cardinality: the sets $[n]^{i}$ for $i \in σ (n)$ are pairwise disjoint with union $P (n)$ , and $∣ [n]^{i} ∣ = (\binom{n}{i})$ (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , clause 2, The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ , $∣ P (A) ∣ = 2^{∣ A ∣}$ for finite $A$ ).

[L6]

Splitting a sum along a partition of its index set (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, clause 3); a constant real summand and the bridge $\sum_{i \in n} u_{i} = \sum_{i < n} u_{i}$ (The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form, clauses (a) and (c)); and scaling of a real finite sum (Laws of finite sums and finite products, clause 2, Finite sums and finite products, by recursion).

[L7]

For $J \subseteq n$ : $∣ J ∣ + ∣ n ∖ J ∣ = n$ , so $∣ n ∖ J ∣ = n - ∣ J ∣$ with the truncated difference (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, clause 1, Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ ).

[L8]

Integrality of the binomial coefficient: for $i \leq n$ , $ι (\binom{n}{i}) = ι (n!) / (ι (i!) ι ((n - i)!))$ ( $(\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})$ , clause 2); and $m! \neq 0$ for every $m$ , so $ι (m!) \neq 0$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ , clause (b), Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ , clause 7).

[L9]

$R$ is an ordered field, so division by a nonzero element is available (Ordered field, Field); and $(- 1)^{0} = 1$ (Integer powers $a^{m}$ ).

Proof

technique · direct

1.1

The ambient set and the sieve family. $X = Bij (n)$ is finite with $∣ X ∣ = n!$ by [L1], the sets $A_{a}$ for $a \in n$ are subsets of $X$ , and $Der (n)$ is the complement in $X$ of their union by [L3].

L1L2L3construct

1.2

The intersections are bijection sets of a smaller set. For $J \subseteq n$ the map $f \mapsto f ⁣ ↾ ⁣ (n ∖ J)$ is a bijection of $A_{J}$ onto $Bij (n ∖ J)$ . Indeed a bijection $f$ of $n$ fixing every point of $J$ has $f [J] = J$ , hence $f [n ∖ J] = n ∖ J$ by injectivity, so its restriction is a bijection of $n ∖ J$ ; conversely a bijection $g$ of $n ∖ J$ extends by the identity on $J$ to a bijection of $n$ fixing every point of $J$ , and the two constructions are mutually inverse. For $J = \emptyset$ both sides are $X$ , by the stipulation of [L2].

L1L2L3construct

1.3

Hence $∣ A_{J} ∣ = ∣ n ∖ J ∣! = (n - ∣ J ∣)!$ for every $J \subseteq n$ , by [L1] applied to $n ∖ J$ and by [L7].

L1L7

2.1

The sieve. Applying [L4] to the family of step 1.1 and substituting step 1.3, $ι (D_{n}) = ι ∣ Der (n) ∣ = \sum_{J \in P (n)} (- 1)^{∣ J ∣} ι ((n - ∣ J ∣)!)$ .

step 1.1step 1.2step 1.3L4

3.1

Grouping the subsets of $n$ by size. Splitting along the partition of [L5] and using the constant clause of [L6] on each block, where the summand depends on $J$ only through $∣ J ∣ = i$ , gives $ι (D_{n}) = \sum_{i < n + 1} ι (\binom{n}{i}) (- 1)^{i} ι ((n - i)!)$ .

step 2.1L5L6

4.1

Each coefficient collapses. For $i < n + 1$ , that is $i \leq n$ , [L8] gives $ι (\binom{n}{i}) ι ((n - i)!) = ι (n!) / ι (i!)$ , so the $i$ -th summand of step 3.1 is $(- 1)^{i} ι (n!) / ι (i!)$ ; scaling the sum by the constant $ι (n!)$ through [L6] gives $ι (D_{n}) = ι (n!) \sum_{i < n + 1} (- 1)^{i} / ι (i!)$ .

step 3.1L6L8L9∎

Remarks

Where the closed formula for the binomial coefficient is spent. Only in the last step, and only in the range $i \leq n$ , which is exactly the range the sum runs over. Outside that range the identity of $(\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})$ is not asserted, and it is not used.
Why the identity is stated in $R$ . It contains both a subtraction, through the alternating sign, and a division by $i!$ . Neither operation exists in $N$ , so the count is carried across by $ι$ ; injectivity of $ι$ is what carries the conclusion back.
The first index is $0$ and it matters. The term at $i = 0$ is $1$ , and the identity at $n = 0$ is the statement $D_{0} = 1$ , which is where the empty function enters. A version of this formula whose sum began at $i = 1$ would be false at every $n$ .

Depends on

Used by

Dependency tree · two levels

69 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

Derangement (Wikipedia) (standard reference, not scraped)
Inclusion-exclusion principle (Wikipedia) (standard reference, not scraped)
Rencontres numbers (Wikipedia) (standard reference, not scraped)
Derangements (OpenText at the University of Lethbridge) (standard reference, not scraped)

ι(Dn)=ι(n!)∑i<n+1(−1)i/ι(i!)ι(Dn​)=ι(n!)∑i<n+1​(−1)i/ι(i!), with the term at i=0i=0 equal to 11 and D0=1D0​=1