Theorem prmnn 15760

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.

Step	Hyp	Ref	Expression
1		isprm 15759	. 2 ⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑧 ∈ ℕ ∣ 𝑧 ∥ 𝑃} ≈ 2o))
2	1	simplbi 493	1 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2166  {crab 3121   class class class wbr 4873  2_oc2o 7820   ≈ cen 8219  ℕcn 11350   ∥ cdvds 15357  ℙcprime 15757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-br 4874  df-prm 15758

This theorem is referenced by:  prmz  15761  prmssnn  15762  nprmdvds1  15789  isprm5  15790  coprm  15794  prmdvdsexpr  15800  prmndvdsfaclt  15806  cncongrprm  15808  phiprmpw  15852  fermltl  15860  prmdiv  15861  prmdiveq  15862  prmdivdiv  15863  modprm1div  15873  m1dvdsndvds  15874  vfermltl  15877  vfermltlALT  15878  powm2modprm  15879  reumodprminv  15880  modprm0  15881  nnnn0modprm0  15882  modprmn0modprm0  15883  oddprm  15886  nnoddn2prm  15887  prm23lt5  15890  pcpremul  15919  pcdvdsb  15944  pcelnn  15945  pcidlem  15947  pcid  15948  pcdvdstr  15951  pcgcd1  15952  pcprmpw2  15957  dvdsprmpweqnn  15960  dvdsprmpweqle  15961  pcaddlem  15963  pcadd  15964  pcmptcl  15966  pcmpt  15967  pcmpt2  15968  pcfaclem  15973  pcfac  15974  pcbc  15975  expnprm  15977  oddprmdvds  15978  prmpwdvds  15979  pockthlem  15980  pockthg  15981  pockthi  15982  prminf  15990  prmreclem4  15994  prmreclem5  15995  prmreclem6  15996  prmrec  15997  1arith  16002  4sqlem11  16030  4sqlem12  16031  4sqlem13  16032  4sqlem14  16033  4sqlem17  16036  4sqlem18  16037  4sqlem19  16038  prmdvdsprmo  16117  prmgaplem3  16128  prmgaplem4  16129  prmgaplem5  16130  prmgaplem6  16131  prmgaplem8  16133  cshwshashnsame  16176  cshwshash  16177  prmlem1a  16179  pgpfi1  18361  pgp0  18362  sylow1lem1  18364  sylow1lem3  18366  sylow1lem4  18367  sylow1lem5  18368  odcau  18370  pgpfi  18371  fislw  18391  sylow3lem6  18398  gexexlem  18608  prmcyg  18648  ablfac1lem  18821  ablfac1b  18823  ablfac1eu  18826  pgpfac1lem3a  18829  pgpfac1lem3  18830  ablfaclem3  18840  prmirredlem  20201  dfprm2  20202  prmirred  20203  znfld  20268  wilthlem1  25207  wilthlem2  25208  wilthlem3  25209  prmdvdsfi  25246  chtf  25247  efchtcl  25250  vmaval  25252  isppw2  25254  vmappw  25255  vmaprm  25256  vmacl  25257  efvmacl  25259  muval1  25272  chtprm  25292  chtdif  25297  efchtdvds  25298  mumul  25320  sqff1o  25321  dvdsppwf1o  25325  sgmppw  25335  0sgmppw  25336  1sgmprm  25337  vmalelog  25343  chtleppi  25348  chtublem  25349  fsumvma2  25352  vmasum  25354  chpchtsum  25357  chpub  25358  mersenne  25365  perfect1  25366  perfect  25369  pcbcctr  25414  bpos1lem  25420  bposlem1  25422  bposlem2  25423  bposlem6  25427  lgslem1  25435  lgsval2lem  25445  lgsvalmod  25454  lgsmod  25461  lgsdirprm  25469  lgsne0  25473  lgsprme0  25477  lgsqrlem1  25484  lgsqrlem2  25485  lgsqrlem4  25487  lgsqr  25489  lgsqrmod  25490  lgsqrmodndvds  25491  gausslemma2dlem0c  25496  gausslemma2dlem0i  25502  gausslemma2dlem1a  25503  gausslemma2dlem5a  25508  gausslemma2dlem7  25511  gausslemma2d  25512  lgseisenlem1  25513  lgseisenlem2  25514  lgseisenlem3  25515  lgseisenlem4  25516  lgseisen  25517  lgsquadlem1  25518  lgsquadlem2  25519  lgsquadlem3  25520  lgsquad2lem2  25523  lgsquad2  25524  m1lgs  25526  2lgslem1a  25529  2lgslem1c  25531  2lgs  25545  2sqlem3  25558  2sqlem8  25564  2sqlem11  25567  2sqblem  25569  chtppilimlem1  25575  rplogsumlem2  25587  rpvmasumlem  25589  dchrisum0flblem1  25610  dchrisum0flblem2  25611  dirith2  25630  padicabvf  25733  ostth1  25735  ostth3  25740  hashecclwwlkn1  27430  umgrhashecclwwlk  27431  fusgrhashclwwlkn  27432  clwlksfclwwlkOLD  27438  clwlksfoclwwlkOLD  27439  clwlksf1clwwlkOLD  27445  clwlksndivn  27457  numclwwlk5  27803  numclwwlk6  27805  numclwwlk7  27806  numclwwlk8  27807  2sqmod  30193  nn0prpwlem  32855  nn0prpw  32856  nzprmdif  39358  etransclem41  41286  etransclem44  41289  etransclem47  41292  etransclem48  41293  odz2prm2pw  42305  fmtnoprmfac1lem  42306  fmtnoprmfac1  42307  fmtnoprmfac2  42309  prmdvdsfmtnof1lem2  42327  2pwp1prm  42333  sfprmdvdsmersenne  42350  lighneallem2  42353  lighneallem3  42354  lighneallem4  42357  lighneal  42358  perfectALTV  42462  gbepos  42476  gbowpos  42477  sbgoldbaltlem1  42497  ztprmneprm  42972