Theorem prmnn 16634

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

Syntax hints:   → wi 4   ∈ wcel 2119  {crab 3391   class class class wbr 5072  2_oc2o 8389   ≈ cen 8880  ℕcn 12165   ∥ cdvds 16212  ℙcprime 16631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-prm 16632

This theorem is referenced by:  prmz  16635  prmssnn  16636  0nprm  16638  2mulprm  16653  nprmdvds1  16667  isprm5  16668  coprm  16672  prmdvdsexpr  16678  prmndvdsfaclt  16686  prmdvdsbc  16687  prmdvdsncoprmbd  16688  cncongrprm  16690  phiprmpw  16737  fermltl  16745  prmdiv  16746  prmdiveq  16747  prmdivdiv  16748  m1dvdsndvds  16760  vfermltl  16763  vfermltlALT  16764  powm2modprm  16765  reumodprminv  16766  modprm0  16767  nnnn0modprm0  16768  modprmn0modprm0  16769  oddprm  16772  nnoddn2prm  16773  prm23lt5  16776  pcpremul  16805  pcdvdsb  16831  pcelnn  16832  pcidlem  16834  pcid  16835  pcdvdstr  16838  pcgcd1  16839  pcprmpw2  16844  dvdsprmpweqnn  16847  dvdsprmpweqle  16848  pcaddlem  16850  pcadd  16851  pcmptcl  16853  pcmpt  16854  pcmpt2  16855  pcfaclem  16860  pcfac  16861  pcbc  16862  expnprm  16864  oddprmdvds  16865  prmpwdvds  16866  pockthlem  16867  pockthg  16868  pockthi  16869  prmreclem4  16881  prmreclem5  16882  prmreclem6  16883  prmrec  16884  1arith  16889  4sqlem11  16917  4sqlem12  16918  4sqlem13  16919  4sqlem14  16920  4sqlem17  16923  4sqlem18  16924  4sqlem19  16925  prmdvdsprmo  17004  prmgaplem3  17015  prmgaplem4  17016  prmgaplem5  17017  prmgaplem6  17018  prmgaplem8  17020  cshwshashnsame  17065  cshwshash  17066  prmlem1a  17068  pgpfi1  19561  pgp0  19562  sylow1lem1  19564  sylow1lem3  19566  sylow1lem4  19567  sylow1lem5  19568  odcau  19570  pgpfi  19571  fislw  19591  sylow3lem6  19598  gexexlem  19818  prmcyg  19860  ablfac1lem  20036  ablfac1b  20038  ablfac1eu  20041  pgpfac1lem3a  20044  pgpfac1lem3  20045  ablfaclem3  20055  prmgrpsimpgd  20082  prmirredlem  21447  dfprm2  21448  prmirred  21449  fermltlchr  21504  znfld  21535  freshmansdream  21549  frobrhm  21550  ply1fermltlchr  22298  rtprmirr  26742  wilthlem1  27049  wilthlem2  27050  wilthlem3  27051  chtf  27089  efchtcl  27092  isppw2  27096  vmappw  27097  vmaprm  27098  vmacl  27099  efvmacl  27101  muval1  27114  chtprm  27134  chtdif  27139  efchtdvds  27140  dvdsppwf1o  27167  sgmppw  27178  0sgmppw  27179  1sgmprm  27180  vmalelog  27186  chtleppi  27191  chtublem  27192  fsumvma2  27195  vmasum  27197  chpchtsum  27200  chpub  27201  mersenne  27208  perfect1  27209  perfect  27212  pcbcctr  27257  bpos1lem  27263  bposlem1  27265  bposlem2  27266  bposlem6  27270  lgslem1  27278  lgsval2lem  27288  lgsvalmod  27297  lgsmod  27304  lgsdirprm  27312  lgsne0  27316  lgsprme0  27320  lgsqrlem1  27327  lgsqrlem2  27328  lgsqrlem4  27330  lgsqr  27332  lgsqrmod  27333  lgsqrmodndvds  27334  gausslemma2dlem0c  27339  gausslemma2dlem0i  27345  gausslemma2dlem1a  27346  gausslemma2dlem5a  27351  gausslemma2dlem7  27354  gausslemma2d  27355  lgseisenlem1  27356  lgseisenlem2  27357  lgseisenlem3  27358  lgseisenlem4  27359  lgsquadlem1  27361  lgsquadlem3  27363  lgsquad2lem2  27366  lgsquad2  27367  m1lgs  27369  2lgslem1a  27372  2lgslem1c  27374  2lgs  27388  2sqlem3  27401  2sqlem8  27407  2sqlem11  27410  2sqblem  27412  2sqmod  27417  chtppilimlem1  27454  rplogsumlem2  27466  rpvmasumlem  27468  dchrisum0flblem1  27489  dchrisum0flblem2  27490  padicabvf  27612  ostth1  27614  ostth3  27619  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  fusgrhashclwwlkn  30167  clwlksndivn  30174  numclwwlk5  30476  numclwwlk6  30478  numclwwlk7  30479  numclwwlk8  30480  znfermltl  33449  ply1fermltl  33669  cos9thpiminplylem2  33967  nn0prpwlem  36550  nn0prpw  36551  aks4d1p6  42566  aks4d1p8d1  42569  aks4d1p8d2  42570  aks4d1p8d3  42571  aks4d1p8  42572  aks6d1c1p2  42594  aks6d1c1p3  42595  aks6d1c1  42601  aks6d1c2p1  42603  aks6d1c2p2  42604  aks6d1c3  42608  aks6d1c4  42609  aks6d1c2lem4  42612  aks6d1c5lem1  42621  aks6d1c6lem3  42657  aks6d1c6lem4  42658  aks6d1c7lem1  42665  aks6d1c7  42669  aks5lem1  42671  aks5lem2  42672  aks5lem3a  42674  aks5lem8  42686  aks5  42689  nzprmdif  44763  etransclem41  46718  etransclem44  46721  etransclem47  46724  etransclem48  46725  odz2prm2pw  48041  fmtnoprmfac1lem  48042  fmtnoprmfac1  48043  fmtnoprmfac2  48045  prmdvdsfmtnof1lem2  48063  2pwp1prm  48067  sfprmdvdsmersenne  48081  lighneallem2  48084  lighneallem3  48085  lighneallem4  48088  lighneal  48089  perfectALTV  48214  gbepos  48249  gbowpos  48250  sbgoldbaltlem1  48270  ztprmneprm  48838