Theorem prmz 16637

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

Syntax hints:   → wi 4   ∈ wcel 2099  ℤcz 12580  ℙcprime 16633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7734  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-i2m1 11198  ax-1ne0 11199  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-om 7865  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-neg 11469  df-nn 12235  df-n0 12495  df-z 12581  df-prm 16634

This theorem is referenced by:  dvdsprime  16649  oddprmge3  16662  exprmfct  16666  prmdvdsfz  16667  isprm5  16669  isprm7  16670  maxprmfct  16671  coprm  16673  prmrp  16674  euclemma  16675  prmdvdsexpb  16678  prmexpb  16682  prmfac1  16683  rpexp  16685  cncongrprm  16692  phiprmpw  16736  phiprm  16737  fermltl  16744  prmdiv  16745  prmdiveq  16746  vfermltl  16761  vfermltlALT  16762  reumodprminv  16764  modprm0  16765  oddprm  16770  prm23lt5  16774  prm23ge5  16775  pcneg  16834  pcprmpw2  16842  pcprmpw  16843  difsqpwdvds  16847  pcprod  16855  prmpwdvds  16864  prmunb  16874  prmreclem3  16878  prmreclem5  16880  1arithlem4  16886  1arith  16887  4sqlem11  16915  4sqlem12  16916  4sqlem13  16917  4sqlem14  16918  4sqlem17  16921  prmdvdsprmo  17002  prmdvdsprmop  17003  fvprmselgcd1  17005  prmgaplem4  17014  prmgaplem5  17015  prmgaplem6  17016  prmgaplem8  17018  pgpfi  19551  sylow2alem2  19564  sylow2blem3  19568  gexexlem  19798  ablfacrplem  20013  ablfac1lem  20016  ablfac1b  20018  ablfac1eu  20021  pgpfac1lem2  20023  pgpfac1lem3a  20024  pgpfac1lem3  20025  pgpfac1lem4  20026  ablfaclem3  20035  prmirredlem  21385  wilthlem1  26987  wilthlem2  26988  ppisval  27023  vmappw  27035  muval1  27052  dvdssqf  27057  mumullem1  27098  mumul  27100  sqff1o  27101  dvdsppwf1o  27105  ppiublem1  27122  ppiublem2  27123  chtublem  27131  vmasum  27136  perfect1  27148  bposlem3  27206  bposlem6  27209  lgslem1  27217  lgsval2lem  27227  lgsvalmod  27236  lgsmod  27243  lgsdirprm  27251  lgsdir  27252  lgsdilem2  27253  lgsdi  27254  lgsne0  27255  lgsprme0  27259  lgsqr  27271  gausslemma2dlem1a  27285  gausslemma2dlem4  27289  gausslemma2dlem5a  27290  lgseisenlem1  27295  lgseisenlem2  27296  lgseisenlem3  27297  lgseisenlem4  27298  lgseisen  27299  lgsquadlem2  27301  lgsquadlem3  27302  lgsquad2lem2  27305  m1lgs  27308  2lgslem1a  27311  2lgslem1  27314  2lgslem2  27315  2lgsoddprm  27336  2sqlem3  27340  2sqlem4  27341  2sqlem6  27343  2sqlem8  27346  2sqblem  27351  2sqb  27352  2sqmod  27356  rpvmasumlem  27407  dchrisum0flblem1  27428  dchrisum0flblem2  27429  dirith  27449  clwwlkndivn  29877  oddprm2  34223  nn0prpwlem  35742  nn0prpw  35743  rtprmirr  41828  flt4lem5elem  41997  prmunb2  43671  nzprmdif  43679  etransclem48  45593  sfprmdvdsmersenne  46866  sgprmdvdsmersenne  46867  oddprmALTV  46950  oddprmne2  46978  even3prm2  46982  mogoldbblem  46983  sbgoldbst  47041  sbgoldbaltlem1  47042  sbgoldbaltlem2  47043  nnsum3primesprm  47053  nnsum3primesgbe  47055  nnsum4primesodd  47059  nnsum4primesoddALTV  47060  nnsum4primeseven  47063  nnsum4primesevenALTV  47064  bgoldbtbndlem2  47069  bgoldbtbndlem3  47070  bgoldbtbndlem4  47071  bgoldbtbnd  47072  ztprmneprm  47334