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\in \mathbb{Z}\to \left(\neg 2\parallel Z\leftrightarrow 2\gcd Z=1\right)$$

Proof

Step	Hyp	Ref	Expression
1		2prm	$$⊢2\in \mathbb{P}$$
2		coprm	$$⊢\left(2\in \mathbb{P}\wedge Z\in \mathbb{Z}\right)\to \left(\neg 2\parallel Z\leftrightarrow 2\gcd Z=1\right)$$
3	1 2	mpan	$$⊢Z\in \mathbb{Z}\to \left(\neg 2\parallel Z\leftrightarrow 2\gcd Z=1\right)$$