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 ) )