Theorem prmnn 12907

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  {crab 2532   class class class wbr 4130  2_oc2o 6681   ≈ cen 7020  ℕcn 9307   ∥ cdvds 12573  ℙcprime 12904

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 4131  df-prm 12905

This theorem is used by:  prmz  12908  prmssnn  12909  prmdcz  12928  nprmdvds1  12938  isprm5lem  12939  isprm5  12940  coprm  12942  euclemma  12944  prmdvdsexpr  12948  cncongrprm  12955  phiprmpw  13023  fermltl  13035  prmdiv  13036  prmdiveq  13037  prmdivdiv  13038  m1dvdsndvds  13050  vfermltl  13053  powm2modprm  13054  reumodprminv  13055  modprm0  13056  nnnn0modprm0  13057  modprmn0modprm0  13058  oddprm  13061  nnoddn2prm  13062  prm23lt5  13065  pcpremul  13095  pcdvdsb  13122  pcelnn  13123  pcidlem  13125  pcid  13126  pcdvdstr  13129  pcgcd1  13130  pcprmpw2  13135  dvdsprmpweqnn  13138  dvdsprmpweqle  13139  pcaddlem  13141  pcadd  13142  pcmptcl  13144  pcmpt  13145  pcmpt2  13146  pcfaclem  13151  pcfac  13152  pcbc  13153  expnprm  13155  oddprmdvds  13156  prmpwdvds  13157  pockthlem  13158  pockthg  13159  pockthi  13160  1arith  13169  4sqlem11  13203  4sqlem12  13204  4sqlem13m  13205  4sqlem14  13206  4sqlem17  13209  4sqlem18  13210  4sqlem19  13211  prmlem1a  13244  znidom  15076  zprmlogbaplem1  16176  zprmlogbaplem2  16177  zprmlogbaplem3  16178  wilthlem1  16193  chtqcl  16205  chtqval  16206  efchtqcl  16207  chtprm  16222  chtdif  16225  efchtqdvds  16226  dvdsppwf1o  16244  sgmppw  16247  0sgmppw  16248  1sgmprm  16249  chtqleppi  16255  chtublem  16256  mersenne  16258  perfect1  16259  perfect  16262  pcbcctr  16264  prmefexple  16269  bpos1lem  16270  bposlem1  16272  bposlem2  16273  bposlem6  16277  bpos  16281  lgslem1  16285  lgslem4  16288  lgsval  16289  lgsval2lem  16295  lgsvalmod  16304  lgsmod  16311  lgsdirprm  16319  lgsne0  16323  lgsprme0  16327  gausslemma2dlem0c  16336  gausslemma2dlem1a  16343  gausslemma2dlem5a  16350  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem3  16357  lgseisenlem4  16358  lgsquadlem1  16362  lgsquadlem3  16364  lgsquad2lem2  16367  lgsquad2  16368  m1lgs  16370  2lgslem1a  16373  2lgslem1c  16375  2lgs  16389  2sqlem3  16402  2sqlem8  16408