LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-02 (claude-opus-5)

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.

Order is compatible with multiplication

Statement

For all $m, n, k \in N$ : if $m \leq n$ then $m \cdot k \leq n \cdot k$ ; and if in addition $k \neq 0$ and $m < n$ , then $m \cdot k < n \cdot k$ (Order on the natural numbers).

Facts & Assumptions

Given: The order $m \leq n ⟺ \exists d (m + d = n)$ , with $m < n$ meaning $m \leq n$ and $m \neq n$ (Order on the natural numbers); addition with $m + 0 = m$ (Addition of natural numbers); and multiplication with $m \cdot 0 = 0$ , $m \cdot σ (n) = m \cdot n + m$ (Multiplication of natural numbers).

[L1]

Right distributivity $(m + d) \cdot k = m \cdot k + d \cdot k$ , from left distributivity and commutativity (Distributivity and the successor law for multiplication, Multiplication is commutative).

[L2]

No zero divisors: $d \neq 0$ and $k \neq 0 \Rightarrow d \cdot k \neq 0$ (The natural numbers have no zero divisors).

[L3]

Cancellation for addition: $x + k = y + k \Rightarrow x = y$ (Addition is cancellative).

[L4]

Addition is commutative: $x + y = y + x$ (Addition is commutative).

Proof

technique · direct

1.1

If $m \leq n$ , write $m + d = n$ ; then $n \cdot k = (m + d) \cdot k = m \cdot k + d \cdot k$ by right distributivity, so $m \cdot k \leq n \cdot k$ .

givenL1

2.1

If moreover $m < n$ then $d \neq 0$ , for $d = 0$ would give $n = m + 0 = m$ , contradicting $m \neq n$ ; then with $k \neq 0$ we get $d \cdot k \neq 0$ by [L2], so $m \cdot k + d \cdot k = n \cdot k$ with $d \cdot k \neq 0$ ; and $m \cdot k \neq n \cdot k$ , since equality would give $m \cdot k + d \cdot k = m \cdot k + 0$ , hence $d \cdot k + m \cdot k = 0 + m \cdot k$ by [L4] and $d \cdot k = 0$ by [L3], a contradiction; therefore $m \cdot k < n \cdot k$ .

step 1.1givenL2L3L4∎

Depends on

Used by

Dependency tree · two levels

19 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)