Metamath Proof Explorer

Theorem oddp1eveni

Description: The successor of an odd number is even. (Contributed by AV, 16-Jun-2020)

		Ref	Expression
	Assertion	oddp1eveni	$⊢ Z \in Odd \to Z + 1 \in Even$

Step	Hyp	Ref	Expression
1		oddz	$⊢ Z \in Odd \to Z \in ℤ$
2	1	peano2zd	$⊢ Z \in Odd \to Z + 1 \in ℤ$
3		oddp1div2z	$⊢ Z \in Odd \to \frac{Z + 1}{2} \in ℤ$
4		iseven	$⊢ Z + 1 \in Even \leftrightarrow (Z + 1 \in ℤ \land \frac{Z + 1}{2} \in ℤ)$
5	2 3 4	sylanbrc	$⊢ Z \in Odd \to Z + 1 \in Even$