Theorem prmz 16812

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℤcz 12662  ℙcprime 16808

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7734  ax-1cn 11229  ax-icn 11230  ax-addcl 11231  ax-addrcl 11232  ax-mulcl 11233  ax-mulrcl 11234  ax-i2m1 11239  ax-1ne0 11240  ax-rnegex 11242  ax-rrecex 11243  ax-cnre 11244

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6293  df-ord 6354  df-on 6355  df-lim 6356  df-suc 6357  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-ov 7411  df-om 7861  df-2nd 7985  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-neg 11515  df-nn 12305  df-n0 12576  df-z 12663  df-prm 16809

This theorem is used by:  dvdsprime  16824  oddprmge3  16838  exprmfct  16842  prmdvdsfz  16843  isprm5  16845  isprm7  16846  maxprmfct  16847  coprm  16849  prmrp  16850  euclemma  16851  prmdvdsexpb  16854  prmexpb  16857  prmfac1  16858  rpexp  16860  cncongrprm  16867  phiprmpw  16914  phiprm  16915  fermltl  16922  prmdiv  16923  prmdiveq  16924  vfermltl  16940  vfermltlALT  16941  reumodprminv  16943  modprm0  16944  oddprm  16949  prm23lt5  16953  prm23ge5  16954  pcneg  17013  pcprmpw2  17021  pcprmpw  17022  difsqpwdvds  17026  pcprod  17034  prmpwdvds  17043  prmunb  17053  prmreclem3  17057  prmreclem5  17059  1arithlem4  17065  1arith  17066  4sqlem11  17094  4sqlem12  17095  4sqlem13  17096  4sqlem14  17097  4sqlem17  17100  prmdvdsprmo  17181  prmdvdsprmop  17182  fvprmselgcd1  17184  prmgaplem4  17193  prmgaplem5  17194  prmgaplem6  17195  prmgaplem8  17197  pgpfi  19780  sylow2alem2  19793  sylow2blem3  19797  gexexlem  20027  ablfacrplem  20242  ablfac1lem  20245  ablfac1b  20247  ablfac1eu  20250  pgpfac1lem2  20252  pgpfac1lem3a  20253  pgpfac1lem3  20254  pgpfac1lem4  20255  ablfaclem3  20264  prmirredlem  21739  rtprmirr  27051  wilthlem1  27358  wilthlem2  27359  ppisval  27394  vmappw  27406  muval1  27423  dvdssqf  27428  mumullem1  27469  mumul  27471  sqff1o  27472  dvdsppwf1o  27476  ppiublem1  27492  ppiublem2  27493  chtublem  27501  vmasum  27506  perfect1  27518  bposlem3  27576  bposlem6  27579  lgslem1  27587  lgsval2lem  27597  lgsvalmod  27606  lgsmod  27613  lgsdirprm  27621  lgsdir  27622  lgsdilem2  27623  lgsdi  27624  lgsne0  27625  lgsprme0  27629  lgsqr  27641  gausslemma2dlem1a  27655  gausslemma2dlem4  27659  gausslemma2dlem5a  27660  lgseisenlem1  27665  lgseisenlem2  27666  lgseisenlem3  27667  lgseisenlem4  27668  lgseisen  27669  lgsquadlem2  27671  lgsquadlem3  27672  lgsquad2lem2  27675  m1lgs  27678  2lgslem1a  27681  2lgslem1  27684  2lgslem2  27685  2lgsoddprm  27706  2sqlem3  27710  2sqlem4  27711  2sqlem6  27713  2sqlem8  27716  2sqblem  27721  2sqb  27722  2sqmod  27726  rpvmasumlem  27777  dchrisum0flblem1  27798  dchrisum0flblem2  27799  dirith  27819  clwwlkndivn  30604  oddprm2  35218  nn0prpwlem  37032  nn0prpw  37033  flt4lem5elem  43601  prmunb2  45239  nzprmdif  45247  etransclem48  47214  sfprmdvdsmersenne  48610  sgprmdvdsmersenne  48611  oddprmALTV  48707  oddprmne2  48735  even3prm2  48739  mogoldbblem  48740  sbgoldbst  48798  sbgoldbaltlem1  48799  sbgoldbaltlem2  48800  nnsum3primesprm  48810  nnsum3primesgbe  48812  nnsum4primesodd  48816  nnsum4primesoddALTV  48817  nnsum4primeseven  48820  nnsum4primesevenALTV  48821  bgoldbtbndlem2  48826  bgoldbtbndlem3  48827  bgoldbtbndlem4  48828  bgoldbtbnd  48829  ztprmneprm  49381