Theorem nprmdvds1

Description: No prime number divides 1. (Contributed by Paul Chapman, 17-Nov-2012) (Proof shortened by Mario Carneiro, 2-Jul-2015)

	Ref	Expression
Assertion	nprmdvds1	$$⊢P\in \mathbb{P}\to \neg P\parallel 1$$

Proof

Step	Hyp	Ref	Expression
1		1nprm	$$⊢\neg 1\in \mathbb{P}$$
2		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
3	2	nnnn0d	$$⊢P\in \mathbb{P}\to P\in {\mathbb{N}}_0$$
4		dvds1	$$⊢P\in {\mathbb{N}}_0\to \left(P\parallel 1\leftrightarrow P=1\right)$$
5	3 4	syl	$$⊢P\in \mathbb{P}\to \left(P\parallel 1\leftrightarrow P=1\right)$$
6		eleq1	$$⊢P=1\to \left(P\in \mathbb{P}\leftrightarrow 1\in \mathbb{P}\right)$$
7	6	biimpcd	$$⊢P\in \mathbb{P}\to \left(P=1\to 1\in \mathbb{P}\right)$$
8	5 7	sylbid	$$⊢P\in \mathbb{P}\to \left(P\parallel 1\to 1\in \mathbb{P}\right)$$
9	1 8	mtoi	$$⊢P\in \mathbb{P}\to \neg P\parallel 1$$