Theorem prmlem1

Description: A quick proof skeleton to show that the numbers less than 25 are prime, by trial division. (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$$
	prmlem1.lt	$$⊢N<25$$
Assertion	prmlem1	$$⊢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		prmlem1.lt	$$⊢N<25$$
6		eluzelre	$$⊢x\in {\mathbb{Z}}_{\ge 5}\to x\in ℝ$$
7	6	resqcld	$$⊢x\in {\mathbb{Z}}_{\ge 5}\to x^2\in ℝ$$
8		eluzle	$$⊢x\in {\mathbb{Z}}_{\ge 5}\to 5\le x$$
9		5re	$$⊢5\in ℝ$$
10		5nn0	$$⊢5\in {\mathbb{N}}_0$$
11	10	nn0ge0i	$$⊢0\le 5$$
12		le2sq2	$$⊢\left(\left(5\in ℝ\wedge 0\le 5\right)\wedge \left(x\in ℝ\wedge 5\le x\right)\right)\to 5^2\le x^2$$
13	9 11 12	mpanl12	$$⊢\left(x\in ℝ\wedge 5\le x\right)\to 5^2\le x^2$$
14	6 8 13	syl2anc	$$⊢x\in {\mathbb{Z}}_{\ge 5}\to 5^2\le x^2$$
15	1	nnrei	$$⊢N\in ℝ$$
16	9	resqcli	$$⊢5^2\in ℝ$$
17		5cn	$$⊢5\in ℂ$$
18	17	sqvali	$$⊢5^2=5\cdot 5$$
19		5t5e25	$$⊢5\cdot 5=25$$
20	18 19	eqtri	$$⊢5^2=25$$
21	5 20	breqtrri	$$⊢N<5^2$$
22		ltletr	$$⊢\left(N\in ℝ\wedge 5^2\in ℝ\wedge x^2\in ℝ\right)\to \left(\left(N<5^2\wedge 5^2\le x^2\right)\to N<x^2\right)$$
23	21 22	mpani	$$⊢\left(N\in ℝ\wedge 5^2\in ℝ\wedge x^2\in ℝ\right)\to \left(5^2\le x^2\to N<x^2\right)$$
24	15 16 23	mp3an12	$$⊢x^2\in ℝ\to \left(5^2\le x^2\to N<x^2\right)$$
25	7 14 24	sylc	$$⊢x\in {\mathbb{Z}}_{\ge 5}\to N<x^2$$
26		ltnle	$$⊢\left(N\in ℝ\wedge x^2\in ℝ\right)\to \left(N<x^2\leftrightarrow \neg x^2\le N\right)$$
27	15 7 26	sylancr	$$⊢x\in {\mathbb{Z}}_{\ge 5}\to \left(N<x^2\leftrightarrow \neg x^2\le N\right)$$
28	25 27	mpbid	$$⊢x\in {\mathbb{Z}}_{\ge 5}\to \neg x^2\le N$$
29	28	pm2.21d	$$⊢x\in {\mathbb{Z}}_{\ge 5}\to \left(x^2\le N\to \neg x\parallel N\right)$$
30	29	adantld	$$⊢x\in {\mathbb{Z}}_{\ge 5}\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)$$
31	30	adantl	$$⊢\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)$$
32	1 2 3 4 31	prmlem1a	$$⊢N\in \mathbb{P}$$