This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2dvdsoddm1

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

		Ref	Expression
	Assertion	2dvdsoddm1	$⊢ Z \in Odd \to 2 ∥ (Z - 1)$

Step	Hyp	Ref	Expression
1		2ndvdsodd	$⊢ Z \in Odd \to \neg 2 ∥ Z$
2		oddz	$⊢ Z \in Odd \to Z \in ℤ$
3		oddm1even	$⊢ Z \in ℤ \to (\neg 2 ∥ Z \leftrightarrow 2 ∥ (Z - 1))$
4	2 3	syl	$⊢ Z \in Odd \to (\neg 2 ∥ Z \leftrightarrow 2 ∥ (Z - 1))$
5	1 4	mpbid	$⊢ Z \in Odd \to 2 ∥ (Z - 1)$