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	⊢ ( 𝑍 ∈ Odd → ( 𝑍 gcd 2 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		oddz	⊢ ( 𝑍 ∈ Odd → 𝑍 ∈ ℤ )
2		2z	⊢ 2 ∈ ℤ
3		gcdcom	⊢ ( ( 𝑍 ∈ ℤ ∧ 2 ∈ ℤ ) → ( 𝑍 gcd 2 ) = ( 2 gcd 𝑍 ) )
4	1 2 3	sylancl	⊢ ( 𝑍 ∈ Odd → ( 𝑍 gcd 2 ) = ( 2 gcd 𝑍 ) )
5		2ndvdsodd	⊢ ( 𝑍 ∈ Odd → ¬ 2 ∥ 𝑍 )
6		2prm	⊢ 2 ∈ ℙ
7		coprm	⊢ ( ( 2 ∈ ℙ ∧ 𝑍 ∈ ℤ ) → ( ¬ 2 ∥ 𝑍 ↔ ( 2 gcd 𝑍 ) = 1 ) )
8	6 1 7	sylancr	⊢ ( 𝑍 ∈ Odd → ( ¬ 2 ∥ 𝑍 ↔ ( 2 gcd 𝑍 ) = 1 ) )
9	5 8	mpbid	⊢ ( 𝑍 ∈ Odd → ( 2 gcd 𝑍 ) = 1 )
10	4 9	eqtrd	⊢ ( 𝑍 ∈ Odd → ( 𝑍 gcd 2 ) = 1 )