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

Metamath Proof Explorer

Theorem dvdsprm

Description: An integer greater than or equal to 2 divides a prime number iff it is equal to it. (Contributed by Paul Chapman, 26-Oct-2012)

Ref Expression
Assertion dvdsprm ⊢ N ∈ ℤ ≥ 2 ∧ P ∈ ℙ → N ∥ P ↔ N = P

Proof

Step Hyp Ref Expression
1 breq1 ⊢ z = N → z ∥ P ↔ N ∥ P
2 eqeq1 ⊢ z = N → z = P ↔ N = P
3 1 2 imbi12d ⊢ z = N → z ∥ P → z = P ↔ N ∥ P → N = P
4 3 rspcv ⊢ N ∈ ℤ ≥ 2 → ∀ z ∈ ℤ ≥ 2 z ∥ P → z = P → N ∥ P → N = P
5 isprm4 ⊢ P ∈ ℙ ↔ P ∈ ℤ ≥ 2 ∧ ∀ z ∈ ℤ ≥ 2 z ∥ P → z = P
6 5 simprbi ⊢ P ∈ ℙ → ∀ z ∈ ℤ ≥ 2 z ∥ P → z = P
7 4 6 impel ⊢ N ∈ ℤ ≥ 2 ∧ P ∈ ℙ → N ∥ P → N = P
8 eluzelz ⊢ N ∈ ℤ ≥ 2 → N ∈ ℤ
9 iddvds ⊢ N ∈ ℤ → N ∥ N
10 breq2 ⊢ N = P → N ∥ N ↔ N ∥ P
11 9 10 syl5ibcom ⊢ N ∈ ℤ → N = P → N ∥ P
12 8 11 syl ⊢ N ∈ ℤ ≥ 2 → N = P → N ∥ P
13 12 adantr ⊢ N ∈ ℤ ≥ 2 ∧ P ∈ ℙ → N = P → N ∥ P
14 7 13 impbid ⊢ N ∈ ℤ ≥ 2 ∧ P ∈ ℙ → N ∥ P ↔ N = P