Exercise 4.1.2 Show that the definition of negation on the integers is well-defined in the sense that if \((a — b) = (a' — b')\), then \(−(a — b) = −(a' — b')\) (so equal integers have equal negations).
-
\(\bullet\) Show that if \((a — b) = (a' — b')\), then \(−(a — b) = −(a' — b')\)
-
\(\Vdash\) \((a — b) = (a' — b')\)
-
\(\equiv\) { Definition 4.1.1 }
- \(a + b' = a' + b\)
-
\(\equiv\) { Symmetry of the equality on \(\mathbb N\) }
- \(a' + b = a + b'\)
-
\(\equiv\) { Commutativity of the additon on \(\mathbb N\) }
- \(b + a' = b' + a\)
-
\(\equiv\) { Definition 4.1.1 }
- \((b — a) = (b' — a')\)
-
\(\equiv\) { Definition 4.1.4 }
- \(−(a — b) = −(a' — b')\)
-
\(\square\)