evenm1odd

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

		Ref	Expression
	Assertion	evenm1odd	$⊢ Z \in Even \to Z - 1 \in Odd$

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

Metamath Proof Explorer