Metamath Proof Explorer

Theorem 1gcd

Description: The GCD of one and an integer is one. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion 1gcd ⊢ M ∈ ℤ → 1 gcd M = 1

Proof

Step Hyp Ref Expression
1 1z ⊢ 1 ∈ ℤ
2 gcdcom ⊢ 1 ∈ ℤ ∧ M ∈ ℤ → 1 gcd M = M gcd 1
3 1 2 mpan ⊢ M ∈ ℤ → 1 gcd M = M gcd 1
4 gcd1 ⊢ M ∈ ℤ → M gcd 1 = 1
5 3 4 eqtrd ⊢ M ∈ ℤ → 1 gcd M = 1