Metamath Proof Explorer

Theorem dvds1

Description: The only nonnegative integer that divides 1 is 1. (Contributed by Mario Carneiro, 2-Jul-2015)

Ref Expression
Assertion dvds1 ⊢ M ∈ ℕ 0 → M ∥ 1 ↔ M = 1

Proof

Step Hyp Ref Expression
1 simpl ⊢ M ∈ ℕ 0 ∧ M ∥ 1 → M ∈ ℕ 0
2 1nn0 ⊢ 1 ∈ ℕ 0
3 2 a1i ⊢ M ∈ ℕ 0 ∧ M ∥ 1 → 1 ∈ ℕ 0
4 simpr ⊢ M ∈ ℕ 0 ∧ M ∥ 1 → M ∥ 1
5 nn0z ⊢ M ∈ ℕ 0 → M ∈ ℤ
6 1dvds ⊢ M ∈ ℤ → 1 ∥ M
7 5 6 syl ⊢ M ∈ ℕ 0 → 1 ∥ M
8 7 adantr ⊢ M ∈ ℕ 0 ∧ M ∥ 1 → 1 ∥ M
9 dvdseq ⊢ M ∈ ℕ 0 ∧ 1 ∈ ℕ 0 ∧ M ∥ 1 ∧ 1 ∥ M → M = 1
10 1 3 4 8 9 syl22anc ⊢ M ∈ ℕ 0 ∧ M ∥ 1 → M = 1
11 10 ex ⊢ M ∈ ℕ 0 → M ∥ 1 → M = 1
12 id ⊢ M = 1 → M = 1
13 1z ⊢ 1 ∈ ℤ
14 iddvds ⊢ 1 ∈ ℤ → 1 ∥ 1
15 13 14 ax-mp ⊢ 1 ∥ 1
16 12 15 eqbrtrdi ⊢ M = 1 → M ∥ 1
17 11 16 impbid1 ⊢ M ∈ ℕ 0 → M ∥ 1 ↔ M = 1