Metamath Proof Explorer


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 Odd Z gcd 2 = 1

Proof

Step Hyp Ref Expression
1 oddz Z Odd Z
2 2z 2
3 gcdcom Z 2 Z gcd 2 = 2 gcd Z
4 1 2 3 sylancl Z Odd Z gcd 2 = 2 gcd Z
5 2ndvdsodd Z Odd ¬ 2 Z
6 2prm 2
7 coprm 2 Z ¬ 2 Z 2 gcd Z = 1
8 6 1 7 sylancr Z Odd ¬ 2 Z 2 gcd Z = 1
9 5 8 mpbid Z Odd 2 gcd Z = 1
10 4 9 eqtrd Z Odd Z gcd 2 = 1