Theorem prmz 16603

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℤcz 12489  ℙcprime 16599

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 5231  ax-nul 5241  ax-pr 5368  ax-un 7680  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-i2m1 11095  ax-1ne0 11096  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100

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 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8222  df-wrecs 8253  df-recs 8302  df-rdg 8340  df-neg 11368  df-nn 12147  df-n0 12403  df-z 12490  df-prm 16600

This theorem is referenced by:  dvdsprime  16615  oddprmge3  16628  exprmfct  16632  prmdvdsfz  16633  isprm5  16635  isprm7  16636  maxprmfct  16637  coprm  16639  prmrp  16640  euclemma  16641  prmdvdsexpb  16644  prmexpb  16647  prmfac1  16648  rpexp  16650  cncongrprm  16657  phiprmpw  16704  phiprm  16705  fermltl  16712  prmdiv  16713  prmdiveq  16714  vfermltl  16730  vfermltlALT  16731  reumodprminv  16733  modprm0  16734  oddprm  16739  prm23lt5  16743  prm23ge5  16744  pcneg  16803  pcprmpw2  16811  pcprmpw  16812  difsqpwdvds  16816  pcprod  16824  prmpwdvds  16833  prmunb  16843  prmreclem3  16847  prmreclem5  16849  1arithlem4  16855  1arith  16856  4sqlem11  16884  4sqlem12  16885  4sqlem13  16886  4sqlem14  16887  4sqlem17  16890  prmdvdsprmo  16971  prmdvdsprmop  16972  fvprmselgcd1  16974  prmgaplem4  16983  prmgaplem5  16984  prmgaplem6  16985  prmgaplem8  16987  pgpfi  19538  sylow2alem2  19551  sylow2blem3  19555  gexexlem  19785  ablfacrplem  20000  ablfac1lem  20003  ablfac1b  20005  ablfac1eu  20008  pgpfac1lem2  20010  pgpfac1lem3a  20011  pgpfac1lem3  20012  pgpfac1lem4  20013  ablfaclem3  20022  prmirredlem  21429  rtprmirr  26710  wilthlem1  27018  wilthlem2  27019  ppisval  27054  vmappw  27066  muval1  27083  dvdssqf  27088  mumullem1  27129  mumul  27131  sqff1o  27132  dvdsppwf1o  27136  ppiublem1  27153  ppiublem2  27154  chtublem  27162  vmasum  27167  perfect1  27179  bposlem3  27237  bposlem6  27240  lgslem1  27248  lgsval2lem  27258  lgsvalmod  27267  lgsmod  27274  lgsdirprm  27282  lgsdir  27283  lgsdilem2  27284  lgsdi  27285  lgsne0  27286  lgsprme0  27290  lgsqr  27302  gausslemma2dlem1a  27316  gausslemma2dlem4  27320  gausslemma2dlem5a  27321  lgseisenlem1  27326  lgseisenlem2  27327  lgseisenlem3  27328  lgseisenlem4  27329  lgseisen  27330  lgsquadlem2  27332  lgsquadlem3  27333  lgsquad2lem2  27336  m1lgs  27339  2lgslem1a  27342  2lgslem1  27345  2lgslem2  27346  2lgsoddprm  27367  2sqlem3  27371  2sqlem4  27372  2sqlem6  27374  2sqlem8  27377  2sqblem  27382  2sqb  27383  2sqmod  27387  rpvmasumlem  27438  dchrisum0flblem1  27459  dchrisum0flblem2  27460  dirith  27480  clwwlkndivn  30139  oddprm2  34805  nn0prpwlem  36510  nn0prpw  36511  flt4lem5elem  43083  prmunb2  44741  nzprmdif  44749  etransclem48  46714  sfprmdvdsmersenne  48037  sgprmdvdsmersenne  48038  oddprmALTV  48121  oddprmne2  48149  even3prm2  48153  mogoldbblem  48154  sbgoldbst  48212  sbgoldbaltlem1  48213  sbgoldbaltlem2  48214  nnsum3primesprm  48224  nnsum3primesgbe  48226  nnsum4primesodd  48230  nnsum4primesoddALTV  48231  nnsum4primeseven  48234  nnsum4primesevenALTV  48235  bgoldbtbndlem2  48240  bgoldbtbndlem3  48241  bgoldbtbndlem4  48242  bgoldbtbnd  48243  ztprmneprm  48781