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 e. ZZ -> ( 1 gcd M ) = 1 )

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
2 gcdcom 
 |-  ( ( 1 e. ZZ /\ M e. ZZ ) -> ( 1 gcd M ) = ( M gcd 1 ) )
3 1 2 mpan 
 |-  ( M e. ZZ -> ( 1 gcd M ) = ( M gcd 1 ) )
4 gcd1 
 |-  ( M e. ZZ -> ( M gcd 1 ) = 1 )
5 3 4 eqtrd 
 |-  ( M e. ZZ -> ( 1 gcd M ) = 1 )