LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25

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.

Distributivity and the successor law for multiplication

Statement

For all $a, b, c, n \in N$ : (left distributivity) $a \cdot (b + c) = a \cdot b + a \cdot c$ ; and (successor-left law) $σ (a) \cdot n = a \cdot n + n$ .

Facts & Assumptions

Given: multiplication $m \cdot 0 = 0$ , $m \cdot σ (n) = m \cdot n + m$ and addition $m + 0 = m$ , $m + σ (k) = σ (m + k)$ (Multiplication of natural numbers, Addition of natural numbers); in particular the addition recursion $a + σ (k) = σ (a + k)$ is available.

[L1]

Addition is associative (Addition is associative) and commutative (Addition is commutative).

[L2]

The induction principle (The principle of mathematical induction).

Proof

technique · induction on $c$ for distributivity, with a second induction on $n$ for the successor law

1.1

Base $c = 0$ : $a \cdot (b + 0) = a \cdot b = a \cdot b + 0 = a \cdot b + a \cdot 0$ , using $b + 0 = b$ and $a \cdot 0 = 0$ .

base

1.2

Inductive hypothesis: $a \cdot (b + c) = a \cdot b + a \cdot c$ .

1.3

Successor-left law $σ (a) \cdot n = a \cdot n + n$ , by a second induction on $n$ : base $n = 0$ gives $σ (a) \cdot 0 = 0 = a \cdot 0 + 0$ ; assuming $σ (a) \cdot n = a \cdot n + n$ , the step gives $σ (a) \cdot σ (n) = σ (a) \cdot n + σ (a) = (a \cdot n + n) + σ (a) = a \cdot n + (n + σ (a)) = a \cdot n + σ (n + a) = a \cdot n + σ (a + n) = a \cdot n + (a + σ (n)) = (a \cdot n + a) + σ (n) = a \cdot σ (n) + σ (n)$ , using associativity and commutativity [L1] and $a + σ (k) = σ (a + k)$ .

L1given

2.1

Step: $a \cdot (b + σ (c)) = a \cdot σ (b + c) = a \cdot (b + c) + a = (a \cdot b + a \cdot c) + a = a \cdot b + (a \cdot c + a) = a \cdot b + a \cdot σ (c)$ , using $b + σ (c) = σ (b + c)$ , the multiplication recursion, the hypothesis, associativity [L1], and $a \cdot σ (c) = a \cdot c + a$ .

step 1.2L1

3.1

By induction [L2], $a \cdot (b + c) = a \cdot b + a \cdot c$ for all $c$ (hence all $a, b, c$ ) and $σ (a) \cdot n = a \cdot n + n$ for all $a, n$ .

step 2.1step 1.3discharge-induction∎

Depends on

Used by

Dependency tree · two levels

13 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

T. Tao, Analysis I, 3rd ed., §2.1-2.3 (Peano axioms, recursion, arithmetic) (standard reference, not scraped)
Peano axioms (Wikipedia) (standard reference, not scraped)
W. Aitken, MATH 378 Ch. 1: The Peano Axioms (CSU San Marcos) (standard reference, not scraped)