Theorem 1nprm

Description: 1 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011) (Proof shortened by Fan Zheng, 3-Jul-2016)

	Ref	Expression
Assertion	1nprm	$$⊢\neg 1\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		1nn	$$⊢1\in \mathbb{N}$$
2		eleq1	$$⊢z=1\to \left(z\in \mathbb{N}\leftrightarrow 1\in \mathbb{N}\right)$$
3	1 2	mpbiri	$$⊢z=1\to z\in \mathbb{N}$$
4		nnnn0	$$⊢z\in \mathbb{N}\to z\in {\mathbb{N}}_0$$
5		dvds1	$$⊢z\in {\mathbb{N}}_0\to \left(z\parallel 1\leftrightarrow z=1\right)$$
6	4 5	syl	$$⊢z\in \mathbb{N}\to \left(z\parallel 1\leftrightarrow z=1\right)$$
7	6	bicomd	$$⊢z\in \mathbb{N}\to \left(z=1\leftrightarrow z\parallel 1\right)$$
8	3 7	biadanii	$$⊢z=1\leftrightarrow \left(z\in \mathbb{N}\wedge z\parallel 1\right)$$
9		velsn	$$⊢z\in \left\{1\right\}\leftrightarrow z=1$$
10		breq1	$$⊢n=z\to \left(n\parallel 1\leftrightarrow z\parallel 1\right)$$
11	10	elrab	$$⊢z\in \left\{n\in \mathbb{N}|n\parallel 1\right\}\leftrightarrow \left(z\in \mathbb{N}\wedge z\parallel 1\right)$$
12	8 9 11	3bitr4ri	$$⊢z\in \left\{n\in \mathbb{N}|n\parallel 1\right\}\leftrightarrow z\in \left\{1\right\}$$
13	12	eqriv	$$⊢\left\{n\in \mathbb{N}|n\parallel 1\right\}=\left\{1\right\}$$
14		1ex	$$⊢1\in \mathrm{V}$$
15	14	ensn1	$$⊢\left\{1\right\}\approx 1_{𝑜}$$
16	13 15	eqbrtri	$$⊢\left\{n\in \mathbb{N}|n\parallel 1\right\}\approx 1_{𝑜}$$
17		1sdom2	$$⊢1_{𝑜}\prec 2_{𝑜}$$
18		ensdomtr	$$⊢\left(\left\{n\in \mathbb{N}|n\parallel 1\right\}\approx 1_{𝑜}\wedge 1_{𝑜}\prec 2_{𝑜}\right)\to \left\{n\in \mathbb{N}|n\parallel 1\right\}\prec 2_{𝑜}$$
19	16 17 18	mp2an	$$⊢\left\{n\in \mathbb{N}|n\parallel 1\right\}\prec 2_{𝑜}$$
20		sdomnen	$$⊢\left\{n\in \mathbb{N}|n\parallel 1\right\}\prec 2_{𝑜}\to \neg \left\{n\in \mathbb{N}|n\parallel 1\right\}\approx 2_{𝑜}$$
21	19 20	ax-mp	$$⊢\neg \left\{n\in \mathbb{N}|n\parallel 1\right\}\approx 2_{𝑜}$$
22		isprm	$$⊢1\in \mathbb{P}\leftrightarrow \left(1\in \mathbb{N}\wedge \left\{n\in \mathbb{N}|n\parallel 1\right\}\approx 2_{𝑜}\right)$$
23	1 22	mpbiran	$$⊢1\in \mathbb{P}\leftrightarrow \left\{n\in \mathbb{N}|n\parallel 1\right\}\approx 2_{𝑜}$$
24	21 23	mtbir	$$⊢\neg 1\in \mathbb{P}$$