Natural number addition


Definition 1

ProofWiki

Definition 2

$$ 0 + n = n \\ s(m) + n = s(m + n) $$

Definition 3

  add_0: 0 + ?a = ?a
add_Suc: Suc ?m + ?n = Suc (?m + ?n)
LEMMA   

Zero is a left identity element of natural number addition.

$$\forall x \in \mathbb{N} : 0 + x = x$$
Proof.    
LEMMA   

Zero is a right identity element of natural number addition.

$$\forall x \in \mathbb{N} : x + 0 = x$$
Proof.    
THEOREM   

Zero is an identity element of natural number addition.

\(\forall x \in \mathbb{N} : x + 0 = 0 + x = x\)
Proof.    

Zero is both a left and right identity element of natural number addition. Therefore, zero is an identity element of natural number addition.

THEOREM   

Natural number addition is commutative.

$$\forall x,y \in \mathbb{N} : x + y = y + x$$
Proof.    
THEOREM   

Natural number addition is associative.

$$\forall x,y,z \in \mathbb{N} : x + y + z = x + (y + z)$$
Proof.    
THEOREM   

Natural number addition is left-cancellative.

$$\forall a,b,c \in \mathbb{N} : a + b = a + c \Rightarrow b = c$$
Proof 1.     ProofWiki
Proof 2.    
THEOREM   

Natural number addition is right-cancellative.

$$\forall a,b,c \in \mathbb{N} : b + a = c + a \Rightarrow b = c$$
Proof 1.     ProofWiki
Proof 2.    
THEOREM   

Natural number addition is cancellative.

Proof.    

Natural number addition is both left and right-cancellative. Therefore, natural number addition is cancellative.

THEOREM   

Zero is the only idempotent element of natural number addition.

$$\begin{align} & 0 + 0 = 0 \\ & (x + 1) + (x + 1) \ne x + 1 \end{align}$$
THEOREM    $$\forall x \in \mathbb{N} : x + y = x \Leftrightarrow y = 0$$
THEOREM    \(\forall a,b,c \in \mathbb{N} : a \lt b \Rightarrow c + a \lt c + b\)
Proof.    
THEOREM    \(\forall a,b,c \in \mathbb{N} : a \lt b \Rightarrow a + c \lt b + c\)
Proof.    
THEOREM    \(\forall a,b,c,d \in \mathbb{N} : a \lt b \wedge c \lt d \Rightarrow a + c \lt b + d\)
Proof.    

Proper supersets

Parent topics