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

Theorem prmnn 16006
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 16005 . 2 (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑧 ∈ ℕ ∣ 𝑧𝑃} ≈ 2o))
21simplbi 498 1 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  {crab 3139   class class class wbr 5057  2oc2o 8085  cen 8494  cn 11626  cdvds 15595  cprime 16003
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-prm 16004
This theorem is referenced by:  prmz  16007  prmssnn  16008  0nprm  16010  2mulprm  16025  nprmdvds1  16038  isprm5  16039  coprm  16043  prmdvdsexpr  16049  prmndvdsfaclt  16055  cncongrprm  16057  phiprmpw  16101  fermltl  16109  prmdiv  16110  prmdiveq  16111  prmdivdiv  16112  m1dvdsndvds  16123  vfermltl  16126  vfermltlALT  16127  powm2modprm  16128  reumodprminv  16129  modprm0  16130  nnnn0modprm0  16131  modprmn0modprm0  16132  oddprm  16135  nnoddn2prm  16136  prm23lt5  16139  pcpremul  16168  pcdvdsb  16193  pcelnn  16194  pcidlem  16196  pcid  16197  pcdvdstr  16200  pcgcd1  16201  pcprmpw2  16206  dvdsprmpweqnn  16209  dvdsprmpweqle  16210  pcaddlem  16212  pcadd  16213  pcmptcl  16215  pcmpt  16216  pcmpt2  16217  pcfaclem  16222  pcfac  16223  pcbc  16224  expnprm  16226  oddprmdvds  16227  prmpwdvds  16228  pockthlem  16229  pockthg  16230  pockthi  16231  prmreclem4  16243  prmreclem5  16244  prmreclem6  16245  prmrec  16246  1arith  16251  4sqlem11  16279  4sqlem12  16280  4sqlem13  16281  4sqlem14  16282  4sqlem17  16285  4sqlem18  16286  4sqlem19  16287  prmdvdsprmo  16366  prmgaplem3  16377  prmgaplem4  16378  prmgaplem5  16379  prmgaplem6  16380  prmgaplem8  16382  cshwshashnsame  16425  cshwshash  16426  prmlem1a  16428  pgpfi1  18649  pgp0  18650  sylow1lem1  18652  sylow1lem3  18654  sylow1lem4  18655  sylow1lem5  18656  odcau  18658  pgpfi  18659  fislw  18679  sylow3lem6  18686  gexexlem  18901  prmcyg  18943  ablfac1lem  19119  ablfac1b  19121  ablfac1eu  19124  pgpfac1lem3a  19127  pgpfac1lem3  19128  ablfaclem3  19138  prmgrpsimpgd  19165  prmirredlem  20568  dfprm2  20569  prmirred  20570  znfld  20635  wilthlem1  25572  wilthlem2  25573  wilthlem3  25574  chtf  25612  efchtcl  25615  isppw2  25619  vmappw  25620  vmaprm  25621  vmacl  25622  efvmacl  25624  muval1  25637  chtprm  25657  chtdif  25662  efchtdvds  25663  dvdsppwf1o  25690  sgmppw  25700  0sgmppw  25701  1sgmprm  25702  vmalelog  25708  chtleppi  25713  chtublem  25714  fsumvma2  25717  vmasum  25719  chpchtsum  25722  chpub  25723  mersenne  25730  perfect1  25731  perfect  25734  pcbcctr  25779  bpos1lem  25785  bposlem1  25787  bposlem2  25788  bposlem6  25792  lgslem1  25800  lgsval2lem  25810  lgsvalmod  25819  lgsmod  25826  lgsdirprm  25834  lgsne0  25838  lgsprme0  25842  lgsqrlem1  25849  lgsqrlem2  25850  lgsqrlem4  25852  lgsqr  25854  lgsqrmod  25855  lgsqrmodndvds  25856  gausslemma2dlem0c  25861  gausslemma2dlem0i  25867  gausslemma2dlem1a  25868  gausslemma2dlem5a  25873  gausslemma2dlem7  25876  gausslemma2d  25877  lgseisenlem1  25878  lgseisenlem2  25879  lgseisenlem3  25880  lgseisenlem4  25881  lgsquadlem1  25883  lgsquadlem3  25885  lgsquad2lem2  25888  lgsquad2  25889  m1lgs  25891  2lgslem1a  25894  2lgslem1c  25896  2lgs  25910  2sqlem3  25923  2sqlem8  25929  2sqlem11  25932  2sqblem  25934  2sqmod  25939  chtppilimlem1  25976  rplogsumlem2  25988  rpvmasumlem  25990  dchrisum0flblem1  26011  dchrisum0flblem2  26012  padicabvf  26134  ostth1  26136  ostth3  26141  hashecclwwlkn1  27783  umgrhashecclwwlk  27784  fusgrhashclwwlkn  27785  clwlksndivn  27792  numclwwlk5  28094  numclwwlk6  28096  numclwwlk7  28097  numclwwlk8  28098  prmdvdsbc  30458  freshmansdream  30786  nn0prpwlem  33567  nn0prpw  33568  rtprmirr  39072  nzprmdif  40528  etransclem41  42437  etransclem44  42440  etransclem47  42443  etransclem48  42444  odz2prm2pw  43602  fmtnoprmfac1lem  43603  fmtnoprmfac1  43604  fmtnoprmfac2  43606  prmdvdsfmtnof1lem2  43624  2pwp1prm  43628  sfprmdvdsmersenne  43645  lighneallem2  43648  lighneallem3  43649  lighneallem4  43652  lighneal  43653  perfectALTV  43765  gbepos  43800  gbowpos  43801  sbgoldbaltlem1  43821  ztprmneprm  44323
  Copyright terms: Public domain W3C validator