Theorem prmz 16009

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℤcz 11969  ℙcprime 16005

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-i2m1 10594  ax-1ne0 10595  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-om 7561  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-neg 10862  df-nn 11626  df-n0 11886  df-z 11970  df-prm 16006

This theorem is referenced by:  dvdsprime  16021  oddprmge3  16034  exprmfct  16038  prmdvdsfz  16039  isprm5  16041  isprm7  16042  maxprmfct  16043  coprm  16045  prmrp  16046  euclemma  16047  prmdvdsexpb  16050  prmexpb  16052  prmfac1  16053  rpexp  16054  cncongrprm  16059  phiprmpw  16103  phiprm  16104  fermltl  16111  prmdiv  16112  prmdiveq  16113  vfermltl  16128  vfermltlALT  16129  reumodprminv  16131  modprm0  16132  oddprm  16137  prm23lt5  16141  prm23ge5  16142  pcneg  16200  pcprmpw2  16208  pcprmpw  16209  difsqpwdvds  16213  pcprod  16221  prmpwdvds  16230  prmunb  16240  prmreclem3  16244  prmreclem5  16246  1arithlem4  16252  1arith  16253  4sqlem11  16281  4sqlem12  16282  4sqlem13  16283  4sqlem14  16284  4sqlem17  16287  prmdvdsprmo  16368  prmdvdsprmop  16369  fvprmselgcd1  16371  prmgaplem4  16380  prmgaplem5  16381  prmgaplem6  16382  prmgaplem8  16384  pgpfi  18722  sylow2alem2  18735  sylow2blem3  18739  gexexlem  18965  ablfacrplem  19180  ablfac1lem  19183  ablfac1b  19185  ablfac1eu  19188  pgpfac1lem2  19190  pgpfac1lem3a  19191  pgpfac1lem3  19192  pgpfac1lem4  19193  ablfaclem3  19202  prmirredlem  20186  wilthlem1  25653  wilthlem2  25654  ppisval  25689  vmappw  25701  muval1  25718  dvdssqf  25723  mumullem1  25764  mumul  25766  sqff1o  25767  dvdsppwf1o  25771  ppiublem1  25786  ppiublem2  25787  chtublem  25795  vmasum  25800  perfect1  25812  bposlem3  25870  bposlem6  25873  lgslem1  25881  lgsval2lem  25891  lgsvalmod  25900  lgsmod  25907  lgsdirprm  25915  lgsdir  25916  lgsdilem2  25917  lgsdi  25918  lgsne0  25919  lgsprme0  25923  lgsqr  25935  gausslemma2dlem1a  25949  gausslemma2dlem4  25953  gausslemma2dlem5a  25954  lgseisenlem1  25959  lgseisenlem2  25960  lgseisenlem3  25961  lgseisenlem4  25962  lgseisen  25963  lgsquadlem2  25965  lgsquadlem3  25966  lgsquad2lem2  25969  m1lgs  25972  2lgslem1a  25975  2lgslem1  25978  2lgslem2  25979  2lgsoddprm  26000  2sqlem3  26004  2sqlem4  26005  2sqlem6  26007  2sqlem8  26010  2sqblem  26015  2sqb  26016  2sqmod  26020  rpvmasumlem  26071  dchrisum0flblem1  26092  dchrisum0flblem2  26093  dirith  26113  clwwlkndivn  27865  oddprm2  32036  nn0prpwlem  33783  nn0prpw  33784  rtprmirr  39502  prmunb2  41015  nzprmdif  41023  etransclem48  42924  sfprmdvdsmersenne  44121  sgprmdvdsmersenne  44122  oddprmALTV  44205  oddprmne2  44233  even3prm2  44237  mogoldbblem  44238  sbgoldbst  44296  sbgoldbaltlem1  44297  sbgoldbaltlem2  44298  nnsum3primesprm  44308  nnsum3primesgbe  44310  nnsum4primesodd  44314  nnsum4primesoddALTV  44315  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  bgoldbtbndlem2  44324  bgoldbtbndlem3  44325  bgoldbtbndlem4  44326  bgoldbtbnd  44327  ztprmneprm  44749