Skip to content
Axiomatic Wiki
Lemma·L54

Multiplicative cancellation in the integers

A nonzero factor can be cancelled from an equation of integer products.

For with : if then .
In words
If multiplying x and y by the same nonzero integer gives equal results, then x and y were already equal.
Rests onF02F03F04F05F06F08F09F11F12F13F14A01A02A06A08
Never needed: F10 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    From , add to both sides (substitutivity) and simplify with the inverse law of T22:
  2. 2
    By the sign rule for pulling a negation through multiplication and distributivity:
  3. 3
    By L53, or . Since , .
  4. 4
    Adding to both sides and simplifying with the associativity, inverse and identity laws of T22:
∎

Remarks

The integer analogue of L10, but for multiplication, and dependent on L53 rather than following from the group axioms alone. Used directly in the transitivity proof of L55.
Wikipedia ↗mul_left_cancel0 ↗

Used by

L55
Propose an edit1 published revision