Theorem 2dvdsoddm1

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

	Ref	Expression
Assertion	2dvdsoddm1	|- ( Z e. Odd -> 2 || ( Z - 1 ) )

Proof

Step	Hyp	Ref	Expression
1		2ndvdsodd	|- ( Z e. Odd -> -. 2 || Z )
2		oddz	|- ( Z e. Odd -> Z e. ZZ )
3		oddm1even	|- ( Z e. ZZ -> ( -. 2 || Z <-> 2 || ( Z - 1 ) ) )
4	2 3	syl	|- ( Z e. Odd -> ( -. 2 || Z <-> 2 || ( Z - 1 ) ) )
5	1 4	mpbid	|- ( Z e. Odd -> 2 || ( Z - 1 ) )