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

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 ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ) → ( 𝑀 ∥ 𝑃 ↔ ( 𝑀 = 𝑃 ∨ 𝑀 = 1 ) ) )

Proof

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