Theorem isoddgcd1

Description: The predicate "is an odd number". An odd number and 2 have 1 as greatest common divisor. (Contributed by AV, 1-Jul-2020) (Revised by AV, 8-Aug-2021)

	Ref	Expression
Assertion	isoddgcd1	|- ( Z e. ZZ -> ( -. 2 || Z <-> ( 2 gcd Z ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		2prm	|- 2 e. Prime
2		coprm	|- ( ( 2 e. Prime /\ Z e. ZZ ) -> ( -. 2 || Z <-> ( 2 gcd Z ) = 1 ) )
3	1 2	mpan	|- ( Z e. ZZ -> ( -. 2 || Z <-> ( 2 gcd Z ) = 1 ) )