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 
|- N e. NN
prmlem2.lt 
|- N < ; ; 8 4 1
prmlem2.gt 
|- 1 < N
prmlem2.2 
|- -. 2 || N
prmlem2.3 
|- -. 3 || N
prmlem2.5 
|- -. 5 || N
prmlem2.7 
|- -. 7 || N
prmlem2.11 
|- -. ; 1 1 || N
prmlem2.13 
|- -. ; 1 3 || N
prmlem2.17 
|- -. ; 1 7 || N
prmlem2.19 
|- -. ; 1 9 || N
prmlem2.23 
|- -. ; 2 3 || N
Assertion prmlem2 
|- N e. Prime

Proof

Step Hyp Ref Expression
1 prmlem2.n 
 |-  N e. NN
2 prmlem2.lt 
 |-  N < ; ; 8 4 1
3 prmlem2.gt 
 |-  1 < N
4 prmlem2.2 
 |-  -. 2 || N
5 prmlem2.3 
 |-  -. 3 || N
6 prmlem2.5 
 |-  -. 5 || N
7 prmlem2.7 
 |-  -. 7 || N
8 prmlem2.11 
 |-  -. ; 1 1 || N
9 prmlem2.13 
 |-  -. ; 1 3 || N
10 prmlem2.17 
 |-  -. ; 1 7 || N
11 prmlem2.19 
 |-  -. ; 1 9 || N
12 prmlem2.23 
 |-  -. ; 2 3 || N
13 eluzelre 
 |-  ( x e. ( ZZ>= ` ; 2 9 ) -> x e. RR )
14 13 resqcld 
 |-  ( x e. ( ZZ>= ` ; 2 9 ) -> ( x ^ 2 ) e. RR )
15 eluzle 
 |-  ( x e. ( ZZ>= ` ; 2 9 ) -> ; 2 9 <_ x )
16 2nn0 
 |-  2 e. NN0
17 9nn0 
 |-  9 e. NN0
18 16 17 deccl 
 |-  ; 2 9 e. NN0
19 18 nn0rei 
 |-  ; 2 9 e. RR
20 18 nn0ge0i 
 |-  0 <_ ; 2 9
21 le2sq2 
 |-  ( ( ( ; 2 9 e. RR /\ 0 <_ ; 2 9 ) /\ ( x e. RR /\ ; 2 9 <_ x ) ) -> ( ; 2 9 ^ 2 ) <_ ( x ^ 2 ) )
22 19 20 21 mpanl12 
 |-  ( ( x e. RR /\ ; 2 9 <_ x ) -> ( ; 2 9 ^ 2 ) <_ ( x ^ 2 ) )
23 13 15 22 syl2anc 
 |-  ( x e. ( ZZ>= ` ; 2 9 ) -> ( ; 2 9 ^ 2 ) <_ ( x ^ 2 ) )
24 1 nnrei 
 |-  N e. RR
25 19 resqcli 
 |-  ( ; 2 9 ^ 2 ) e. RR
26 18 nn0cni 
 |-  ; 2 9 e. CC
27 26 sqvali 
 |-  ( ; 2 9 ^ 2 ) = ( ; 2 9 x. ; 2 9 )
28 eqid 
 |-  ; 2 9 = ; 2 9
29 1nn0 
 |-  1 e. NN0
30 6nn0 
 |-  6 e. NN0
31 16 30 deccl 
 |-  ; 2 6 e. NN0
32 5nn0 
 |-  5 e. NN0
33 8nn0 
 |-  8 e. NN0
