Theorem gcd2odd1

Description: The greatest common divisor of an odd number and 2 is 1, i.e., 2 and any odd number are coprime. Remark: The proof using dfodd7 is longer (see proof in comment)! (Contributed by AV, 5-Jun-2023)

	Ref	Expression
Assertion	gcd2odd1	$$⊢Z\in \mathrm{Odd}\to Z\gcd 2=1$$

Proof

Step	Hyp	Ref	Expression
1		oddz	$$⊢Z\in \mathrm{Odd}\to Z\in \mathbb{Z}$$
2		2z	$$⊢2\in \mathbb{Z}$$
3		gcdcom	$$⊢\left(Z\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\to Z\gcd 2=2\gcd Z$$
4	1 2 3	sylancl	$$⊢Z\in \mathrm{Odd}\to Z\gcd 2=2\gcd Z$$
5		2ndvdsodd	$$⊢Z\in \mathrm{Odd}\to \neg 2\parallel Z$$
6		2prm	$$⊢2\in \mathbb{P}$$
7		coprm	$$⊢\left(2\in \mathbb{P}\wedge Z\in \mathbb{Z}\right)\to \left(\neg 2\parallel Z\leftrightarrow 2\gcd Z=1\right)$$
8	6 1 7	sylancr	$$⊢Z\in \mathrm{Odd}\to \left(\neg 2\parallel Z\leftrightarrow 2\gcd Z=1\right)$$
9	5 8	mpbid	$$⊢Z\in \mathrm{Odd}\to 2\gcd Z=1$$
10	4 9	eqtrd	$$⊢Z\in \mathrm{Odd}\to Z\gcd 2=1$$