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∈ℤ→Mgcd1=1

Proof

Step Hyp Ref Expression
1 1z ⊢1∈ℤ
2 gcddvds ⊢M∈ℤ∧1∈ℤ→Mgcd1∥M∧Mgcd1∥1
3 1 2 mpan2 ⊢M∈ℤ→Mgcd1∥M∧Mgcd1∥1
4 3 simprd ⊢M∈ℤ→Mgcd1∥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∈ℤ∧1∈ℤ∧¬M=0∧1=0→Mgcd1∈ℕ
10 8 9 mpan2 ⊢M∈ℤ∧1∈ℤ→Mgcd1∈ℕ
11 1 10 mpan2 ⊢M∈ℤ→Mgcd1∈ℕ
12 11 nnzd ⊢M∈ℤ→Mgcd1∈ℤ
13 1nn ⊢1∈ℕ
14 dvdsle ⊢Mgcd1∈ℤ∧1∈ℕ→Mgcd1∥1→Mgcd1≤1
15 12 13 14 sylancl ⊢M∈ℤ→Mgcd1∥1→Mgcd1≤1
16 4 15 mpd ⊢M∈ℤ→Mgcd1≤1
17 nnle1eq1 ⊢Mgcd1∈ℕ→Mgcd1≤1↔Mgcd1=1
18 11 17 syl ⊢M∈ℤ→Mgcd1≤1↔Mgcd1=1
19 16 18 mpbid ⊢M∈ℤ→Mgcd1=1