Skip to content
Axiomatic Wiki
Lemma·L51

A product of positive integers is positive

If two integers are both greater than zero, so is their product.

For , if then , with from D062 and from D060.
In words
If two integers are both greater than zero, their product is also greater than zero.
Rests onF02F03F04F06F08F09F11F12F14A01A02A06A08
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    Write , , and (D057). By D062, unwinds to , i.e. ; likewise unwinds to .
  2. 2
    By L17 (ii), there are with , , , .
  3. 3
    Expanding and via distributivity on : Both right-hand sides are sums of the four terms (regrouped by commutativity/associativity), and the first has one extra term :
  4. 4
    by L18 (i) (no zero divisors on ), so by L17 (ii) read right to left, . By D060 and D062, this is exactly .
∎

Remarks

The engine behind L53: it establishes the "positive" quadrant of the sign rule for multiplication, and the other quadrants follow from it via negation.
Wikipedia ↗mul_pos ↗

Used by

L53
Propose an edit1 published revision