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