Theorem 2dvdsoddm1

Description: 2 divides an odd number decreased by 1. (Contributed by AV, 18-Jun-2020)

	Ref	Expression
Assertion	2dvdsoddm1	$$⊢Z\in \mathrm{Odd}\to 2\parallel \left(Z-1\right)$$

Proof

Step	Hyp	Ref	Expression
1		2ndvdsodd	$$⊢Z\in \mathrm{Odd}\to \neg 2\parallel Z$$
2		oddz	$$⊢Z\in \mathrm{Odd}\to Z\in \mathbb{Z}$$
3		oddm1even	$$⊢Z\in \mathbb{Z}\to \left(\neg 2\parallel Z\leftrightarrow 2\parallel \left(Z-1\right)\right)$$
4	2 3	syl	$$⊢Z\in \mathrm{Odd}\to \left(\neg 2\parallel Z\leftrightarrow 2\parallel \left(Z-1\right)\right)$$
5	1 4	mpbid	$$⊢Z\in \mathrm{Odd}\to 2\parallel \left(Z-1\right)$$