Theorem prmlem1a

Description: Lemma for prmlem1 and prmlem2 . (Contributed by Mario Carneiro, 18-Feb-2014)

	Ref	Expression
Hypotheses	prmlem1.n	$$⊢N\in \mathbb{N}$$
	prmlem1.gt	$$⊢1<N$$
	prmlem1.2	$$⊢\neg 2\parallel N$$
	prmlem1.3	$$⊢\neg 3\parallel N$$
	prmlem1a.x	$$⊢\left(\neg 2\parallel 5\wedge x\in {\mathbb{Z}}_{\ge 5}\right)\to \left(\left(x\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\wedge x^2\le N\right)\to \neg x\parallel N\right)$$
Assertion	prmlem1a	$$⊢N\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		prmlem1.n	$$⊢N\in \mathbb{N}$$
2		prmlem1.gt	$$⊢1<N$$
3		prmlem1.2	$$⊢\neg 2\parallel N$$
4		prmlem1.3	$$⊢\neg 3\parallel N$$
5		prmlem1a.x	$$⊢\left(\neg 2\parallel 5\wedge x\in {\mathbb{Z}}_{\ge 5}\right)\to \left(\left(x\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\wedge x^2\le N\right)\to \neg x\parallel N\right)$$
6		eluz2b2	$$⊢N\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(N\in \mathbb{N}\wedge 1<N\right)$$
7	1 2 6	mpbir2an	$$⊢N\in {\mathbb{Z}}_{\ge 2}$$
8		breq1	$$⊢x=2\to \left(x\parallel N\leftrightarrow 2\parallel N\right)$$
9	8	notbid	$$⊢x=2\to \left(\neg x\parallel N\leftrightarrow \neg 2\parallel N\right)$$
10	9	imbi2d	$$⊢x=2\to \left(\left(x^2\le N\to \neg x\parallel N\right)\leftrightarrow \left(x^2\le N\to \neg 2\parallel N\right)\right)$$
11		prmnn	$$⊢x\in \mathbb{P}\to x\in \mathbb{N}$$
12	11	adantr	$$⊢\left(x\in \mathbb{P}\wedge x\ne 2\right)\to x\in \mathbb{N}$$
13		eldifsn	$$⊢x\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\leftrightarrow \left(x\in \mathbb{P}\wedge x\ne 2\right)$$
14		n2dvds1	$$⊢\neg 2\parallel 1$$
15	4	a1i	$$⊢3\in \mathbb{P}\to \neg 3\parallel N$$
16		3p2e5	$$⊢3+2=5$$
17	5 15 16	prmlem0	$$⊢\left(\neg 2\parallel 3\wedge x\in {\mathbb{Z}}_{\ge 3}\right)\to \left(\left(x\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\wedge x^2\le N\right)\to \neg x\parallel N\right)$$
18		1nprm	$$⊢\neg 1\in \mathbb{P}$$
19	18	pm2.21i	$$⊢1\in \mathbb{P}\to \neg 1\parallel N$$
20		1p2e3	$$⊢1+2=3$$
21	17 19 20	prmlem0	$$⊢\left(\neg 2\parallel 1\wedge x\in {\mathbb{Z}}_{\ge 1}\right)\to \left(\left(x\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\wedge x^2\le N\right)\to \neg x\parallel N\right)$$
22	14 21	mpan	$$⊢x\in {\mathbb{Z}}_{\ge 1}\to \left(\left(x\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\wedge x^2\le N\right)\to \neg x\parallel N\right)$$
23		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
24	22 23	eleq2s	$$⊢x\in \mathbb{N}\to \left(\left(x\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\wedge x^2\le N\right)\to \neg x\parallel N\right)$$
25	24	expd	$$⊢x\in \mathbb{N}\to \left(x\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to \left(x^2\le N\to \neg x\parallel N\right)\right)$$
26	13 25	biimtrrid	$$⊢x\in \mathbb{N}\to \left(\left(x\in \mathbb{P}\wedge x\ne 2\right)\to \left(x^2\le N\to \neg x\parallel N\right)\right)$$
27	12 26	mpcom	$$⊢\left(x\in \mathbb{P}\wedge x\ne 2\right)\to \left(x^2\le N\to \neg x\parallel N\right)$$
28	3	2a1i	$$⊢x\in \mathbb{P}\to \left(x^2\le N\to \neg 2\parallel N\right)$$
29	10 27 28	pm2.61ne	$$⊢x\in \mathbb{P}\to \left(x^2\le N\to \neg x\parallel N\right)$$
30	29	rgen	$$⊢\forall x\in \mathbb{P}\left(x^2\le N\to \neg x\parallel N\right)$$
31		isprm5	$$⊢N\in \mathbb{P}\leftrightarrow \left(N\in {\mathbb{Z}}_{\ge 2}\wedge \forall x\in \mathbb{P}\left(x^2\le N\to \neg x\parallel N\right)\right)$$
32	7 30 31	mpbir2an	$$⊢N\in \mathbb{P}$$