Metamath Proof Explorer

Theorem oddm1div2z

Description: The result of dividing an odd number decreased by 1 and then divided by 2 is an integer. (Contributed by AV, 15-Jun-2020)

		Ref	Expression
	Assertion	oddm1div2z	$⊢ Z \in Odd \to \frac{Z - 1}{2} \in ℤ$

Step	Hyp	Ref	Expression
1		oddp1div2z	$⊢ Z \in Odd \to \frac{Z + 1}{2} \in ℤ$
2		oddz	$⊢ Z \in Odd \to Z \in ℤ$
3		zob	$⊢ Z \in ℤ \to (\frac{Z + 1}{2} \in ℤ \leftrightarrow \frac{Z - 1}{2} \in ℤ)$
4	2 3	syl	$⊢ Z \in Odd \to (\frac{Z + 1}{2} \in ℤ \leftrightarrow \frac{Z - 1}{2} \in ℤ)$
5	1 4	mpbid	$⊢ Z \in Odd \to \frac{Z - 1}{2} \in ℤ$