Skip to content
Axiomatic Wiki
Lemma·L53

The integers have no zero divisors

If a product of two integers is zero, one of the factors must be zero.

For : if then , with from D060.
In words
If two integers multiply to zero, at least one of them must itself be zero.
Rests onF02F03F04F05F06F08F09F11F12F13F14A01A02A06A08
Never needed: F10 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    Suppose toward a contradiction that and and . By L50 applied to (T24) with : since , either or ; likewise for .
  2. 2
    Case , : L51 gives . Since , this reads , i.e. and (D062), which is false.
  3. 3
    Case , : L52 gives , so L51 gives . By the sign rule for multiplying by a negation and , this reads ; but directly by D059 (swapping the coordinates of gives back), so again , false as above.
  4. 4
    Case , : symmetric to the previous case, using the sign rule for negating the first factor: again , false.
  5. 5
    Case , : L52 gives and , so L51 gives . By the sign rule for negating both factors and , again , false.
  6. 6
    Assuming and (together with ) leads to a contradiction in all four cases, so (negation) that assumption fails: or .
∎

Remarks

Makes an integral domain (a commutative ring with no zero divisors), though that term is not separately defined in this library. Immediately gives multiplicative cancellation by nonzero integers, the key fact needed for the rational equivalence relation to be transitive.
Wikipedia ↗mul_eq_zero ↗

Used by

L54L59
Propose an edit1 published revision