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