Theorem prmz 16612

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℤcz 12558  ℙcprime 16608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-i2m1 11178  ax-1ne0 11179  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-neg 11447  df-nn 12213  df-n0 12473  df-z 12559  df-prm 16609

This theorem is referenced by:  dvdsprime  16624  oddprmge3  16637  exprmfct  16641  prmdvdsfz  16642  isprm5  16644  isprm7  16645  maxprmfct  16646  coprm  16648  prmrp  16649  euclemma  16650  prmdvdsexpb  16653  prmexpb  16657  prmfac1  16658  rpexp  16659  cncongrprm  16665  phiprmpw  16709  phiprm  16710  fermltl  16717  prmdiv  16718  prmdiveq  16719  vfermltl  16734  vfermltlALT  16735  reumodprminv  16737  modprm0  16738  oddprm  16743  prm23lt5  16747  prm23ge5  16748  pcneg  16807  pcprmpw2  16815  pcprmpw  16816  difsqpwdvds  16820  pcprod  16828  prmpwdvds  16837  prmunb  16847  prmreclem3  16851  prmreclem5  16853  1arithlem4  16859  1arith  16860  4sqlem11  16888  4sqlem12  16889  4sqlem13  16890  4sqlem14  16891  4sqlem17  16894  prmdvdsprmo  16975  prmdvdsprmop  16976  fvprmselgcd1  16978  prmgaplem4  16987  prmgaplem5  16988  prmgaplem6  16989  prmgaplem8  16991  pgpfi  19473  sylow2alem2  19486  sylow2blem3  19490  gexexlem  19720  ablfacrplem  19935  ablfac1lem  19938  ablfac1b  19940  ablfac1eu  19943  pgpfac1lem2  19945  pgpfac1lem3a  19946  pgpfac1lem3  19947  pgpfac1lem4  19948  ablfaclem3  19957  prmirredlem  21042  wilthlem1  26572  wilthlem2  26573  ppisval  26608  vmappw  26620  muval1  26637  dvdssqf  26642  mumullem1  26683  mumul  26685  sqff1o  26686  dvdsppwf1o  26690  ppiublem1  26705  ppiublem2  26706  chtublem  26714  vmasum  26719  perfect1  26731  bposlem3  26789  bposlem6  26792  lgslem1  26800  lgsval2lem  26810  lgsvalmod  26819  lgsmod  26826  lgsdirprm  26834  lgsdir  26835  lgsdilem2  26836  lgsdi  26837  lgsne0  26838  lgsprme0  26842  lgsqr  26854  gausslemma2dlem1a  26868  gausslemma2dlem4  26872  gausslemma2dlem5a  26873  lgseisenlem1  26878  lgseisenlem2  26879  lgseisenlem3  26880  lgseisenlem4  26881  lgseisen  26882  lgsquadlem2  26884  lgsquadlem3  26885  lgsquad2lem2  26888  m1lgs  26891  2lgslem1a  26894  2lgslem1  26897  2lgslem2  26898  2lgsoddprm  26919  2sqlem3  26923  2sqlem4  26924  2sqlem6  26926  2sqlem8  26929  2sqblem  26934  2sqb  26935  2sqmod  26939  rpvmasumlem  26990  dchrisum0flblem1  27011  dchrisum0flblem2  27012  dirith  27032  clwwlkndivn  29333  oddprm2  33667  nn0prpwlem  35207  nn0prpw  35208  rtprmirr  41237  flt4lem5elem  41393  prmunb2  43070  nzprmdif  43078  etransclem48  44998  sfprmdvdsmersenne  46271  sgprmdvdsmersenne  46272  oddprmALTV  46355  oddprmne2  46383  even3prm2  46387  mogoldbblem  46388  sbgoldbst  46446  sbgoldbaltlem1  46447  sbgoldbaltlem2  46448  nnsum3primesprm  46458  nnsum3primesgbe  46460  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  bgoldbtbndlem4  46476  bgoldbtbnd  46477  ztprmneprm  47023