Theorem prmlem2

Description: Our last proving session got as far as 25 because we started with the two "bootstrap" primes 2 and 3, and the next prime is 5, so knowing that 2 and 3 are prime and 4 is not allows us to cover the numbers less than 5 ^ 2 = 2 5 . Additionally, nonprimes are "easy", so we can extend this range of known prime/nonprimes all the way until 29, which is the first prime larger than 25. Thus, in this lemma we extend another blanket out to 2 9 ^ 2 = 8 4 1 , from which we can prove even more primes. If we wanted, we could keep doing this, but the goal is Bertrand's postulate, and for that we only need a few large primes - we don't need to find them all, as we have been doing thus far. So after this blanket runs out, we'll have to switch to another method (see 1259prm ).

As a side note, you can see the pattern of the primes in the indentation pattern of this lemma! (Contributed by Mario Carneiro, 18-Feb-2014) (Proof shortened by Mario Carneiro, 20-Apr-2015)

	Ref	Expression
Hypotheses	prmlem2.n	$$⊢N\in \mathbb{N}$$
	prmlem2.lt	$$⊢N<841$$
	prmlem2.gt	$$⊢1<N$$
	prmlem2.2	$$⊢\neg 2\parallel N$$
	prmlem2.3	$$⊢\neg 3\parallel N$$
	prmlem2.5	$$⊢\neg 5\parallel N$$
	prmlem2.7	$$⊢\neg 7\parallel N$$
	prmlem2.11	$$⊢\neg 11\parallel N$$
	prmlem2.13	$$⊢\neg 13\parallel N$$
	prmlem2.17	$$⊢\neg 17\parallel N$$
	prmlem2.19	$$⊢\neg 19\parallel N$$
	prmlem2.23	$$⊢\neg 23\parallel N$$
