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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oddz | ||
2 | 2z | ||
3 | gcdcom | ||
4 | 1 2 3 | sylancl | |
5 | 2ndvdsodd | ||
6 | 2prm | ||
7 | coprm | ||
8 | 6 1 7 | sylancr | |
9 | 5 8 | mpbid | |
10 | 4 9 | eqtrd |