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 e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( 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 e. ( ZZ>= ` 2 ) -> ( A. z e. ( ZZ>= ` 2 ) ( z || P -> z = P ) -> ( N || P -> N = P ) ) )
5 isprm4 
 |-  ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. z e. ( ZZ>= ` 2 ) ( z || P -> z = P ) ) )
6 5 simprbi 
 |-  ( P e. Prime -> A. z e. ( ZZ>= ` 2 ) ( z || P -> z = P ) )
7 4 6 impel 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( N || P -> N = P ) )
8 eluzelz 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. ZZ )
9 iddvds 
 |-  ( N e. ZZ -> N || N )
10 breq2 
 |-  ( N = P -> ( N || N <-> N || P ) )
11 9 10 syl5ibcom 
 |-  ( N e. ZZ -> ( N = P -> N || P ) )
12 8 11 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N = P -> N || P ) )
13 12 adantr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( N = P -> N || P ) )
14 7 13 impbid 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( N || P <-> N = P ) )