Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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∈Nm, n, k \in \mathbb{N}: if m≤nm \le n then m⋅k≤n⋅km \cdot k \le n \cdot k; and if in addition k≠0k \ne 0 and m<nm < n, then m⋅k<n⋅km \cdot k < n \cdot k (Order on the natural numbers).

Facts & Assumptions

Given: The order m≤n  ⟺  ∃d (m+d=n)m \le n \iff \exists d\ (m + d = n), with m<nm < n meaning m≤nm \le n and m≠nm \ne n (Order on the natural numbers); addition with m+0=mm + 0 = m (Addition of natural numbers); and multiplication with m⋅0=0m \cdot 0 = 0, m⋅σ(n)=m⋅n+mm \cdot \sigma(n) = m \cdot n + m (Multiplication of natural numbers).

[L1]

Right distributivity (m+d)⋅k=m⋅k+d⋅k(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≠0d \ne 0 and k≠0⇒d⋅k≠0k \ne 0 \Rightarrow d \cdot k \ne 0 (The natural numbers have no zero divisors).

[L3]

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

[L4]

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

Proof

technique · direct
1.1

If m≤nm \le n, write m+d=nm + d = n; then n⋅k=(m+d)⋅k=m⋅k+d⋅kn \cdot k = (m + d) \cdot k = m \cdot k + d \cdot k by right distributivity, so m⋅k≤n⋅km \cdot k \le n \cdot k.

givenL1
2.1

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

step 1.1givenL2L3L4∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 25 results over 12 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources