Theorem 2dvdsoddm1

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

	Ref	Expression
Assertion	2dvdsoddm1	⊢ ( 𝑍 ∈ Odd → 2 ∥ ( 𝑍 − 1 ) )

Proof

Step	Hyp	Ref	Expression
1		2ndvdsodd	⊢ ( 𝑍 ∈ Odd → ¬ 2 ∥ 𝑍 )
2		oddz	⊢ ( 𝑍 ∈ Odd → 𝑍 ∈ ℤ )
3		oddm1even	⊢ ( 𝑍 ∈ ℤ → ( ¬ 2 ∥ 𝑍 ↔ 2 ∥ ( 𝑍 − 1 ) ) )
4	2 3	syl	⊢ ( 𝑍 ∈ Odd → ( ¬ 2 ∥ 𝑍 ↔ 2 ∥ ( 𝑍 − 1 ) ) )
5	1 4	mpbid	⊢ ( 𝑍 ∈ Odd → 2 ∥ ( 𝑍 − 1 ) )