Theorem prmz 16607

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℤcz 12493  ℙcprime 16603

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 5242  ax-nul 5252  ax-pr 5378  ax-un 7683  ax-1cn 11089  ax-icn 11090  ax-addcl 11091  ax-addrcl 11092  ax-mulcl 11093  ax-mulrcl 11094  ax-i2m1 11099  ax-1ne0 11100  ax-rnegex 11102  ax-rrecex 11103  ax-cnre 11104

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 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7364  df-om 7812  df-2nd 7937  df-frecs 8226  df-wrecs 8257  df-recs 8306  df-rdg 8344  df-neg 11372  df-nn 12151  df-n0 12407  df-z 12494  df-prm 16604

This theorem is referenced by:  dvdsprime  16619  oddprmge3  16632  exprmfct  16636  prmdvdsfz  16637  isprm5  16639  isprm7  16640  maxprmfct  16641  coprm  16643  prmrp  16644  euclemma  16645  prmdvdsexpb  16648  prmexpb  16651  prmfac1  16652  rpexp  16654  cncongrprm  16661  phiprmpw  16708  phiprm  16709  fermltl  16716  prmdiv  16717  prmdiveq  16718  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  19539  sylow2alem2  19552  sylow2blem3  19556  gexexlem  19786  ablfacrplem  20001  ablfac1lem  20004  ablfac1b  20006  ablfac1eu  20009  pgpfac1lem2  20011  pgpfac1lem3a  20012  pgpfac1lem3  20013  pgpfac1lem4  20014  ablfaclem3  20023  prmirredlem  21432  rtprmirr  26731  wilthlem1  27039  wilthlem2  27040  ppisval  27075  vmappw  27087  muval1  27104  dvdssqf  27109  mumullem1  27150  mumul  27152  sqff1o  27153  dvdsppwf1o  27157  ppiublem1  27174  ppiublem2  27175  chtublem  27183  vmasum  27188  perfect1  27200  bposlem3  27258  bposlem6  27261  lgslem1  27269  lgsval2lem  27279  lgsvalmod  27288  lgsmod  27295  lgsdirprm  27303  lgsdir  27304  lgsdilem2  27305  lgsdi  27306  lgsne0  27307  lgsprme0  27311  lgsqr  27323  gausslemma2dlem1a  27337  gausslemma2dlem4  27341  gausslemma2dlem5a  27342  lgseisenlem1  27347  lgseisenlem2  27348  lgseisenlem3  27349  lgseisenlem4  27350  lgseisen  27351  lgsquadlem2  27353  lgsquadlem3  27354  lgsquad2lem2  27357  m1lgs  27360  2lgslem1a  27363  2lgslem1  27366  2lgslem2  27367  2lgsoddprm  27388  2sqlem3  27392  2sqlem4  27393  2sqlem6  27395  2sqlem8  27398  2sqblem  27403  2sqb  27404  2sqmod  27408  rpvmasumlem  27459  dchrisum0flblem1  27480  dchrisum0flblem2  27481  dirith  27501  clwwlkndivn  30160  oddprm2  34825  nn0prpwlem  36529  nn0prpw  36530  flt4lem5elem  42972  prmunb2  44630  nzprmdif  44638  etransclem48  46603  sfprmdvdsmersenne  47926  sgprmdvdsmersenne  47927  oddprmALTV  48010  oddprmne2  48038  even3prm2  48042  mogoldbblem  48043  sbgoldbst  48101  sbgoldbaltlem1  48102  sbgoldbaltlem2  48103  nnsum3primesprm  48113  nnsum3primesgbe  48115  nnsum4primesodd  48119  nnsum4primesoddALTV  48120  nnsum4primeseven  48123  nnsum4primesevenALTV  48124  bgoldbtbndlem2  48129  bgoldbtbndlem3  48130  bgoldbtbndlem4  48131  bgoldbtbnd  48132  ztprmneprm  48670