Theorem prmnn 12112

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

Syntax hints:   → wi 4   ∈ wcel 2148  {crab 2459   class class class wbr 4005  2_oc2o 6413   ≈ cen 6740  ℕcn 8921   ∥ cdvds 11796  ℙcprime 12109

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rab 2464  df-v 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-br 4006  df-prm 12110

This theorem is referenced by:  prmz  12113  prmssnn  12114  nprmdvds1  12142  isprm5lem  12143  isprm5  12144  coprm  12146  euclemma  12148  prmdvdsexpr  12152  cncongrprm  12159  phiprmpw  12224  fermltl  12236  prmdiv  12237  prmdiveq  12238  prmdivdiv  12239  m1dvdsndvds  12250  vfermltl  12253  powm2modprm  12254  reumodprminv  12255  modprm0  12256  nnnn0modprm0  12257  modprmn0modprm0  12258  oddprm  12261  nnoddn2prm  12262  prm23lt5  12265  pcpremul  12295  pcdvdsb  12321  pcelnn  12322  pcidlem  12324  pcid  12325  pcdvdstr  12328  pcgcd1  12329  pcprmpw2  12334  dvdsprmpweqnn  12337  dvdsprmpweqle  12338  pcaddlem  12340  pcadd  12341  pcmptcl  12342  pcmpt  12343  pcmpt2  12344  pcfaclem  12349  pcfac  12350  pcbc  12351  expnprm  12353  oddprmdvds  12354  prmpwdvds  12355  pockthlem  12356  pockthg  12357  pockthi  12358  1arith  12367  lgslem1  14486  lgslem4  14489  lgsval  14490  lgsval2lem  14496  lgsvalmod  14505  lgsmod  14512  lgsdirprm  14520  lgsne0  14524  lgsprme0  14528  lgseisenlem1  14535  lgseisenlem2  14536  m1lgs  14537  2sqlem3  14549  2sqlem8  14555