This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑀 ∈ ℕ0 → ( 𝑀 ∥ 1 ↔ 𝑀 = 1 ) )

Proof

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