Theorem prmz 16879

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℤcz 12720  ℙcprime 16875

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7775  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-i2m1 11295  ax-1ne0 11296  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7446  df-om 7902  df-2nd 8026  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-neg 11571  df-nn 12363  df-n0 12634  df-z 12721  df-prm 16876

This theorem is used by:  dvdsprime  16891  oddprmge3  16905  exprmfct  16909  prmdvdsfz  16910  isprm5  16912  isprm7  16913  maxprmfct  16914  coprm  16916  prmrp  16917  euclemma  16918  prmdvdsexpb  16921  prmexpb  16924  prmfac1  16925  rpexp  16927  cncongrprm  16934  phiprmpw  16982  phiprm  16983  fermltl  16990  prmdiv  16991  prmdiveq  16992  vfermltl  17008  vfermltlALT  17009  reumodprminv  17011  modprm0  17012  oddprm  17017  prm23lt5  17021  prm23ge5  17022  pcneg  17081  pcprmpw2  17089  pcprmpw  17090  difsqpwdvds  17094  pcprod  17102  prmpwdvds  17111  prmunb  17121  prmreclem3  17125  prmreclem5  17127  1arithlem4  17133  1arith  17134  4sqlem11  17162  4sqlem12  17163  4sqlem13  17164  4sqlem14  17165  4sqlem17  17168  prmdvdsprmo  17249  prmdvdsprmop  17250  fvprmselgcd1  17252  prmgaplem4  17261  prmgaplem5  17262  prmgaplem6  17263  prmgaplem8  17265  pgpfi  19849  sylow2alem2  19862  sylow2blem3  19866  gexexlem  20096  ablfacrplem  20311  ablfac1lem  20314  ablfac1b  20316  ablfac1eu  20319  pgpfac1lem2  20321  pgpfac1lem3a  20322  pgpfac1lem3  20323  pgpfac1lem4  20324  ablfaclem3  20333  prmirredlem  21808  rtprmirr  27118  wilthlem1  27425  wilthlem2  27426  ppisval  27461  vmappw  27473  muval1  27490  dvdssqf  27495  mumullem1  27536  mumul  27538  sqff1o  27539  dvdsppwf1o  27543  ppiublem1  27559  ppiublem2  27560  chtublem  27568  vmasum  27573  perfect1  27585  bposlem3  27643  bposlem6  27646  lgslem1  27654  lgsval2lem  27664  lgsvalmod  27673  lgsmod  27680  lgsdirprm  27688  lgsdir  27689  lgsdilem2  27690  lgsdi  27691  lgsne0  27692  lgsprme0  27696  lgsqr  27708  gausslemma2dlem1a  27722  gausslemma2dlem4  27726  gausslemma2dlem5a  27727  lgseisenlem1  27732  lgseisenlem2  27733  lgseisenlem3  27734  lgseisenlem4  27735  lgseisen  27736  lgsquadlem2  27738  lgsquadlem3  27739  lgsquad2lem2  27742  m1lgs  27745  2lgslem1a  27748  2lgslem1  27751  2lgslem2  27752  2lgsoddprm  27773  2sqlem3  27777  2sqlem4  27778  2sqlem6  27780  2sqlem8  27783  2sqblem  27788  2sqb  27789  2sqmod  27793  rpvmasumlem  27844  dchrisum0flblem1  27865  dchrisum0flblem2  27866  dirith  27886  flt4lem5elem  28011  fltoprmgt3  28026  clwwlkndivn  30701  oddprm2  35354  nn0prpwlem  37288  nn0prpw  37289  prmunb2  45487  nzprmdif  45495  etransclem48  47497  sfprmdvdsmersenne  48893  sgprmdvdsmersenne  48894  oddprmALTV  48990  oddprmne2  49018  even3prm2  49022  mogoldbblem  49023  sbgoldbst  49081  sbgoldbaltlem1  49082  sbgoldbaltlem2  49083  nnsum3primesprm  49093  nnsum3primesgbe  49095  nnsum4primesodd  49099  nnsum4primesoddALTV  49100  nnsum4primeseven  49103  nnsum4primesevenALTV  49104  bgoldbtbndlem2  49109  bgoldbtbndlem3  49110  bgoldbtbndlem4  49111  bgoldbtbnd  49112  ztprmneprm  49664