Metamath Proof Explorer

Theorem gcd1

Description: The gcd of a number with 1 is 1. Theorem 1.4(d)1 in ApostolNT p. 16. (Contributed by Mario Carneiro, 19-Feb-2014)

Ref Expression
Assertion gcd1 
|- ( M e. ZZ -> ( M gcd 1 ) = 1 )

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
2 gcddvds 
 |-  ( ( M e. ZZ /\ 1 e. ZZ ) -> ( ( M gcd 1 ) || M /\ ( M gcd 1 ) || 1 ) )
3 1 2 mpan2 
 |-  ( M e. ZZ -> ( ( M gcd 1 ) || M /\ ( M gcd 1 ) || 1 ) )
4 3 simprd 
 |-  ( M e. ZZ -> ( M gcd 1 ) || 1 )
5 ax-1ne0 
 |-  1 =/= 0
6 simpr 
 |-  ( ( M = 0 /\ 1 = 0 ) -> 1 = 0 )
7 6 necon3ai 
 |-  ( 1 =/= 0 -> -. ( M = 0 /\ 1 = 0 ) )
8 5 7 ax-mp 
 |-  -. ( M = 0 /\ 1 = 0 )
9 gcdn0cl 
 |-  ( ( ( M e. ZZ /\ 1 e. ZZ ) /\ -. ( M = 0 /\ 1 = 0 ) ) -> ( M gcd 1 ) e. NN )
10 8 9 mpan2 
 |-  ( ( M e. ZZ /\ 1 e. ZZ ) -> ( M gcd 1 ) e. NN )
11 1 10 mpan2 
 |-  ( M e. ZZ -> ( M gcd 1 ) e. NN )
12 11 nnzd 
 |-  ( M e. ZZ -> ( M gcd 1 ) e. ZZ )
13 1nn 
 |-  1 e. NN
14 dvdsle 
 |-  ( ( ( M gcd 1 ) e. ZZ /\ 1 e. NN ) -> ( ( M gcd 1 ) || 1 -> ( M gcd 1 ) <_ 1 ) )
15 12 13 14 sylancl 
 |-  ( M e. ZZ -> ( ( M gcd 1 ) || 1 -> ( M gcd 1 ) <_ 1 ) )
16 4 15 mpd 
 |-  ( M e. ZZ -> ( M gcd 1 ) <_ 1 )
17 nnle1eq1 
 |-  ( ( M gcd 1 ) e. NN -> ( ( M gcd 1 ) <_ 1 <-> ( M gcd 1 ) = 1 ) )
18 11 17 syl 
 |-  ( M e. ZZ -> ( ( M gcd 1 ) <_ 1 <-> ( M gcd 1 ) = 1 ) )
19 16 18 mpbid 
 |-  ( M e. ZZ -> ( M gcd 1 ) = 1 )