34 26 2timesi 
 |-  ( 2 x. ; 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 x. ; 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 e. NN0
48 8p6e14 
 |-  ( 8 + 6 ) = ; 1 4
49 32 33 16 30 41 42 46 47 48 decaddc 
 |-  ( ( 2 x. ; 2 9 ) + ; 2 6 ) = ; 8 4
50 9t2e18 
 |-  ( 9 x. 2 ) = ; 1 8
51 1p1e2 
 |-  ( 1 + 1 ) = 2
52 8p8e16 
 |-  ( 8 + 8 ) = ; 1 6
53 29 33 33 50 51 30 52 decaddci 
 |-  ( ( 9 x. 2 ) + 8 ) = ; 2 6
54 9t9e81 
 |-  ( 9 x. 9 ) = ; 8 1
55 17 16 17 28 29 33 53 54 decmul2c 
 |-  ( 9 x. ; 2 9 ) = ; ; 2 6 1
56 18 16 17 28 29 31 49 55 decmul1c 
 |-  ( ; 2 9 x. ; 2 9 ) = ; ; 8 4 1
57 27 56 eqtri 
 |-  ( ; 2 9 ^ 2 ) = ; ; 8 4 1
58 2 57 breqtrri 
 |-  N < ( ; 2 9 ^ 2 )
59 ltletr 
 |-  ( ( N e. RR /\ ( ; 2 9 ^ 2 ) e. RR /\ ( x ^ 2 ) e. RR ) -> ( ( N < ( ; 2 9 ^ 2 ) /\ ( ; 2 9 ^ 2 ) <_ ( x ^ 2 ) ) -> N < ( x ^ 2 ) ) )
60 58 59 mpani 
 |-  ( ( N e. RR /\ ( ; 2 9 ^ 2 ) e. RR /\ ( x ^ 2 ) e. RR ) -> ( ( ; 2 9 ^ 2 ) <_ ( x ^ 2 ) -> N < ( x ^ 2 ) ) )
61 24 25 60 mp3an12 
 |-  ( ( x ^ 2 ) e. RR -> ( ( ; 2 9 ^ 2 ) <_ ( x ^ 2 ) -> N < ( x ^ 2 ) ) )
62 14 23 61 sylc 
 |-  ( x e. ( ZZ>= ` ; 2 9 ) -> N < ( x ^ 2 ) )
63 ltnle 
 |-  ( ( N e. RR /\ ( x ^ 2 ) e. RR ) -> ( N < ( x ^ 2 ) <-> -. ( x ^ 2 ) <_ N ) )
64 24 14 63 sylancr 
 |-  ( x e. ( ZZ>= ` ; 2 9 ) -> ( N < ( x ^ 2 ) <-> -. ( x ^ 2 ) <_ N ) )
65 62 64 mpbid 
 |-  ( x e. ( ZZ>= ` ; 2 9 ) -> -. ( x ^ 2 ) <_ N )
66 65 pm2.21d 
 |-  ( x e. ( ZZ>= ` ; 2 9 ) -> ( ( x ^ 2 ) <_ N -> -. x || N ) )
67 66 adantld 
 |-  ( x e. ( ZZ>= ` ; 2 9 ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
68 67 adantl 
 |-  ( ( -. 2 || ; 2 9 /\ x e. ( ZZ>= ` ; 2 9 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
69 9nn 
 |-  9 e. NN
70 3nn 
 |-  3 e. NN
71 1lt9 
 |-  1 < 9
72 1lt3 
 |-  1 < 3
73 9t3e27 
 |-  ( 9 x. 3 ) = ; 2 7
74 69 70 71 72 73 nprmi 
 |-  -. ; 2 7 e. Prime
75 74 pm2.21i 
 |-  ( ; 2 7 e. Prime -> -. ; 2 7 || N )
76 7nn0 
 |-  7 e. NN0
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 /\ x e. ( ZZ>= ` ; 2 7 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
81 5nn 
 |-  5 e. NN
82 1lt5 
 |-  1 < 5
83 5t5e25 
 |-  ( 5 x. 5 ) = ; 2 5
84 81 81 82 82 83 nprmi 
 |-  -. ; 2 5 e. Prime
85 84 pm2.21i 
 |-  ( ; 2 5 e. Prime -> -. ; 2 5 || N )
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 /\ x e. ( ZZ>= ` ; 2 5 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
89 12 a1i 
 |-  ( ; 2 3 e. Prime -> -. ; 2 3 || N )
90 3nn0 
 |-  3 e. NN0
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 /\ x e. ( ZZ>= ` ; 2 3 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
95 7nn 
 |-  7 e. NN
96 1lt7 
 |-  1 < 7
97 7t3e21 
 |-  ( 7 x. 3 ) = ; 2 1
98 95 70 96 72 97 nprmi 
 |-  -. ; 2 1 e. Prime
99 98 pm2.21i 
 |-  ( ; 2 1 e. Prime -> -. ; 2 1 || N )
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 /\ x e. ( ZZ>= ` ; 2 1 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
104 11 a1i 
 |-  ( ; 1 9 e. Prime -> -. ; 1 9 || N )
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 /\ x e. ( ZZ>= ` ; 1 9 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
109 10 a1i 
 |-  ( ; 1 7 e. Prime -> -. ; 1 7 || N )
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 /\ x e. ( ZZ>= ` ; 1 7 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
113 5t3e15 
 |-  ( 5 x. 3 ) = ; 1 5
114 81 70 82 72 113 nprmi 
 |-  -. ; 1 5 e. Prime
115 114 pm2.21i 
 |-  ( ; 1 5 e. Prime -> -. ; 1 5 || N )
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 /\ x e. ( ZZ>= ` ; 1 5 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
119 9 a1i 
 |-  ( ; 1 3 e. Prime -> -. ; 1 3 || N )
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 /\ x e. ( ZZ>= ` ; 1 3 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
123 8 a1i 
 |-  ( ; 1 1 e. Prime -> -. ; 1 1 || N )
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 /\ x e. ( ZZ>= ` ; 1 1 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
127 9nprm 
 |-  -. 9 e. Prime
128 127 pm2.21i 
 |-  ( 9 e. Prime -> -. 9 || N )
129 126 128 106 prmlem0 
 |-  ( ( -. 2 || 9 /\ x e. ( ZZ>= ` 9 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
130 7 a1i 
 |-  ( 7 e. Prime -> -. 7 || N )
131 129 130 78 prmlem0 
 |-  ( ( -. 2 || 7 /\ x e. ( ZZ>= ` 7 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
132 6 a1i 
 |-  ( 5 e. Prime -> -. 5 || N )
133 131 132 43 prmlem0 
 |-  ( ( -. 2 || 5 /\ x e. ( ZZ>= ` 5 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
134 1 3 4 5 133 prmlem1a 
 |-  N e. Prime