Metamath Proof Explorer

Theorem dvdsprime

Description: If M divides a prime, then M is either the prime or one. (Contributed by Scott Fenton, 8-Apr-2014)

Ref Expression
Assertion dvdsprime ⊢ P ∈ ℙ ∧ M ∈ ℕ → M ∥ P ↔ M = P ∨ M = 1

Proof

Step Hyp Ref Expression
1 isprm2 ⊢ P ∈ ℙ ↔ P ∈ ℤ ≥ 2 ∧ ∀ m ∈ ℕ m ∥ P → m = 1 ∨ m = P
2 breq1 ⊢ m = M → m ∥ P ↔ M ∥ P
3 eqeq1 ⊢ m = M → m = 1 ↔ M = 1
4 eqeq1 ⊢ m = M → m = P ↔ M = P
5 3 4 orbi12d ⊢ m = M → m = 1 ∨ m = P ↔ M = 1 ∨ M = P
6 orcom ⊢ M = 1 ∨ M = P ↔ M = P ∨ M = 1
7 5 6 bitrdi ⊢ m = M → m = 1 ∨ m = P ↔ M = P ∨ M = 1
8 2 7 imbi12d ⊢ m = M → m ∥ P → m = 1 ∨ m = P ↔ M ∥ P → M = P ∨ M = 1
9 8 rspccva ⊢ ∀ m ∈ ℕ m ∥ P → m = 1 ∨ m = P ∧ M ∈ ℕ → M ∥ P → M = P ∨ M = 1
10 9 adantll ⊢ P ∈ ℤ ≥ 2 ∧ ∀ m ∈ ℕ m ∥ P → m = 1 ∨ m = P ∧ M ∈ ℕ → M ∥ P → M = P ∨ M = 1
11 1 10 sylanb ⊢ P ∈ ℙ ∧ M ∈ ℕ → M ∥ P → M = P ∨ M = 1
12 prmz ⊢ P ∈ ℙ → P ∈ ℤ
13 iddvds ⊢ P ∈ ℤ → P ∥ P
14 12 13 syl ⊢ P ∈ ℙ → P ∥ P
15 14 adantr ⊢ P ∈ ℙ ∧ M ∈ ℕ → P ∥ P
16 breq1 ⊢ M = P → M ∥ P ↔ P ∥ P
17 15 16 syl5ibrcom ⊢ P ∈ ℙ ∧ M ∈ ℕ → M = P → M ∥ P
18 1dvds ⊢ P ∈ ℤ → 1 ∥ P
19 12 18 syl ⊢ P ∈ ℙ → 1 ∥ P
20 19 adantr ⊢ P ∈ ℙ ∧ M ∈ ℕ → 1 ∥ P
21 breq1 ⊢ M = 1 → M ∥ P ↔ 1 ∥ P
22 20 21 syl5ibrcom ⊢ P ∈ ℙ ∧ M ∈ ℕ → M = 1 → M ∥ P
23 17 22 jaod ⊢ P ∈ ℙ ∧ M ∈ ℕ → M = P ∨ M = 1 → M ∥ P
24 11 23 impbid ⊢ P ∈ ℙ ∧ M ∈ ℕ → M ∥ P ↔ M = P ∨ M = 1