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 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	⊢ 𝑁 ∈ ℕ
	prmlem2.lt	⊢ 𝑁 < ; ; 8 4 1
	prmlem2.gt	⊢ 1 < 𝑁
	prmlem2.2	⊢ ¬ 2 ∥ 𝑁
	prmlem2.3	⊢ ¬ 3 ∥ 𝑁
	prmlem2.5	⊢ ¬ 5 ∥ 𝑁
	prmlem2.7	⊢ ¬ 7 ∥ 𝑁
	prmlem2.11	⊢ ¬ ; 1 1 ∥ 𝑁
	prmlem2.13	⊢ ¬ ; 1 3 ∥ 𝑁
	prmlem2.17	⊢ ¬ ; 1 7 ∥ 𝑁
	prmlem2.19	⊢ ¬ ; 1 9 ∥ 𝑁
	prmlem2.23	⊢ ¬ ; 2 3 ∥ 𝑁
Assertion	prmlem2	⊢ 𝑁 ∈ ℙ

Proof

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