Skip to content
Axiomatic Wiki
Lemma·L18

Order and multiplication

No zero divisors, and multiplying by a non-zero number preserves order.

For all , with from D028 and from D029:(i) ;(ii) ;(iii) .
In words
A product of non-zero naturals is non-zero; multiplying both sides of a strict inequality by a non-zero number keeps it strict; and a non-zero factor can be cancelled from an equation of products.
Rests onF02F03F04F06F08F09F11F12F14A01A06A08
Never needed: F05 · F10 · F13 · A02 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    (i) By L15 (vii) write and . Then by D028 and D027, and successors are never by (P3).
  2. 2
    (ii) From , L17 (ii) gives with . Then by distributivity, and by (i). So by L17 (ii) read right to left.
  3. 3
    (iii) Suppose with . By L16: if then by (ii), contradicting equality with L15 (i) and substitutivity; the case is symmetric. Hence .
∎

Remarks

Part (i), "no zero divisors", makes an integral domain in miniature and is exactly what L21 needs to keep factorials positive. Parts (ii) and (iii) are the multiplicative analogues of L17 and power the uniqueness half of the division algorithm and the size bound in divisibility.
Wikipedia ↗Nat.mul_lt_mul_left ↗

Used by

L19L21L51
Propose an edit2 published revisions