Theorem prmz 16592

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 16591	. 2 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
2	1	nnzd 12501	1 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2111  ℤcz 12474  ℙcprime 16588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674  ax-1cn 11070  ax-icn 11071  ax-addcl 11072  ax-addrcl 11073  ax-mulcl 11074  ax-mulrcl 11075  ax-i2m1 11080  ax-1ne0 11081  ax-rnegex 11083  ax-rrecex 11084  ax-cnre 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6254  df-ord 6315  df-on 6316  df-lim 6317  df-suc 6318  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-ov 7355  df-om 7803  df-2nd 7928  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-neg 11353  df-nn 12132  df-n0 12388  df-z 12475  df-prm 16589

This theorem is referenced by:  dvdsprime  16604  oddprmge3  16617  exprmfct  16621  prmdvdsfz  16622  isprm5  16624  isprm7  16625  maxprmfct  16626  coprm  16628  prmrp  16629  euclemma  16630  prmdvdsexpb  16633  prmexpb  16636  prmfac1  16637  rpexp  16639  cncongrprm  16646  phiprmpw  16693  phiprm  16694  fermltl  16701  prmdiv  16702  prmdiveq  16703  vfermltl  16719  vfermltlALT  16720  reumodprminv  16722  modprm0  16723  oddprm  16728  prm23lt5  16732  prm23ge5  16733  pcneg  16792  pcprmpw2  16800  pcprmpw  16801  difsqpwdvds  16805  pcprod  16813  prmpwdvds  16822  prmunb  16832  prmreclem3  16836  prmreclem5  16838  1arithlem4  16844  1arith  16845  4sqlem11  16873  4sqlem12  16874  4sqlem13  16875  4sqlem14  16876  4sqlem17  16879  prmdvdsprmo  16960  prmdvdsprmop  16961  fvprmselgcd1  16963  prmgaplem4  16972  prmgaplem5  16973  prmgaplem6  16974  prmgaplem8  16976  pgpfi  19523  sylow2alem2  19536  sylow2blem3  19540  gexexlem  19770  ablfacrplem  19985  ablfac1lem  19988  ablfac1b  19990  ablfac1eu  19993  pgpfac1lem2  19995  pgpfac1lem3a  19996  pgpfac1lem3  19997  pgpfac1lem4  19998  ablfaclem3  20007  prmirredlem  21415  rtprmirr  26703  wilthlem1  27011  wilthlem2  27012  ppisval  27047  vmappw  27059  muval1  27076  dvdssqf  27081  mumullem1  27122  mumul  27124  sqff1o  27125  dvdsppwf1o  27129  ppiublem1  27146  ppiublem2  27147  chtublem  27155  vmasum  27160  perfect1  27172  bposlem3  27230  bposlem6  27233  lgslem1  27241  lgsval2lem  27251  lgsvalmod  27260  lgsmod  27267  lgsdirprm  27275  lgsdir  27276  lgsdilem2  27277  lgsdi  27278  lgsne0  27279  lgsprme0  27283  lgsqr  27295  gausslemma2dlem1a  27309  gausslemma2dlem4  27313  gausslemma2dlem5a  27314  lgseisenlem1  27319  lgseisenlem2  27320  lgseisenlem3  27321  lgseisenlem4  27322  lgseisen  27323  lgsquadlem2  27325  lgsquadlem3  27326  lgsquad2lem2  27329  m1lgs  27332  2lgslem1a  27335  2lgslem1  27338  2lgslem2  27339  2lgsoddprm  27360  2sqlem3  27364  2sqlem4  27365  2sqlem6  27367  2sqlem8  27370  2sqblem  27375  2sqb  27376  2sqmod  27380  rpvmasumlem  27431  dchrisum0flblem1  27452  dchrisum0flblem2  27453  dirith  27473  clwwlkndivn  30067  oddprm2  34675  nn0prpwlem  36373  nn0prpw  36374  flt4lem5elem  42750  prmunb2  44409  nzprmdif  44417  etransclem48  46385  sfprmdvdsmersenne  47708  sgprmdvdsmersenne  47709  oddprmALTV  47792  oddprmne2  47820  even3prm2  47824  mogoldbblem  47825  sbgoldbst  47883  sbgoldbaltlem1  47884  sbgoldbaltlem2  47885  nnsum3primesprm  47895  nnsum3primesgbe  47897  nnsum4primesodd  47901  nnsum4primesoddALTV  47902  nnsum4primeseven  47905  nnsum4primesevenALTV  47906  bgoldbtbndlem2  47911  bgoldbtbndlem3  47912  bgoldbtbndlem4  47913  bgoldbtbnd  47914  ztprmneprm  48452