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 ) )