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 ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑁 ∥ 𝑃 ↔ 𝑁 = 𝑃 ) )

Proof

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