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.

The binomial theorem in $R$ : $(x + y)^{n} = \sum_{k < n + 1} ι ⁣ (\binom{n}{k}) x^{k} y^{n - k}$

Statement

For all $x, y \in R$ and every $n \in N$ ,

$(x + y)^{n} = \sum_{k < n + 1} ι (\binom{n}{k}) x^{k} y^{n - k},$

where the powers are the integer powers of Integer powers $a^{m}$ , the sum is the real finite sum of Finite sums and finite products, by recursion over $k = 0, 1, \dots, n$ , the difference $n - k$ is a genuine one because $k \leq n$ throughout the range, and $ι$ is the canonical natural of The canonical natural $ι (n) = n \cdot 1_{F}$ of a field.

The coefficient is $ι (\binom{n}{k})$ and not $(\binom{n}{k})$ . A binomial coefficient is a natural number, that is a von Neumann natural, that is a set; it is not an element of $R$ , and it enters the field through $ι$ .

The identity is stated in $R$ and only in $R$ . The same proof uses nothing but commutativity, associativity, distributivity and natural-number multiples of a ring element, so a commutative-ring version is available wherever rings are; rings are not available at this point in the reading order, and the ring statement is a separate statement, to be made where they are. See the Remarks below.

Facts & Assumptions

Given: Reals $x, y$ ; a natural $n$ ; and the abbreviation $c_{k} : = ι (\binom{n}{k})$ for every $k \in N$ , so that $c_{k} = ι (0) = 0$ whenever $k > n$ .

[L1]

Induction (The principle of mathematical induction).

[L2]

Integer powers (Integer powers $a^{m}$ ): $a^{0} = 1$ for every real $a$ , including $a = 0$ , and $a^{σ (m)} = a^{m} \cdot a$ . An immediate induction gives $1^{m} = 1$ .

[L3]

Real finite sums (Finite sums and finite products, by recursion): $\sum_{k < 0} u_{k} = 0$ and $\sum_{k < σ (N)} u_{k} = \sum_{k < N} u_{k} + u_{N}$ ; additivity $\sum (u_{k} + v_{k}) = \sum u_{k} + \sum v_{k}$ , scaling $\sum λ u_{k} = λ \sum u_{k}$ , and splitting $\sum_{k < N} u_{k} = \sum_{k < p} u_{k} + \sum_{j < N - p} u_{p + j}$ for $p \leq N$ (Laws of finite sums and finite products, clauses 1, 2 and 3).

[L4]

$ι$ is additive and multiplicative with $ι (0) = 0$ and $ι (1) = 1$ (clause 0 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).

[L5]

Binomial coefficients (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ): $(\binom{m}{0}) = 1$ and $(\binom{m}{j}) = 0$ for $j > m$ ; Pascal's rule $(\binom{σ (m)}{σ (j)}) = (\binom{m}{j}) + (\binom{m}{σ (j)})$ for all $m, j$ (Pascal's rule $(\binom{n + 1}{k + 1}) = (\binom{n}{k}) + (\binom{n}{k + 1})$ , and the hockey-stick identity $\sum_{i \leq n} (\binom{i}{k}) = (\binom{n + 1}{k + 1})$ , clause 1).

[L6]

Field arithmetic of $R$ : associativity, commutativity, distributivity, $0 \cdot a = 0$ (Field, Ordered field, Multiplication by zero: $0 \cdot a = 0$ ).

[L7]

Arithmetic of $N$ : for $k \leq n$ , $k + (n - k) = n$ , and hence $(n - k) + 1 = σ (n) - k$ and $σ (n) - σ (k) = n - k$ ; every nonzero natural is a successor (Order on the natural numbers, Addition is cancellative, Every nonzero natural number is a successor, Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ for the truncated difference).

Proof

technique · induction

1.1

Both sides are functions of $n$ with $x, y$ fixed, and the induction is on $n$ . Note first that $c_{σ (n)} = ι (\binom{n}{σ (n)}) = ι (0) = 0$ , since $σ (n) > n$ .

givenL4L5

1.2

Base case $n = 0$ . The left-hand side is $(x + y)^{0} = 1$ by [L2]. The right-hand side is $\sum_{k < 1} ι (\binom{0}{k}) x^{k} y^{0 - k} = ι (\binom{0}{0}) x^{0} y^{0} = 1 \cdot 1 \cdot 1 = 1$ , using [L3], $(\binom{0}{0}) = 1$ , $ι (1) = 1$ and [L2]. This is correct at $x = 0$ and at $y = 0$ as well, because $a^{0} = 1$ for every real $a$ .

baseL2L3L4L5

1.3

Inductive hypothesis: fix $n$ and assume $(x + y)^{n} = \sum_{k < σ (n)} c_{k} x^{k} y^{n - k}$ for all $x, y \in R$ .

2.1

Expanding one factor. By [L2] and distributivity, $(x + y)^{σ (n)} = (x + y)^{n} (x + y) = (\sum_{k < σ (n)} c_{k} x^{k} y^{n - k}) x + (\sum_{k < σ (n)} c_{k} x^{k} y^{n - k}) y$ , using the hypothesis of step 1.3; and by the scaling clause of [L3] together with $x^{k} x = x^{σ (k)}$ and $y^{n - k} y = y^{(n - k) + 1}$ this equals $Σ_{1} + Σ_{2}$ with $Σ_{1} : = \sum_{k < σ (n)} c_{k} x^{σ (k)} y^{n - k}$ and $Σ_{2} : = \sum_{k < σ (n)} c_{k} x^{k} y^{(n - k) + 1}$ .

