![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > prmnn | Unicode version |
Description: A prime number is a positive integer. (Contributed by Paul Chapman, 22-Jun-2011.) |
Ref | Expression |
---|---|
prmnn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isprm 12250 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simplbi 274 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2175 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ral 2477 df-rab 2481 df-v 2762 df-un 3158 df-sn 3625 df-pr 3626 df-op 3628 df-br 4031 df-prm 12249 |
This theorem is referenced by: prmz 12252 prmssnn 12253 nprmdvds1 12281 isprm5lem 12282 isprm5 12283 coprm 12285 euclemma 12287 prmdvdsexpr 12291 cncongrprm 12298 phiprmpw 12363 fermltl 12375 prmdiv 12376 prmdiveq 12377 prmdivdiv 12378 m1dvdsndvds 12389 vfermltl 12392 powm2modprm 12393 reumodprminv 12394 modprm0 12395 nnnn0modprm0 12396 modprmn0modprm0 12397 oddprm 12400 nnoddn2prm 12401 prm23lt5 12404 pcpremul 12434 pcdvdsb 12461 pcelnn 12462 pcidlem 12464 pcid 12465 pcdvdstr 12468 pcgcd1 12469 pcprmpw2 12474 dvdsprmpweqnn 12477 dvdsprmpweqle 12478 pcaddlem 12480 pcadd 12481 pcmptcl 12483 pcmpt 12484 pcmpt2 12485 pcfaclem 12490 pcfac 12491 pcbc 12492 expnprm 12494 oddprmdvds 12495 prmpwdvds 12496 pockthlem 12497 pockthg 12498 pockthi 12499 1arith 12508 4sqlem11 12542 4sqlem12 12543 4sqlem13m 12544 4sqlem14 12545 4sqlem17 12548 4sqlem18 12549 4sqlem19 12550 znidom 14156 wilthlem1 15153 lgslem1 15157 lgslem4 15160 lgsval 15161 lgsval2lem 15167 lgsvalmod 15176 lgsmod 15183 lgsdirprm 15191 lgsne0 15195 lgsprme0 15199 gausslemma2dlem0c 15208 gausslemma2dlem1a 15215 gausslemma2dlem5a 15222 lgseisenlem1 15227 lgseisenlem2 15228 lgseisenlem3 15229 lgseisenlem4 15230 lgsquadlem1 15234 lgsquadlem3 15236 lgsquad2lem2 15239 lgsquad2 15240 m1lgs 15242 2lgslem1a 15245 2lgslem1c 15247 2lgs 15261 2sqlem3 15274 2sqlem8 15280 |
Copyright terms: Public domain | W3C validator |