Metamath Proof Explorer

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 ⊢ 𝑁 ∈ ℕ
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 ⊢ 𝑁 ∈ ℙ