step 1.3L2L3L6

3.1

Rewriting $Σ_{2}$ . For $k \leq n$ one has $(n - k) + 1 = σ (n) - k$ by [L7], so $Σ_{2} = \sum_{k < σ (n)} c_{k} x^{k} y^{σ (n) - k}$ . Extending the range by one term costs nothing: by the recursion clause of [L3], $\sum_{k < σ (σ (n))} c_{k} x^{k} y^{σ (n) - k} = Σ_{2} + c_{σ (n)} x^{σ (n)} y^{0}$ , and $c_{σ (n)} = 0$ by step 1.1, so the added term is $0$ by [L6] and $Σ_{2} = \sum_{k < σ (σ (n))} c_{k} x^{k} y^{σ (n) - k}$ .

step 1.1step 2.1L3L6L7

3.2

Rewriting $Σ_{1}$ . Define a list $b$ of length $σ (σ (n))$ by $b_{0} : = 0$ and $b_{σ (i)} : = c_{i} x^{σ (i)} y^{n - i}$ for $i < σ (n)$ ; every index below $σ (σ (n))$ is $0$ or a successor $σ (i)$ with $i < σ (n)$ , by [L7], so $b$ is well defined. Splitting at $p = 1$ by [L3] and using $σ (σ (n)) - 1 = σ (n)$ and $1 + i = σ (i)$ , $\sum_{j < σ (σ (n))} b_{j} = b_{0} + \sum_{i < σ (n)} b_{σ (i)} = 0 + Σ_{1} = Σ_{1}$ .

step 2.1L3L6L7

4.1

Adding the two. By step 3.1, step 3.2 and the additivity clause of [L3], $(x + y)^{σ (n)} = \sum_{k < σ (σ (n))} (b_{k} + c_{k} x^{k} y^{σ (n) - k})$ . Evaluate the general term. At $k = 0$ it is $0 + ι (\binom{n}{0}) x^{0} y^{σ (n)} = y^{σ (n)} = ι (\binom{σ (n)}{0}) x^{0} y^{σ (n) - 0}$ , both coefficients being $ι (1) = 1$ . At $k = σ (i)$ with $i < σ (n)$ it is $c_{i} x^{σ (i)} y^{n - i} + c_{σ (i)} x^{σ (i)} y^{σ (n) - σ (i)}$ , and $σ (n) - σ (i) = n - i$ by [L7], so the term equals $(ι (\binom{n}{i}) + ι (\binom{n}{σ (i)})) x^{σ (i)} y^{σ (n) - σ (i)} = ι (\binom{σ (n)}{σ (i)}) x^{σ (i)} y^{σ (n) - σ (i)}$ by the additivity of $ι$ and Pascal's rule. Hence $(x + y)^{σ (n)} = \sum_{k < σ (σ (n))} ι (\binom{σ (n)}{k}) x^{k} y^{σ (n) - k}$ , which is the claim at $σ (n)$ .

step 3.1step 3.2L3L4L5L6L7

5.1

By step 1.2, step 4.1 and induction the identity holds for every $n \in N$ and all reals $x$ , $y$ ; in particular at $x = 0$ or $y = 0$ , where the convention $a^{0} = 1$ of Integer powers $a^{m}$ is what makes the extreme terms come out right and no exceptional case is needed.

step 1.2step 4.1L1L2discharge-induction∎

Remarks

Two index traps, both checked. The sum runs over $k < n + 1$ , that is $k \leq n$ , so the exponent $n - k$ is never a truncated difference in disguise; and the inductive step needs the coefficient $(\binom{n}{σ (n)})$ , which is $0$ by the boundary values of The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ rather than undefined. Step 1.1 records that once and both rewritings use it.
Where $0^{0}$ matters. At $x = 0$ the term with $k = 0$ is $ι (\binom{n}{0}) 0^{0} y^{n} = y^{n}$ , and the identity reads $y^{n} = y^{n}$ . A treatment leaving $0^{0}$ undefined would have to state the theorem with exceptions; Integer powers $a^{m}$ fixes $a^{0} = 1$ for every real $a$ , so there are none.
The ring version is a different statement. It says the same thing about $x, y$ in a commutative ring, with $ι (\binom{n}{k})$ replaced by the $(\binom{n}{k})$ -fold multiple of the ring element. Making it requires rings, which come later in the reading order; the pointer to Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides ↗ is orientation only and nothing above rests on it.

Depends on

Used by

Dependency tree · two levels

52 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 theorem (Wikipedia) (standard reference, not scraped)
Binomial coefficient (Wikipedia) (standard reference, not scraped)
Pascal's rule (Wikipedia) (standard reference, not scraped)

The binomial theorem in RR: (x+y)n=∑k<n+1ι ⁣(nk) xky n−k(x+y)n=∑k<n+1​ι(kn​)xkyn−k