Parity

Definition

An integer is even if and only if it's divisible by two. An integer is odd if and only if it's not divisible by two.

THEOREM
even_iff_mod_2_eq_zero: even ?a = (?a mod 2 = 0)


Proof unavailable

THEOREM
even_iff_mod_2_eq_zero: even ?a = (?a mod 2 = 0)


Proof unavailable

THEOREM    The sum of two even integers is an even integer. $$\forall a,b \in \mathbb{Z} : \even(a) \wedge \even(b) \Rightarrow \even(a + b)$$

Proof available

THEOREM    The sum of an even integer and an odd integer is an odd integer. $$\forall a,b \in \mathbb{Z} : \even(a) \wedge \odd(b) \Rightarrow \odd(a + b)$$

Proof available

THEOREM    The sum of two odd integers is an even integer. $$\forall a,b \in \mathbb{Z} : \odd(a) \wedge \odd(b) \Rightarrow \even(a + b)$$

Proof available

THEOREM

The product of two even integers is an even integer.

$$\forall a,b \in \mathbb{Z} : \even(a) \wedge \even(b) \Rightarrow \even(a * b)$$

Proof available

THEOREM

The product of an even integer and an odd integer is an even integer.

$$\forall a,b \in \mathbb{Z} : \even(a) \wedge \odd(b) \Rightarrow \even(a * b)$$

Proof available

THEOREM

The product of two odd integers is an odd integer.

$$\forall a,b \in \mathbb{Z} : \odd(a) \wedge \odd(b) \Rightarrow \odd(a * b)$$

Proof available