Integer addition


Definition

$$\forall a,b,c,d \in \mathbb{N} : (a, b) + (c, d) = (a + c, b + d)$$
THEOREM   

Integer addition is closed.

$$\forall x,y \in \mathbb{Z} : x + y \in \mathbb{Z}$$

Proof available

THEOREM    $$\forall x \in \mathbb{Z} : x + (-x) = 0$$

Proof available

THEOREM    $$\forall x \in \mathbb{Z} : (-x) + x = 0$$

Proof available

THEOREM    $$\forall x \in \mathbb{Z} \exists! -x \in \mathbb{Z} : x + (-x) = (-x) + x = 0$$

Proof available

LEMMA   

Zero is a left identity element of integer addition.

$$\forall x \in \mathbb{Z} : 0 + x = x$$

Proof available

LEMMA   

Zero is a right identity element of integer addition.

$$\forall x \in \mathbb{Z} : x + 0 = x$$

Proof available

THEOREM   

Zero is the identity element of integer addition.

Proof available

THEOREM   

Integer addition is well-defined.

$$\forall x, x', y, y' \in \mathbb{Z} : x = x' \wedge y = y' \Rightarrow x + y = x' + y'$$

Proof available

THEOREM   

Integer addition is commutative.

$$\forall x,y \in \mathbb{Z} : x + y = y + x$$

Proof available

THEOREM   

Integer addition is associative.

$$\forall x,y,z \in \mathbb{Z} : x + y + z = x + (y + z)$$

Proof available

LEMMA   

Integer addition is left-cancellative.

$$\forall x,y,z \in \mathbb{Z} : z + x = z + y \Rightarrow x = y$$

Proof available

LEMMA   

Integer addition is right-cancellative.

$$\forall x,y,z \in \mathbb{Z} : x + z = y + z \Rightarrow x = y$$

Proof available

THEOREM   

Integer addition is cancellative.

Proof available

THEOREM   

The sum of two positive integers is positive.

$$\forall x,y \in \mathbb{Z} : x \gt 0 \wedge y \gt 0 \Rightarrow x + y \gt 0$$

Proof unavailable

THEOREM   

The sum of two negative integers is negative.

$$\forall x,y \in \mathbb{Z} : x \lt 0 \wedge y \lt 0 \Rightarrow x + y \lt 0$$

Proof unavailable

Proper supersets