Theorem prmz 16604

Description: A prime number is an integer. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Jonathan Yan, 16-Jul-2017.)

Assertion

Ref	Expression
prmz	⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)

Proof of Theorem prmz

Step	Hyp	Ref	Expression
1		prmnn 16603	. 2 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
2	1	nnzd 12516	1 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2109  ℤcz 12489  ℙcprime 16600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-i2m1 11096  ax-1ne0 11097  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-neg 11368  df-nn 12147  df-n0 12403  df-z 12490  df-prm 16601

This theorem is referenced by:  dvdsprime  16616  oddprmge3  16629  exprmfct  16633  prmdvdsfz  16634  isprm5  16636  isprm7  16637  maxprmfct  16638  coprm  16640  prmrp  16641  euclemma  16642  prmdvdsexpb  16645  prmexpb  16648  prmfac1  16649  rpexp  16651  cncongrprm  16658  phiprmpw  16705  phiprm  16706  fermltl  16713  prmdiv  16714  prmdiveq  16715  vfermltl  16731  vfermltlALT  16732  reumodprminv  16734  modprm0  16735  oddprm  16740  prm23lt5  16744  prm23ge5  16745  pcneg  16804  pcprmpw2  16812  pcprmpw  16813  difsqpwdvds  16817  pcprod  16825  prmpwdvds  16834  prmunb  16844  prmreclem3  16848  prmreclem5  16850  1arithlem4  16856  1arith  16857  4sqlem11  16885  4sqlem12  16886  4sqlem13  16887  4sqlem14  16888  4sqlem17  16891  prmdvdsprmo  16972  prmdvdsprmop  16973  fvprmselgcd1  16975  prmgaplem4  16984  prmgaplem5  16985  prmgaplem6  16986  prmgaplem8  16988  pgpfi  19502  sylow2alem2  19515  sylow2blem3  19519  gexexlem  19749  ablfacrplem  19964  ablfac1lem  19967  ablfac1b  19969  ablfac1eu  19972  pgpfac1lem2  19974  pgpfac1lem3a  19975  pgpfac1lem3  19976  pgpfac1lem4  19977  ablfaclem3  19986  prmirredlem  21397  rtprmirr  26686  wilthlem1  26994  wilthlem2  26995  ppisval  27030  vmappw  27042  muval1  27059  dvdssqf  27064  mumullem1  27105  mumul  27107  sqff1o  27108  dvdsppwf1o  27112  ppiublem1  27129  ppiublem2  27130  chtublem  27138  vmasum  27143  perfect1  27155  bposlem3  27213  bposlem6  27216  lgslem1  27224  lgsval2lem  27234  lgsvalmod  27243  lgsmod  27250  lgsdirprm  27258  lgsdir  27259  lgsdilem2  27260  lgsdi  27261  lgsne0  27262  lgsprme0  27266  lgsqr  27278  gausslemma2dlem1a  27292  gausslemma2dlem4  27296  gausslemma2dlem5a  27297  lgseisenlem1  27302  lgseisenlem2  27303  lgseisenlem3  27304  lgseisenlem4  27305  lgseisen  27306  lgsquadlem2  27308  lgsquadlem3  27309  lgsquad2lem2  27312  m1lgs  27315  2lgslem1a  27318  2lgslem1  27321  2lgslem2  27322  2lgsoddprm  27343  2sqlem3  27347  2sqlem4  27348  2sqlem6  27350  2sqlem8  27353  2sqblem  27358  2sqb  27359  2sqmod  27363  rpvmasumlem  27414  dchrisum0flblem1  27435  dchrisum0flblem2  27436  dirith  27456  clwwlkndivn  30042  oddprm2  34622  nn0prpwlem  36295  nn0prpw  36296  flt4lem5elem  42624  prmunb2  44284  nzprmdif  44292  etransclem48  46264  sfprmdvdsmersenne  47588  sgprmdvdsmersenne  47589  oddprmALTV  47672  oddprmne2  47700  even3prm2  47704  mogoldbblem  47705  sbgoldbst  47763  sbgoldbaltlem1  47764  sbgoldbaltlem2  47765  nnsum3primesprm  47775  nnsum3primesgbe  47777  nnsum4primesodd  47781  nnsum4primesoddALTV  47782  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  bgoldbtbndlem2  47791  bgoldbtbndlem3  47792  bgoldbtbndlem4  47793  bgoldbtbnd  47794  ztprmneprm  48319