Theorem prmz 16644

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℤcz 12524  ℙcprime 16640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5376  ax-un 7689  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6266  df-ord 6327  df-on 6328  df-lim 6329  df-suc 6330  df-iota 6455  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-neg 11380  df-nn 12175  df-n0 12438  df-z 12525  df-prm 16641

This theorem is referenced by:  dvdsprime  16656  oddprmge3  16670  exprmfct  16674  prmdvdsfz  16675  isprm5  16677  isprm7  16678  maxprmfct  16679  coprm  16681  prmrp  16682  euclemma  16683  prmdvdsexpb  16686  prmexpb  16689  prmfac1  16690  rpexp  16692  cncongrprm  16699  phiprmpw  16746  phiprm  16747  fermltl  16754  prmdiv  16755  prmdiveq  16756  vfermltl  16772  vfermltlALT  16773  reumodprminv  16775  modprm0  16776  oddprm  16781  prm23lt5  16785  prm23ge5  16786  pcneg  16845  pcprmpw2  16853  pcprmpw  16854  difsqpwdvds  16858  pcprod  16866  prmpwdvds  16875  prmunb  16885  prmreclem3  16889  prmreclem5  16891  1arithlem4  16897  1arith  16898  4sqlem11  16926  4sqlem12  16927  4sqlem13  16928  4sqlem14  16929  4sqlem17  16932  prmdvdsprmo  17013  prmdvdsprmop  17014  fvprmselgcd1  17016  prmgaplem4  17025  prmgaplem5  17026  prmgaplem6  17027  prmgaplem8  17029  pgpfi  19580  sylow2alem2  19593  sylow2blem3  19597  gexexlem  19827  ablfacrplem  20042  ablfac1lem  20045  ablfac1b  20047  ablfac1eu  20050  pgpfac1lem2  20052  pgpfac1lem3a  20053  pgpfac1lem3  20054  pgpfac1lem4  20055  ablfaclem3  20064  prmirredlem  21452  rtprmirr  26724  wilthlem1  27031  wilthlem2  27032  ppisval  27067  vmappw  27079  muval1  27096  dvdssqf  27101  mumullem1  27142  mumul  27144  sqff1o  27145  dvdsppwf1o  27149  ppiublem1  27165  ppiublem2  27166  chtublem  27174  vmasum  27179  perfect1  27191  bposlem3  27249  bposlem6  27252  lgslem1  27260  lgsval2lem  27270  lgsvalmod  27279  lgsmod  27286  lgsdirprm  27294  lgsdir  27295  lgsdilem2  27296  lgsdi  27297  lgsne0  27298  lgsprme0  27302  lgsqr  27314  gausslemma2dlem1a  27328  gausslemma2dlem4  27332  gausslemma2dlem5a  27333  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgseisenlem4  27341  lgseisen  27342  lgsquadlem2  27344  lgsquadlem3  27345  lgsquad2lem2  27348  m1lgs  27351  2lgslem1a  27354  2lgslem1  27357  2lgslem2  27358  2lgsoddprm  27379  2sqlem3  27383  2sqlem4  27384  2sqlem6  27386  2sqlem8  27389  2sqblem  27394  2sqb  27395  2sqmod  27399  rpvmasumlem  27450  dchrisum0flblem1  27471  dchrisum0flblem2  27472  dirith  27492  clwwlkndivn  30150  oddprm2  34799  nn0prpwlem  36504  nn0prpw  36505  flt4lem5elem  43084  prmunb2  44738  nzprmdif  44746  etransclem48  46710  sfprmdvdsmersenne  48060  sgprmdvdsmersenne  48061  oddprmALTV  48157  oddprmne2  48185  even3prm2  48189  mogoldbblem  48190  sbgoldbst  48248  sbgoldbaltlem1  48249  sbgoldbaltlem2  48250  nnsum3primesprm  48260  nnsum3primesgbe  48262  nnsum4primesodd  48266  nnsum4primesoddALTV  48267  nnsum4primeseven  48270  nnsum4primesevenALTV  48271  bgoldbtbndlem2  48276  bgoldbtbndlem3  48277  bgoldbtbndlem4  48278  bgoldbtbnd  48279  ztprmneprm  48817