Theorem prmnn 16610

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 16609	. 2 ⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑧 ∈ ℕ ∣ 𝑧 ∥ 𝑃} ≈ 2o))
2	1	simplbi 498	1 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2106  {crab 3432   class class class wbr 5148  2_oc2o 8459   ≈ cen 8935  ℕcn 12211   ∥ cdvds 16196  ℙcprime 16607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-prm 16608

This theorem is referenced by:  prmz  16611  prmssnn  16612  0nprm  16614  2mulprm  16629  nprmdvds1  16642  isprm5  16643  coprm  16647  prmdvdsexpr  16653  prmndvdsfaclt  16661  prmdvdsncoprmbd  16662  cncongrprm  16664  phiprmpw  16708  fermltl  16716  prmdiv  16717  prmdiveq  16718  prmdivdiv  16719  m1dvdsndvds  16730  vfermltl  16733  vfermltlALT  16734  powm2modprm  16735  reumodprminv  16736  modprm0  16737  nnnn0modprm0  16738  modprmn0modprm0  16739  oddprm  16742  nnoddn2prm  16743  prm23lt5  16746  pcpremul  16775  pcdvdsb  16801  pcelnn  16802  pcidlem  16804  pcid  16805  pcdvdstr  16808  pcgcd1  16809  pcprmpw2  16814  dvdsprmpweqnn  16817  dvdsprmpweqle  16818  pcaddlem  16820  pcadd  16821  pcmptcl  16823  pcmpt  16824  pcmpt2  16825  pcfaclem  16830  pcfac  16831  pcbc  16832  expnprm  16834  oddprmdvds  16835  prmpwdvds  16836  pockthlem  16837  pockthg  16838  pockthi  16839  prmreclem4  16851  prmreclem5  16852  prmreclem6  16853  prmrec  16854  1arith  16859  4sqlem11  16887  4sqlem12  16888  4sqlem13  16889  4sqlem14  16890  4sqlem17  16893  4sqlem18  16894  4sqlem19  16895  prmdvdsprmo  16974  prmgaplem3  16985  prmgaplem4  16986  prmgaplem5  16987  prmgaplem6  16988  prmgaplem8  16990  cshwshashnsame  17036  cshwshash  17037  prmlem1a  17039  pgpfi1  19462  pgp0  19463  sylow1lem1  19465  sylow1lem3  19467  sylow1lem4  19468  sylow1lem5  19469  odcau  19471  pgpfi  19472  fislw  19492  sylow3lem6  19499  gexexlem  19719  prmcyg  19761  ablfac1lem  19937  ablfac1b  19939  ablfac1eu  19942  pgpfac1lem3a  19945  pgpfac1lem3  19946  ablfaclem3  19956  prmgrpsimpgd  19983  prmirredlem  21041  dfprm2  21042  prmirred  21043  znfld  21115  wilthlem1  26569  wilthlem2  26570  wilthlem3  26571  chtf  26609  efchtcl  26612  isppw2  26616  vmappw  26617  vmaprm  26618  vmacl  26619  efvmacl  26621  muval1  26634  chtprm  26654  chtdif  26659  efchtdvds  26660  dvdsppwf1o  26687  sgmppw  26697  0sgmppw  26698  1sgmprm  26699  vmalelog  26705  chtleppi  26710  chtublem  26711  fsumvma2  26714  vmasum  26716  chpchtsum  26719  chpub  26720  mersenne  26727  perfect1  26728  perfect  26731  pcbcctr  26776  bpos1lem  26782  bposlem1  26784  bposlem2  26785  bposlem6  26789  lgslem1  26797  lgsval2lem  26807  lgsvalmod  26816  lgsmod  26823  lgsdirprm  26831  lgsne0  26835  lgsprme0  26839  lgsqrlem1  26846  lgsqrlem2  26847  lgsqrlem4  26849  lgsqr  26851  lgsqrmod  26852  lgsqrmodndvds  26853  gausslemma2dlem0c  26858  gausslemma2dlem0i  26864  gausslemma2dlem1a  26865  gausslemma2dlem5a  26870  gausslemma2dlem7  26873  gausslemma2d  26874  lgseisenlem1  26875  lgseisenlem2  26876  lgseisenlem3  26877  lgseisenlem4  26878  lgsquadlem1  26880  lgsquadlem3  26882  lgsquad2lem2  26885  lgsquad2  26886  m1lgs  26888  2lgslem1a  26891  2lgslem1c  26893  2lgs  26907  2sqlem3  26920  2sqlem8  26926  2sqlem11  26929  2sqblem  26931  2sqmod  26936  chtppilimlem1  26973  rplogsumlem2  26985  rpvmasumlem  26987  dchrisum0flblem1  27008  dchrisum0flblem2  27009  padicabvf  27131  ostth1  27133  ostth3  27138  hashecclwwlkn1  29327  umgrhashecclwwlk  29328  fusgrhashclwwlkn  29329  clwlksndivn  29336  numclwwlk5  29638  numclwwlk6  29640  numclwwlk7  29641  numclwwlk8  29642  prmdvdsbc  32017  freshmansdream  32376  frobrhm  32377  fermltlchr  32473  znfermltl  32474  ply1fermltlchr  32657  ply1fermltl  32658  nn0prpwlem  35202  nn0prpw  35203  aks4d1p6  40941  aks4d1p8d1  40944  aks4d1p8d2  40945  aks4d1p8d3  40946  aks4d1p8  40947  aks6d1c2p1  40951  aks6d1c2p2  40952  rtprmirr  41238  nzprmdif  43068  etransclem41  44981  etransclem44  44984  etransclem47  44987  etransclem48  44988  odz2prm2pw  46221  fmtnoprmfac1lem  46222  fmtnoprmfac1  46223  fmtnoprmfac2  46225  prmdvdsfmtnof1lem2  46243  2pwp1prm  46247  sfprmdvdsmersenne  46261  lighneallem2  46264  lighneallem3  46265  lighneallem4  46268  lighneal  46269  perfectALTV  46381  gbepos  46416  gbowpos  46417  sbgoldbaltlem1  46437  ztprmneprm  47013