# 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}\in ℤ\to {M}\mathrm{gcd}1=1$

### Proof

Step Hyp Ref Expression
1 1z ${⊢}1\in ℤ$
2 gcddvds ${⊢}\left({M}\in ℤ\wedge 1\in ℤ\right)\to \left(\left({M}\mathrm{gcd}1\right)\parallel {M}\wedge \left({M}\mathrm{gcd}1\right)\parallel 1\right)$
3 1 2 mpan2 ${⊢}{M}\in ℤ\to \left(\left({M}\mathrm{gcd}1\right)\parallel {M}\wedge \left({M}\mathrm{gcd}1\right)\parallel 1\right)$
4 3 simprd ${⊢}{M}\in ℤ\to \left({M}\mathrm{gcd}1\right)\parallel 1$
5 ax-1ne0 ${⊢}1\ne 0$
6 simpr ${⊢}\left({M}=0\wedge 1=0\right)\to 1=0$
7 6 necon3ai ${⊢}1\ne 0\to ¬\left({M}=0\wedge 1=0\right)$
8 5 7 ax-mp ${⊢}¬\left({M}=0\wedge 1=0\right)$
9 gcdn0cl ${⊢}\left(\left({M}\in ℤ\wedge 1\in ℤ\right)\wedge ¬\left({M}=0\wedge 1=0\right)\right)\to {M}\mathrm{gcd}1\in ℕ$
10 8 9 mpan2 ${⊢}\left({M}\in ℤ\wedge 1\in ℤ\right)\to {M}\mathrm{gcd}1\in ℕ$
11 1 10 mpan2 ${⊢}{M}\in ℤ\to {M}\mathrm{gcd}1\in ℕ$
12 11 nnzd ${⊢}{M}\in ℤ\to {M}\mathrm{gcd}1\in ℤ$
13 1nn ${⊢}1\in ℕ$
14 dvdsle ${⊢}\left({M}\mathrm{gcd}1\in ℤ\wedge 1\in ℕ\right)\to \left(\left({M}\mathrm{gcd}1\right)\parallel 1\to {M}\mathrm{gcd}1\le 1\right)$
15 12 13 14 sylancl ${⊢}{M}\in ℤ\to \left(\left({M}\mathrm{gcd}1\right)\parallel 1\to {M}\mathrm{gcd}1\le 1\right)$
16 4 15 mpd ${⊢}{M}\in ℤ\to {M}\mathrm{gcd}1\le 1$
17 nnle1eq1 ${⊢}{M}\mathrm{gcd}1\in ℕ\to \left({M}\mathrm{gcd}1\le 1↔{M}\mathrm{gcd}1=1\right)$
18 11 17 syl ${⊢}{M}\in ℤ\to \left({M}\mathrm{gcd}1\le 1↔{M}\mathrm{gcd}1=1\right)$
19 16 18 mpbid ${⊢}{M}\in ℤ\to {M}\mathrm{gcd}1=1$