Skip to content
Axiomatic Wiki
Lemma·L52

Negation reverses the sign of an integer

An integer is negative exactly when its negation is positive.

For : with from D062 and from D059.
In words
An integer is less than zero exactly when its negation is greater than zero.
Rests onF02F09F14A01A06
Never needed: F03 · F04 · F05 · F06 · F08 · F10 · F11 · F12 · F13 · A02 · A03 · A04 · A05 · A07 · A08 (computed from the citation graph, not asserted).

Proof

  1. 1
    Write , so (D059) and . By D062, unwinds to , and unwinds to . Using D027 and commutativity ( ) on both, each condition reduces to the same statement on , so they are equivalent.
∎

Remarks

Used, together with L51, to determine the sign of a product from the signs of its factors in L53.
Wikipedia ↗neg_pos ↗

Used by

L53
Propose an edit1 published revision