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

Theorem prmnn 14220
Description: A prime number is a positive integer. (Contributed by Paul Chapman, 22-Jun-2011.)
Assertion
Ref Expression
prmnn

Proof of Theorem prmnn
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 isprm 14219 . 2
21simplbi 460 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  {crab 2811   class class class wbr 4452   c2o 7143   cen 7533   cn 10561   cdvds 13986   cprime 14217
This theorem is referenced by:  prmz  14221  coprm  14241  nprmdvds1  14252  isprm5  14253  prmdvdsexpr  14257  phiprmpw  14306  fermltl  14314  prmdiv  14315  prmdiveq  14316  prmdivdiv  14317  modprm1div  14324  m1dvdsndvds  14325  powm2modprm  14328  reumodprminv  14329  modprm0  14330  nnnn0modprm0  14331  modprmn0modprm0  14332  oddprm  14339  pcpremul  14367  pcdvdsb  14392  pcelnn  14393  pcidlem  14395  pcid  14396  pcdvdstr  14399  pcgcd1  14400  pcprmpw2  14405  pcaddlem  14407  pcadd  14408  pcmptcl  14410  pcmpt  14411  pcmpt2  14412  pcfaclem  14417  pcfac  14418  pcbc  14419  expnprm  14421  prmpwdvds  14422  pockthlem  14423  pockthg  14424  pockthi  14425  prminf  14433  prmreclem4  14437  prmreclem5  14438  prmreclem6  14439  prmrec  14440  1arith  14445  4sqlem11  14473  4sqlem12  14474  4sqlem13  14475  4sqlem14  14476  4sqlem17  14479  4sqlem18  14480  4sqlem19  14481  cshwshashnsame  14588  cshwshash  14589  prmlem1a  14592  pgpfi1  16615  pgp0  16616  sylow1lem1  16618  sylow1lem3  16620  sylow1lem4  16621  sylow1lem5  16622  odcau  16624  pgpfi  16625  fislw  16645  sylow3lem6  16652  gexexlem  16858  prmcyg  16896  ablfac1lem  17119  ablfac1b  17121  ablfac1eu  17124  pgpfac1lem3a  17127  pgpfac1lem3  17128  ablfaclem3  17138  prmirredlem  18523  dfprm2  18524  prmirred  18525  prmirredlemOLD  18526  dfprm2OLD  18527  prmirredOLD  18528  znfld  18599  wilthlem1  23342  wilthlem2  23343  wilthlem3  23344  prmdvdsfi  23381  chtf  23382  efchtcl  23385  vmaval  23387  isppw2  23389  vmappw  23390  vmaprm  23391  vmacl  23392  efvmacl  23394  muval1  23407  chtprm  23427  chtdif  23432  efchtdvds  23433  mumul  23455  sqff1o  23456  dvdsppwf1o  23462  sgmppw  23472  0sgmppw  23473  1sgmprm  23474  vmalelog  23480  chtleppi  23485  chtublem  23486  fsumvma2  23489  vmasum  23491  chpchtsum  23494  chpub  23495  mersenne  23502  perfect1  23503  perfect  23506  pcbcctr  23551  bpos1lem  23557  bposlem1  23559  bposlem2  23560  bposlem6  23564  lgslem1  23571  lgsval2lem  23581  lgsvalmod  23590  lgsmod  23596  lgsdirprm  23604  lgsne0  23608  lgsqrlem1  23616  lgsqrlem2  23617  lgsqrlem4  23619  lgsqr  23621  lgseisenlem1  23624  lgseisenlem2  23625  lgseisenlem3  23626  lgseisenlem4  23627  lgseisen  23628  lgsquadlem1  23629  lgsquadlem2  23630  lgsquadlem3  23631  lgsquad2lem2  23634  lgsquad2  23635  m1lgs  23637  2sqlem3  23641  2sqlem8  23647  2sqlem11  23650  2sqblem  23652  chtppilimlem1  23658  rplogsumlem2  23670  rpvmasumlem  23672  dchrisum0flblem1  23693  dchrisum0flblem2  23694  dirith2  23713  padicabvf  23816  ostth1  23818  ostth3  23823  hashecclwwlkn1  24834  usghashecclwwlk  24835  hashclwwlkn  24836  clwwlkndivn  24837  clwlkfclwwlk  24844  clwlkfoclwwlk  24845  clwlkf1clwwlk  24850  numclwwlk5  25112  numclwwlk6  25113  numclwwlk7  25114  numclwwlk8  25115  2sqmod  27636  nn0prpwlem  30140  nn0prpw  30141  nzprmdif  31224  etransclem41  32058  etransclem44  32061  etransclem47  32064  etransclem48  32065  ztprmneprm  32936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-prm 14218
  Copyright terms: Public domain W3C validator