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	⊢ ( 𝑀 ∈ ℤ → ( 1 gcd 𝑀 ) = 1 )

Proof

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