Theorem prmz 16617

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℤcz 12563  ℙcprime 16613

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-i2m1 11182  ax-1ne0 11183  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7415  df-om 7860  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-neg 11452  df-nn 12218  df-n0 12478  df-z 12564  df-prm 16614

This theorem is referenced by:  dvdsprime  16629  oddprmge3  16642  exprmfct  16646  prmdvdsfz  16647  isprm5  16649  isprm7  16650  maxprmfct  16651  coprm  16653  prmrp  16654  euclemma  16655  prmdvdsexpb  16658  prmexpb  16662  prmfac1  16663  rpexp  16664  cncongrprm  16670  phiprmpw  16714  phiprm  16715  fermltl  16722  prmdiv  16723  prmdiveq  16724  vfermltl  16739  vfermltlALT  16740  reumodprminv  16742  modprm0  16743  oddprm  16748  prm23lt5  16752  prm23ge5  16753  pcneg  16812  pcprmpw2  16820  pcprmpw  16821  difsqpwdvds  16825  pcprod  16833  prmpwdvds  16842  prmunb  16852  prmreclem3  16856  prmreclem5  16858  1arithlem4  16864  1arith  16865  4sqlem11  16893  4sqlem12  16894  4sqlem13  16895  4sqlem14  16896  4sqlem17  16899  prmdvdsprmo  16980  prmdvdsprmop  16981  fvprmselgcd1  16983  prmgaplem4  16992  prmgaplem5  16993  prmgaplem6  16994  prmgaplem8  16996  pgpfi  19515  sylow2alem2  19528  sylow2blem3  19532  gexexlem  19762  ablfacrplem  19977  ablfac1lem  19980  ablfac1b  19982  ablfac1eu  19985  pgpfac1lem2  19987  pgpfac1lem3a  19988  pgpfac1lem3  19989  pgpfac1lem4  19990  ablfaclem3  19999  prmirredlem  21244  wilthlem1  26809  wilthlem2  26810  ppisval  26845  vmappw  26857  muval1  26874  dvdssqf  26879  mumullem1  26920  mumul  26922  sqff1o  26923  dvdsppwf1o  26927  ppiublem1  26942  ppiublem2  26943  chtublem  26951  vmasum  26956  perfect1  26968  bposlem3  27026  bposlem6  27029  lgslem1  27037  lgsval2lem  27047  lgsvalmod  27056  lgsmod  27063  lgsdirprm  27071  lgsdir  27072  lgsdilem2  27073  lgsdi  27074  lgsne0  27075  lgsprme0  27079  lgsqr  27091  gausslemma2dlem1a  27105  gausslemma2dlem4  27109  gausslemma2dlem5a  27110  lgseisenlem1  27115  lgseisenlem2  27116  lgseisenlem3  27117  lgseisenlem4  27118  lgseisen  27119  lgsquadlem2  27121  lgsquadlem3  27122  lgsquad2lem2  27125  m1lgs  27128  2lgslem1a  27131  2lgslem1  27134  2lgslem2  27135  2lgsoddprm  27156  2sqlem3  27160  2sqlem4  27161  2sqlem6  27163  2sqlem8  27166  2sqblem  27171  2sqb  27172  2sqmod  27176  rpvmasumlem  27227  dchrisum0flblem1  27248  dchrisum0flblem2  27249  dirith  27269  clwwlkndivn  29601  oddprm2  33966  nn0prpwlem  35511  nn0prpw  35512  rtprmirr  41540  flt4lem5elem  41696  prmunb2  43373  nzprmdif  43381  etransclem48  45297  sfprmdvdsmersenne  46570  sgprmdvdsmersenne  46571  oddprmALTV  46654  oddprmne2  46682  even3prm2  46686  mogoldbblem  46687  sbgoldbst  46745  sbgoldbaltlem1  46746  sbgoldbaltlem2  46747  nnsum3primesprm  46757  nnsum3primesgbe  46759  nnsum4primesodd  46763  nnsum4primesoddALTV  46764  nnsum4primeseven  46767  nnsum4primesevenALTV  46768  bgoldbtbndlem2  46773  bgoldbtbndlem3  46774  bgoldbtbndlem4  46775  bgoldbtbnd  46776  ztprmneprm  47112