evenp1odd

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

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

Step	Hyp	Ref	Expression
1		evenz	$⊢ Z \in Even \to Z \in ℤ$
2	1	peano2zd	$⊢ Z \in Even \to Z + 1 \in ℤ$
3		iseven	$⊢ Z \in Even \leftrightarrow (Z \in ℤ \land \frac{Z}{2} \in ℤ)$
4		zcn	$⊢ Z \in ℤ \to Z \in ℂ$
5		pncan1	$⊢ Z \in ℂ \to Z + 1 - 1 = Z$
6	4 5	syl	$⊢ Z \in ℤ \to Z + 1 - 1 = Z$
7	6	eqcomd	$⊢ Z \in ℤ \to Z = Z + 1 - 1$
8	7	oveq1d	$⊢ Z \in ℤ \to \frac{Z}{2} = \frac{Z + 1 - 1}{2}$
9	8	eleq1d	$⊢ Z \in ℤ \to (\frac{Z}{2} \in ℤ \leftrightarrow \frac{Z + 1 - 1}{2} \in ℤ)$
10	9	biimpa	$⊢ (Z \in ℤ \land \frac{Z}{2} \in ℤ) \to \frac{Z + 1 - 1}{2} \in ℤ$
11	3 10	sylbi	$⊢ Z \in Even \to \frac{Z + 1 - 1}{2} \in ℤ$
12		isodd2	$⊢ Z + 1 \in Odd \leftrightarrow (Z + 1 \in ℤ \land \frac{Z + 1 - 1}{2} \in ℤ)$
13	2 11 12	sylanbrc	$⊢ Z \in Even \to Z + 1 \in Odd$

Metamath Proof Explorer