Theorem prmnn 12912

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  {crab 2532   class class class wbr 4131  2_oc2o 6686   ≈ cen 7026  ℕcn 9313   ∥ cdvds 12578  ℙcprime 12909

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rab 2537  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4132  df-prm 12910

This theorem is used by:  prmz  12913  prmssnn  12914  prmdcz  12933  nprmdvds1  12943  isprm5lem  12944  isprm5  12945  coprm  12947  euclemma  12949  prmdvdsexpr  12953  cncongrprm  12960  phiprmpw  13028  fermltl  13040  prmdiv  13041  prmdiveq  13042  prmdivdiv  13043  m1dvdsndvds  13055  vfermltl  13058  powm2modprm  13059  reumodprminv  13060  modprm0  13061  nnnn0modprm0  13062  modprmn0modprm0  13063  oddprm  13066  nnoddn2prm  13067  prm23lt5  13070  pcpremul  13100  pcdvdsb  13127  pcelnn  13128  pcidlem  13130  pcid  13131  pcdvdstr  13134  pcgcd1  13135  pcprmpw2  13140  dvdsprmpweqnn  13143  dvdsprmpweqle  13144  pcaddlem  13146  pcadd  13147  pcmptcl  13149  pcmpt  13150  pcmpt2  13151  pcfaclem  13156  pcfac  13157  pcbc  13158  expnprm  13160  oddprmdvds  13161  prmpwdvds  13162  pockthlem  13163  pockthg  13164  pockthi  13165  1arith  13174  4sqlem11  13208  4sqlem12  13209  4sqlem13m  13210  4sqlem14  13211  4sqlem17  13214  4sqlem18  13215  4sqlem19  13216  prmlem1a  13249  znidom  15100  zprmlogbaplem1  16232  zprmlogbaplem2  16233  zprmlogbaplem3  16234  wilthlem1  16249  chtqcl  16261  chtqval  16262  efchtqcl  16263  chtprm  16278  chtdif  16281  efchtqdvds  16282  dvdsppwf1o  16300  sgmppw  16303  0sgmppw  16304  1sgmprm  16305  chtqleppi  16311  chtublem  16312  mersenne  16314  perfect1  16315  perfect  16318  pcbcctr  16320  prmefexple  16325  bpos1lem  16326  bposlem1  16328  bposlem2  16329  bposlem6  16333  bpos  16337  lgslem1  16341  lgslem4  16344  lgsval  16345  lgsval2lem  16351  lgsvalmod  16360  lgsmod  16367  lgsdirprm  16375  lgsne0  16379  lgsprme0  16383  gausslemma2dlem0c  16392  gausslemma2dlem1a  16399  gausslemma2dlem5a  16406  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem3  16413  lgseisenlem4  16414  lgsquadlem1  16418  lgsquadlem3  16420  lgsquad2lem2  16423  lgsquad2  16424  m1lgs  16426  2lgslem1a  16429  2lgslem1c  16431  2lgs  16445  2sqlem3  16458  2sqlem8  16464