Theorem prmnn 12278

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

Syntax hints:   → wi 4   ∈ wcel 2167  {crab 2479   class class class wbr 4033  2_oc2o 6468   ≈ cen 6797  ℕcn 8990   ∥ cdvds 11952  ℙcprime 12275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rab 2484  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-br 4034  df-prm 12276

This theorem is referenced by:  prmz  12279  prmssnn  12280  nprmdvds1  12308  isprm5lem  12309  isprm5  12310  coprm  12312  euclemma  12314  prmdvdsexpr  12318  cncongrprm  12325  phiprmpw  12390  fermltl  12402  prmdiv  12403  prmdiveq  12404  prmdivdiv  12405  m1dvdsndvds  12417  vfermltl  12420  powm2modprm  12421  reumodprminv  12422  modprm0  12423  nnnn0modprm0  12424  modprmn0modprm0  12425  oddprm  12428  nnoddn2prm  12429  prm23lt5  12432  pcpremul  12462  pcdvdsb  12489  pcelnn  12490  pcidlem  12492  pcid  12493  pcdvdstr  12496  pcgcd1  12497  pcprmpw2  12502  dvdsprmpweqnn  12505  dvdsprmpweqle  12506  pcaddlem  12508  pcadd  12509  pcmptcl  12511  pcmpt  12512  pcmpt2  12513  pcfaclem  12518  pcfac  12519  pcbc  12520  expnprm  12522  oddprmdvds  12523  prmpwdvds  12524  pockthlem  12525  pockthg  12526  pockthi  12527  1arith  12536  4sqlem11  12570  4sqlem12  12571  4sqlem13m  12572  4sqlem14  12573  4sqlem17  12576  4sqlem18  12577  4sqlem19  12578  znidom  14213  wilthlem1  15216  dvdsppwf1o  15225  sgmppw  15228  0sgmppw  15229  1sgmprm  15230  mersenne  15233  perfect1  15234  perfect  15237  lgslem1  15241  lgslem4  15244  lgsval  15245  lgsval2lem  15251  lgsvalmod  15260  lgsmod  15267  lgsdirprm  15275  lgsne0  15279  lgsprme0  15283  gausslemma2dlem0c  15292  gausslemma2dlem1a  15299  gausslemma2dlem5a  15306  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgseisenlem4  15314  lgsquadlem1  15318  lgsquadlem3  15320  lgsquad2lem2  15323  lgsquad2  15324  m1lgs  15326  2lgslem1a  15329  2lgslem1c  15331  2lgs  15345  2sqlem3  15358  2sqlem8  15364