Assertion	prmlem2	$$⊢N\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		prmlem2.n	$$⊢N\in \mathbb{N}$$
2		prmlem2.lt	$$⊢N<841$$
3		prmlem2.gt	$$⊢1<N$$
4		prmlem2.2	$$⊢\neg 2\parallel N$$
5		prmlem2.3	$$⊢\neg 3\parallel N$$
6		prmlem2.5	$$⊢\neg 5\parallel N$$
7		prmlem2.7	$$⊢\neg 7\parallel N$$
8		prmlem2.11	$$⊢\neg 11\parallel N$$
9		prmlem2.13	$$⊢\neg 13\parallel N$$
10		prmlem2.17	$$⊢\neg 17\parallel N$$
11		prmlem2.19	$$⊢\neg 19\parallel N$$
12		prmlem2.23	$$⊢\neg 23\parallel N$$
13		eluzelre	$$⊢x\in {\mathbb{Z}}_{\ge 29}\to x\in ℝ$$
14	13	resqcld	$$⊢x\in {\mathbb{Z}}_{\ge 29}\to x^2\in ℝ$$
15		eluzle	$$⊢x\in {\mathbb{Z}}_{\ge 29}\to 29\le x$$
16		2nn0	$$⊢2\in {\mathbb{N}}_0$$
17		9nn0	$$⊢9\in {\mathbb{N}}_0$$
18	16 17	deccl	$$⊢29\in {\mathbb{N}}_0$$
19	18	nn0rei	$$⊢29\in ℝ$$
20	18	nn0ge0i	$$⊢0\le 29$$
21		le2sq2	$$⊢\left(\left(29\in ℝ\wedge 0\le 29\right)\wedge \left(x\in ℝ\wedge 29\le x\right)\right)\to {29}^2\le x^2$$
22	19 20 21	mpanl12	$$⊢\left(x\in ℝ\wedge 29\le x\right)\to {29}^2\le x^2$$
23	13 15 22	syl2anc	$$⊢x\in {\mathbb{Z}}_{\ge 29}\to {29}^2\le x^2$$
24	1	nnrei	$$⊢N\in ℝ$$
25	19	resqcli	$$⊢{29}^2\in ℝ$$
26	18	nn0cni	$$⊢29\in ℂ$$
27	26	sqvali	$$⊢{29}^2=29\cdot 29$$
28		eqid	$$⊢29=29$$
29		1nn0	$$⊢1\in {\mathbb{N}}_0$$
30		6nn0	$$⊢6\in {\mathbb{N}}_0$$
31	16 30	deccl	$$⊢26\in {\mathbb{N}}_0$$
32		5nn0	$$⊢5\in {\mathbb{N}}_0$$
33		8nn0	$$⊢8\in {\mathbb{N}}_0$$
34	26	2timesi	$$⊢2\cdot 29=29+29$$
35		2p2e4	$$⊢2+2=4$$
36	35	oveq1i	$$⊢2+2+1=4+1$$
37		4p1e5	$$⊢4+1=5$$
38	36 37	eqtri	$$⊢2+2+1=5$$
39		9p9e18	$$⊢9+9=18$$
40	16 17 16 17 28 28 38 33 39	decaddc	$$⊢29+29=58$$
41	34 40	eqtri	$$⊢2\cdot 29=58$$
42		eqid	$$⊢26=26$$
43		5p2e7	$$⊢5+2=7$$
44	43	oveq1i	$$⊢5+2+1=7+1$$
45		7p1e8	$$⊢7+1=8$$
46	44 45	eqtri	$$⊢5+2+1=8$$
47		4nn0	$$⊢4\in {\mathbb{N}}_0$$
48		8p6e14	$$⊢8+6=14$$
49	32 33 16 30 41 42 46 47 48	decaddc	$$⊢2\cdot 29+26=84$$
50		9t2e18	$$⊢9\cdot 2=18$$
51		1p1e2	$$⊢1+1=2$$
52		8p8e16	$$⊢8+8=16$$
53	29 33 33 50 51 30 52	decaddci	$$⊢9\cdot 2+8=26$$
54		9t9e81	$$⊢9\cdot 9=81$$
55	17 16 17 28 29 33 53 54	decmul2c	$$⊢9\cdot 29=261$$
56	18 16 17 28 29 31 49 55	decmul1c	$$⊢29\cdot 29=841$$
57	27 56	eqtri	$$⊢{29}^2=841$$
58	2 57	breqtrri	$$⊢N<{29}^2$$
59		ltletr	$$⊢\left(N\in ℝ\wedge {29}^2\in ℝ\wedge x^2\in ℝ\right)\to \left(\left(N<{29}^2\wedge {29}^2\le x^2\right)\to N<x^2\right)$$
60	58 59	mpani	$$⊢\left(N\in ℝ\wedge {29}^2\in ℝ\wedge x^2\in ℝ\right)\to \left({29}^2\le x^2\to N<x^2\right)$$
61	24 25 60	mp3an12	$$⊢x^2\in ℝ\to \left({29}^2\le x^2\to N<x^2\right)$$
62	14 23 61	sylc	$$⊢x\in {\mathbb{Z}}_{\ge 29}\to N<x^2$$
63		ltnle	$$⊢\left(N\in ℝ\wedge x^2\in ℝ\right)\to \left(N<x^2\leftrightarrow \neg x^2\le N\right)$$
64	24 14 63	sylancr	$$⊢x\in {\mathbb{Z}}_{\ge 29}\to \left(N<x^2\leftrightarrow \neg x^2\le N\right)$$
65	62 64	mpbid	$$⊢x\in {\mathbb{Z}}_{\ge 29}\to \neg x^2\le N$$
66	65	pm2.21d	$$⊢x\in {\mathbb{Z}}_{\ge 29}\to \left(x^2\le N\to \neg x\parallel N\right)$$
67	66	adantld	$$⊢x\in {\mathbb{Z}}_{\ge 29}\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)$$
68	67	adantl	$$⊢\left(\neg 2\parallel 29\wedge x\in {\mathbb{Z}}_{\ge 29}\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)$$
69		9nn	$$⊢9\in \mathbb{N}$$
70		3nn	$$⊢3\in \mathbb{N}$$
71		1lt9	$$⊢1<9$$
72		1lt3	$$⊢1<3$$
73		9t3e27	$$⊢9\cdot 3=27$$
74	69 70 71 72 73	nprmi	$$⊢\neg 27\in \mathbb{P}$$
75	74	pm2.21i	$$⊢27\in \mathbb{P}\to \neg 27\parallel N$$
76		7nn0	$$⊢7\in {\mathbb{N}}_0$$
77		eqid	$$⊢27=27$$
78		7p2e9	$$⊢7+2=9$$
79	16 76 16 77 78	decaddi	$$⊢27+2=29$$
80	68 75 79	prmlem0	$$⊢\left(\neg 2\parallel 27\wedge x\in {\mathbb{Z}}_{\ge 27}\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)$$
81		5nn	$$⊢5\in \mathbb{N}$$
82		1lt5	$$⊢1<5$$
83		5t5e25	$$⊢5\cdot 5=25$$
84	81 81 82 82 83	nprmi	$$⊢\neg 25\in \mathbb{P}$$
85	84	pm2.21i	$$⊢25\in \mathbb{P}\to \neg 25\parallel N$$
86		eqid	$$⊢25=25$$
87	16 32 16 86 43	decaddi	$$⊢25+2=27$$
88	80 85 87	prmlem0	$$⊢\left(\neg 2\parallel 25\wedge x\in {\mathbb{Z}}_{\ge 25}\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)$$
89	12	a1i	$$⊢23\in \mathbb{P}\to \neg 23\parallel N$$
90		3nn0	$$⊢3\in {\mathbb{N}}_0$$
91		eqid	$$⊢23=23$$
92		3p2e5	$$⊢3+2=5$$
93	16 90 16 91 92	decaddi	$$⊢23+2=25$$
94	88 89 93	prmlem0	$$⊢\left(\neg 2\parallel 23\wedge x\in {\mathbb{Z}}_{\ge 23}\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)$$
95		7nn	$$⊢7\in \mathbb{N}$$
96		1lt7	$$⊢1<7$$
97		7t3e21	$$⊢7\cdot 3=21$$
98	95 70 96 72 97	nprmi	$$⊢\neg 21\in \mathbb{P}$$
99	98	pm2.21i	$$⊢21\in \mathbb{P}\to \neg 21\parallel N$$
100		eqid	$$⊢21=21$$
101		1p2e3	$$⊢1+2=3$$
102	16 29 16 100 101	decaddi	$$⊢21+2=23$$
103	94 99 102	prmlem0	$$⊢\left(\neg 2\parallel 21\wedge x\in {\mathbb{Z}}_{\ge 21}\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)$$
104	11	a1i	$$⊢19\in \mathbb{P}\to \neg 19\parallel N$$
105		eqid	$$⊢19=19$$
106		9p2e11	$$⊢9+2=11$$
107	29 17 16 105 51 29 106	decaddci	$$⊢19+2=21$$
108	103 104 107	prmlem0	$$⊢\left(\neg 2\parallel 19\wedge x\in {\mathbb{Z}}_{\ge 19}\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)$$
109	10	a1i	$$⊢17\in \mathbb{P}\to \neg 17\parallel N$$
110		eqid	$$⊢17=17$$
111	29 76 16 110 78	decaddi	$$⊢17+2=19$$
112	108 109 111	prmlem0	$$⊢\left(\neg 2\parallel 17\wedge x\in {\mathbb{Z}}_{\ge 17}\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)$$
113		5t3e15	$$⊢5\cdot 3=15$$
114	81 70 82 72 113	nprmi	$$⊢\neg 15\in \mathbb{P}$$
115	114	pm2.21i	$$⊢15\in \mathbb{P}\to \neg 15\parallel N$$
116		eqid	$$⊢15=15$$
117	29 32 16 116 43	decaddi	$$⊢15+2=17$$
118	112 115 117	prmlem0	$$⊢\left(\neg 2\parallel 15\wedge x\in {\mathbb{Z}}_{\ge 15}\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)$$
119	9	a1i	$$⊢13\in \mathbb{P}\to \neg 13\parallel N$$
120		eqid	$$⊢13=13$$
121	29 90 16 120 92	decaddi	$$⊢13+2=15$$
122	118 119 121	prmlem0	$$⊢\left(\neg 2\parallel 13\wedge x\in {\mathbb{Z}}_{\ge 13}\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)$$
123	8	a1i	$$⊢11\in \mathbb{P}\to \neg 11\parallel N$$
124		eqid	$$⊢11=11$$
125	29 29 16 124 101	decaddi	$$⊢11+2=13$$
126	122 123 125	prmlem0	$$⊢\left(\neg 2\parallel 11\wedge x\in {\mathbb{Z}}_{\ge 11}\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)$$
127		9nprm	$$⊢\neg 9\in \mathbb{P}$$
128	127	pm2.21i	$$⊢9\in \mathbb{P}\to \neg 9\parallel N$$
129	126 128 106	prmlem0	$$⊢\left(\neg 2\parallel 9\wedge x\in {\mathbb{Z}}_{\ge 9}\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)$$
130	7	a1i	$$⊢7\in \mathbb{P}\to \neg 7\parallel N$$
131	129 130 78	prmlem0	$$⊢\left(\neg 2\parallel 7\wedge x\in {\mathbb{Z}}_{\ge 7}\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)$$
132	6	a1i	$$⊢5\in \mathbb{P}\to \neg 5\parallel N$$
133	131 132 43	prmlem0	$$⊢\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)$$
134	1 3 4 5 133	prmlem1a	$$⊢N\in \mathbb{P}$$