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.1givenL1

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$ .

2.1step 1.1givenL2L3L4∎

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$ .

Order is compatible with multiplication

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources