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	$$⊢\left(N\in {\mathbb{Z}}_{\ge 2}\wedge P\in \mathbb{P}\right)\to \left(N\parallel P\leftrightarrow N=P\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq1	$$⊢z=N\to \left(z\parallel P\leftrightarrow N\parallel P\right)$$
2		eqeq1	$$⊢z=N\to \left(z=P\leftrightarrow N=P\right)$$
3	1 2	imbi12d	$$⊢z=N\to \left(\left(z\parallel P\to z=P\right)\leftrightarrow \left(N\parallel P\to N=P\right)\right)$$
4	3	rspcv	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(\forall z\in {\mathbb{Z}}_{\ge 2}\left(z\parallel P\to z=P\right)\to \left(N\parallel P\to N=P\right)\right)$$
5		isprm4	$$⊢P\in \mathbb{P}\leftrightarrow \left(P\in {\mathbb{Z}}_{\ge 2}\wedge \forall z\in {\mathbb{Z}}_{\ge 2}\left(z\parallel P\to z=P\right)\right)$$
6	5	simprbi	$$⊢P\in \mathbb{P}\to \forall z\in {\mathbb{Z}}_{\ge 2}\left(z\parallel P\to z=P\right)$$
7	4 6	impel	$$⊢\left(N\in {\mathbb{Z}}_{\ge 2}\wedge P\in \mathbb{P}\right)\to \left(N\parallel P\to N=P\right)$$
8		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in \mathbb{Z}$$
9		iddvds	$$⊢N\in \mathbb{Z}\to N\parallel N$$
10		breq2	$$⊢N=P\to \left(N\parallel N\leftrightarrow N\parallel P\right)$$
11	9 10	syl5ibcom	$$⊢N\in \mathbb{Z}\to \left(N=P\to N\parallel P\right)$$
12	8 11	syl	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(N=P\to N\parallel P\right)$$
13	12	adantr	$$⊢\left(N\in {\mathbb{Z}}_{\ge 2}\wedge P\in \mathbb{P}\right)\to \left(N=P\to N\parallel P\right)$$
14	7 13	impbid	$$⊢\left(N\in {\mathbb{Z}}_{\ge 2}\wedge P\in \mathbb{P}\right)\to \left(N\parallel P\leftrightarrow N=P\right)$$