Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  prmlem2 Structured version   Unicode version

Theorem prmlem2 13447
 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 . 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 , 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 13460). 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.)
Hypotheses
Ref Expression
prmlem2.n
prmlem2.lt ;;
prmlem2.gt
prmlem2.2
prmlem2.3
prmlem2.5
prmlem2.7
prmlem2.11 ;
prmlem2.13 ;
prmlem2.17 ;
prmlem2.19 ;
prmlem2.23 ;
Assertion
Ref Expression
prmlem2

Proof of Theorem prmlem2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 prmlem2.n . 2
2 prmlem2.gt . 2
3 prmlem2.2 . 2
4 prmlem2.3 . 2
5 eluzelre 10502 . . . . . . . . . . . . . . . . . . . 20 ;
65resqcld 11554 . . . . . . . . . . . . . . . . . . 19 ;
7 eluzle 10503 . . . . . . . . . . . . . . . . . . . 20 ; ;
8 2nn0 10243 . . . . . . . . . . . . . . . . . . . . . . 23
9 9nn0 10250 . . . . . . . . . . . . . . . . . . . . . . 23
108, 9deccl 10401 . . . . . . . . . . . . . . . . . . . . . 22 ;
1110nn0rei 10237 . . . . . . . . . . . . . . . . . . . . 21 ;
1210nn0ge0i 10254 . . . . . . . . . . . . . . . . . . . . 21 ;
13 le2sq2 11462 . . . . . . . . . . . . . . . . . . . . 21 ; ; ; ;
1411, 12, 13mpanl12 665 . . . . . . . . . . . . . . . . . . . 20 ; ;
155, 7, 14syl2anc 644 . . . . . . . . . . . . . . . . . . 19 ; ;
161nnrei 10014 . . . . . . . . . . . . . . . . . . . 20
1711resqcli 11472 . . . . . . . . . . . . . . . . . . . 20 ;
18 prmlem2.lt . . . . . . . . . . . . . . . . . . . . . 22 ;;
1910nn0cni 10238 . . . . . . . . . . . . . . . . . . . . . . . 24 ;
2019sqvali 11466 . . . . . . . . . . . . . . . . . . . . . . 23 ; ; ;
21 eqid 2438 . . . . . . . . . . . . . . . . . . . . . . . 24 ; ;
22 1nn0 10242 . . . . . . . . . . . . . . . . . . . . . . . 24
23 6nn0 10247 . . . . . . . . . . . . . . . . . . . . . . . . 25
248, 23deccl 10401 . . . . . . . . . . . . . . . . . . . . . . . 24 ;
25 5nn0 10246 . . . . . . . . . . . . . . . . . . . . . . . . 25
26 8nn0 10249 . . . . . . . . . . . . . . . . . . . . . . . . 25
27192timesi 10106 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ; ; ;
28 2p2e4 10103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2928oveq1i 6094 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
30 4p1e5 10110 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3129, 30eqtri 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
32 9p9e18 10456 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ;
338, 9, 8, 9, 21, 21, 31, 26, 32decaddc 10429 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ; ; ;
3427, 33eqtri 2458 . . . . . . . . . . . . . . . . . . . . . . . . 25 ; ;
35 eqid 2438 . . . . . . . . . . . . . . . . . . . . . . . . 25 ; ;
36 5p2e7 10121 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3736oveq1i 6094 . . . . . . . . . . . . . . . . . . . . . . . . . 26
38 7p1e8 10113 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3937, 38eqtri 2458 . . . . . . . . . . . . . . . . . . . . . . . . 25
40 4nn0 10245 . . . . . . . . . . . . . . . . . . . . . . . . 25
41 8p6e14 10446 . . . . . . . . . . . . . . . . . . . . . . . . 25 ;
4225, 26, 8, 23, 34, 35, 39, 40, 41decaddc 10429 . . . . . . . . . . . . . . . . . . . . . . . 24 ; ; ;
43 9t2e18 10482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ;
44 1p1e2 10099 . . . . . . . . . . . . . . . . . . . . . . . . . 26
45 8p8e16 10448 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ;
4622, 26, 26, 43, 44, 23, 45decaddci 10432 . . . . . . . . . . . . . . . . . . . . . . . . 25 ;
47 9t9e81 10489 . . . . . . . . . . . . . . . . . . . . . . . . 25 ;
489, 8, 9, 21, 22, 26, 46, 47decmul2c 10435 . . . . . . . . . . . . . . . . . . . . . . . 24 ; ;;
4910, 8, 9, 21, 22, 24, 42, 48decmul1c 10434 . . . . . . . . . . . . . . . . . . . . . . 23 ; ; ;;
5020, 49eqtri 2458 . . . . . . . . . . . . . . . . . . . . . 22 ; ;;
5118, 50breqtrri 4240 . . . . . . . . . . . . . . . . . . . . 21 ;
52 ltletr 9171 . . . . . . . . . . . . . . . . . . . . 21 ; ; ;
5351, 52mpani 659 . . . . . . . . . . . . . . . . . . . 20 ; ;
5416, 17, 53mp3an12 1270 . . . . . . . . . . . . . . . . . . 19 ;
556, 15, 54sylc 59 . . . . . . . . . . . . . . . . . 18 ;
56 ltnle 9160 . . . . . . . . . . . . . . . . . . 19
5716, 6, 56sylancr 646 . . . . . . . . . . . . . . . . . 18 ;
5855, 57mpbid 203 . . . . . . . . . . . . . . . . 17 ;
5958pm2.21d 101 . . . . . . . . . . . . . . . 16 ;
6059adantld 455 . . . . . . . . . . . . . . 15 ;
6160adantl 454 . . . . . . . . . . . . . 14 ; ;
62 9nn 10145 . . . . . . . . . . . . . . . 16
63 3nn 10139 . . . . . . . . . . . . . . . 16
64 1lt9 10182 . . . . . . . . . . . . . . . 16
65 1lt3 10149 . . . . . . . . . . . . . . . 16
66 9t3e27 10483 . . . . . . . . . . . . . . . 16 ;
6762, 63, 64, 65, 66nprmi 13099 . . . . . . . . . . . . . . 15 ;
6867pm2.21i 126 . . . . . . . . . . . . . 14 ; ;
69 7nn0 10248 . . . . . . . . . . . . . . 15
70 eqid 2438 . . . . . . . . . . . . . . 15 ; ;
71 7p2e9 10128 . . . . . . . . . . . . . . 15
728, 69, 8, 70, 71decaddi 10431 . . . . . . . . . . . . . 14 ; ;
7361, 68, 72prmlem0 13433 . . . . . . . . . . . . 13 ; ;
74 5nn 10141 . . . . . . . . . . . . . . 15
75 1lt5 10156 . . . . . . . . . . . . . . 15
76 5t5e25 10463 . . . . . . . . . . . . . . 15 ;
7774, 74, 75, 75, 76nprmi 13099 . . . . . . . . . . . . . 14 ;
7877pm2.21i 126 . . . . . . . . . . . . 13 ; ;
79 eqid 2438 . . . . . . . . . . . . . 14 ; ;
808, 25, 8, 79, 36decaddi 10431 . . . . . . . . . . . . 13 ; ;
8173, 78, 80prmlem0 13433 . . . . . . . . . . . 12 ; ;
82 prmlem2.23 . . . . . . . . . . . . 13 ;
8382a1i 11 . . . . . . . . . . . 12 ; ;
84 3nn0 10244 . . . . . . . . . . . . 13
85 eqid 2438 . . . . . . . . . . . . 13 ; ;
86 3p2e5 10116 . . . . . . . . . . . . 13
878, 84, 8, 85, 86decaddi 10431 . . . . . . . . . . . 12 ; ;
8881, 83, 87prmlem0 13433 . . . . . . . . . . 11 ; ;
89 7nn 10143 . . . . . . . . . . . . 13
90 1lt7 10167 . . . . . . . . . . . . 13
91 7t3e21 10470 . . . . . . . . . . . . 13 ;
9289, 63, 90, 65, 91nprmi 13099 . . . . . . . . . . . 12 ;
9392pm2.21i 126 . . . . . . . . . . 11 ; ;
94 eqid 2438 . . . . . . . . . . . 12 ; ;
95 2cn 10075 . . . . . . . . . . . . 13
96 ax-1cn 9053 . . . . . . . . . . . . 13
97 2p1e3 10108 . . . . . . . . . . . . 13
9895, 96, 97addcomli 9263 . . . . . . . . . . . 12
998, 22, 8, 94, 98decaddi 10431 . . . . . . . . . . 11 ; ;
10088, 93, 99prmlem0 13433 . . . . . . . . . 10 ; ;
101 prmlem2.19 . . . . . . . . . . 11 ;
102101a1i 11 . . . . . . . . . 10 ; ;
103 eqid 2438 . . . . . . . . . . 11 ; ;
104 9p2e11 10449 . . . . . . . . . . 11 ;
10522, 9, 8, 103, 44, 22, 104decaddci 10432 . . . . . . . . . 10 ; ;
106100, 102, 105prmlem0 13433 . . . . . . . . 9 ; ;
107 prmlem2.17 . . . . . . . . . 10 ;
108107a1i 11 . . . . . . . . 9 ; ;
109 eqid 2438 . . . . . . . . . 10 ; ;
11022, 69, 8, 109, 71decaddi 10431 . . . . . . . . 9 ; ;
111106, 108, 110prmlem0 13433 . . . . . . . 8 ; ;
112 5t3e15 10461 . . . . . . . . . 10 ;
11374, 63, 75, 65, 112nprmi 13099 . . . . . . . . 9 ;
114113pm2.21i 126 . . . . . . . 8 ; ;
115 eqid 2438 . . . . . . . . 9 ; ;
11622, 25, 8, 115, 36decaddi 10431 . . . . . . . 8 ; ;
117111, 114, 116prmlem0 13433 . . . . . . 7 ; ;
118 prmlem2.13 . . . . . . . 8 ;
119118a1i 11 . . . . . . 7 ; ;
120 eqid 2438 . . . . . . . 8 ; ;
12122, 84, 8, 120, 86decaddi 10431 . . . . . . 7 ; ;
122117, 119, 121prmlem0 13433 . . . . . 6 ; ;
123 prmlem2.11 . . . . . . 7 ;
124123a1i 11 . . . . . 6 ; ;
125 eqid 2438 . . . . . . 7 ; ;
12622, 22, 8, 125, 98decaddi 10431 . . . . . 6 ; ;
127122, 124, 126prmlem0 13433 . . . . 5 ; ;
128 9nprm 13440 . . . . . 6
129128pm2.21i 126 . . . . 5
130127, 129, 104prmlem0 13433 . . . 4
131 prmlem2.7 . . . . 5
132131a1i 11 . . . 4
133130, 132, 71prmlem0 13433 . . 3
134 prmlem2.5 . . . 4
135134a1i 11 . . 3
136133, 135, 36prmlem0 13433 . 2
1371, 2, 3, 4, 136prmlem1a 13434 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wa 360   w3a 937   wcel 1726   cdif 3319  csn 3816   class class class wbr 4215  cfv 5457  (class class class)co 6084  cr 8994  cc0 8995  c1 8996   caddc 8998   cmul 9000   clt 9125   cle 9126  cn 10005  c2 10054  c3 10055  c4 10056  c5 10057  c6 10058  c7 10059  c8 10060  c9 10061  ;cdc 10387  cuz 10493  cexp 11387   cdivides 12857  cprime 13084 This theorem is referenced by:  37prm  13448  43prm  13449  83prm  13450  139prm  13451  163prm  13452  317prm  13453  631prm  13454 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-cnex 9051  ax-resscn 9052  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-mulcom 9059  ax-addass 9060  ax-mulass 9061  ax-distr 9062  ax-i2m1 9063  ax-1ne0 9064  ax-1rid 9065  ax-rnegex 9066  ax-rrecex 9067  ax-cnre 9068  ax-pre-lttri 9069  ax-pre-lttrn 9070  ax-pre-ltadd 9071  ax-pre-mulgt0 9072 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-1st 6352  df-2nd 6353  df-riota 6552  df-recs 6636  df-rdg 6671  df-1o 6727  df-2o 6728  df-oadd 6731  df-er 6908  df-en 7113  df-dom 7114  df-sdom 7115  df-fin 7116  df-pnf 9127  df-mnf 9128  df-xr 9129  df-ltxr 9130  df-le 9131  df-sub 9298  df-neg 9299  df-div 9683  df-nn 10006  df-2 10063  df-3 10064  df-4 10065  df-5 10066  df-6 10067  df-7 10068  df-8 10069  df-9 10070  df-10 10071  df-n0 10227  df-z 10288  df-dec 10388  df-uz 10494  df-rp 10618  df-fz 11049  df-seq 11329  df-exp 11388  df-dvds 12858  df-prm 13085
 Copyright terms: Public domain W3C validator