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

Proof

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