Theorem prmz 16614

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℤcz 12560  ℙcprime 16610

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7727  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-i2m1 11180  ax-1ne0 11181  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  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 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-neg 11449  df-nn 12215  df-n0 12475  df-z 12561  df-prm 16611

This theorem is referenced by:  dvdsprime  16626  oddprmge3  16639  exprmfct  16643  prmdvdsfz  16644  isprm5  16646  isprm7  16647  maxprmfct  16648  coprm  16650  prmrp  16651  euclemma  16652  prmdvdsexpb  16655  prmexpb  16659  prmfac1  16660  rpexp  16661  cncongrprm  16667  phiprmpw  16711  phiprm  16712  fermltl  16719  prmdiv  16720  prmdiveq  16721  vfermltl  16736  vfermltlALT  16737  reumodprminv  16739  modprm0  16740  oddprm  16745  prm23lt5  16749  prm23ge5  16750  pcneg  16809  pcprmpw2  16817  pcprmpw  16818  difsqpwdvds  16822  pcprod  16830  prmpwdvds  16839  prmunb  16849  prmreclem3  16853  prmreclem5  16855  1arithlem4  16861  1arith  16862  4sqlem11  16890  4sqlem12  16891  4sqlem13  16892  4sqlem14  16893  4sqlem17  16896  prmdvdsprmo  16977  prmdvdsprmop  16978  fvprmselgcd1  16980  prmgaplem4  16989  prmgaplem5  16990  prmgaplem6  16991  prmgaplem8  16993  pgpfi  19475  sylow2alem2  19488  sylow2blem3  19492  gexexlem  19722  ablfacrplem  19937  ablfac1lem  19940  ablfac1b  19942  ablfac1eu  19945  pgpfac1lem2  19947  pgpfac1lem3a  19948  pgpfac1lem3  19949  pgpfac1lem4  19950  ablfaclem3  19959  prmirredlem  21048  wilthlem1  26579  wilthlem2  26580  ppisval  26615  vmappw  26627  muval1  26644  dvdssqf  26649  mumullem1  26690  mumul  26692  sqff1o  26693  dvdsppwf1o  26697  ppiublem1  26712  ppiublem2  26713  chtublem  26721  vmasum  26726  perfect1  26738  bposlem3  26796  bposlem6  26799  lgslem1  26807  lgsval2lem  26817  lgsvalmod  26826  lgsmod  26833  lgsdirprm  26841  lgsdir  26842  lgsdilem2  26843  lgsdi  26844  lgsne0  26845  lgsprme0  26849  lgsqr  26861  gausslemma2dlem1a  26875  gausslemma2dlem4  26879  gausslemma2dlem5a  26880  lgseisenlem1  26885  lgseisenlem2  26886  lgseisenlem3  26887  lgseisenlem4  26888  lgseisen  26889  lgsquadlem2  26891  lgsquadlem3  26892  lgsquad2lem2  26895  m1lgs  26898  2lgslem1a  26901  2lgslem1  26904  2lgslem2  26905  2lgsoddprm  26926  2sqlem3  26930  2sqlem4  26931  2sqlem6  26933  2sqlem8  26936  2sqblem  26941  2sqb  26942  2sqmod  26946  rpvmasumlem  26997  dchrisum0flblem1  27018  dchrisum0flblem2  27019  dirith  27039  clwwlkndivn  29371  oddprm2  33736  nn0prpwlem  35299  nn0prpw  35300  rtprmirr  41325  flt4lem5elem  41481  prmunb2  43158  nzprmdif  43166  etransclem48  45083  sfprmdvdsmersenne  46356  sgprmdvdsmersenne  46357  oddprmALTV  46440  oddprmne2  46468  even3prm2  46472  mogoldbblem  46473  sbgoldbst  46531  sbgoldbaltlem1  46532  sbgoldbaltlem2  46533  nnsum3primesprm  46543  nnsum3primesgbe  46545  nnsum4primesodd  46549  nnsum4primesoddALTV  46550  nnsum4primeseven  46553  nnsum4primesevenALTV  46554  bgoldbtbndlem2  46559  bgoldbtbndlem3  46560  bgoldbtbndlem4  46561  bgoldbtbnd  46562  ztprmneprm  47108