Theorem prmz 16739

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  ℤcz 12597  ℙcprime 16735

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pr 5403  ax-un 7734  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-i2m1 11174  ax-1ne0 11175  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7415  df-om 7861  df-2nd 7985  df-frecs 8276  df-wrecs 8307  df-recs 8356  df-rdg 8395  df-neg 11450  df-nn 12240  df-n0 12511  df-z 12598  df-prm 16736

This theorem is used by:  dvdsprime  16751  oddprmge3  16765  exprmfct  16769  prmdvdsfz  16770  isprm5  16772  isprm7  16773  maxprmfct  16774  coprm  16776  prmrp  16777  euclemma  16778  prmdvdsexpb  16781  prmexpb  16784  prmfac1  16785  rpexp  16787  cncongrprm  16794  phiprmpw  16841  phiprm  16842  fermltl  16849  prmdiv  16850  prmdiveq  16851  vfermltl  16867  vfermltlALT  16868  reumodprminv  16870  modprm0  16871  oddprm  16876  prm23lt5  16880  prm23ge5  16881  pcneg  16940  pcprmpw2  16948  pcprmpw  16949  difsqpwdvds  16953  pcprod  16961  prmpwdvds  16970  prmunb  16980  prmreclem3  16984  prmreclem5  16986  1arithlem4  16992  1arith  16993  4sqlem11  17021  4sqlem12  17022  4sqlem13  17023  4sqlem14  17024  4sqlem17  17027  prmdvdsprmo  17108  prmdvdsprmop  17109  fvprmselgcd1  17111  prmgaplem4  17120  prmgaplem5  17121  prmgaplem6  17122  prmgaplem8  17124  pgpfi  19681  sylow2alem2  19694  sylow2blem3  19698  gexexlem  19928  ablfacrplem  20143  ablfac1lem  20146  ablfac1b  20148  ablfac1eu  20151  pgpfac1lem2  20153  pgpfac1lem3a  20154  pgpfac1lem3  20155  pgpfac1lem4  20156  ablfaclem3  20165  prmirredlem  21633  rtprmirr  26936  wilthlem1  27243  wilthlem2  27244  ppisval  27279  vmappw  27291  muval1  27308  dvdssqf  27313  mumullem1  27354  mumul  27356  sqff1o  27357  dvdsppwf1o  27361  ppiublem1  27377  ppiublem2  27378  chtublem  27386  vmasum  27391  perfect1  27403  bposlem3  27461  bposlem6  27464  lgslem1  27472  lgsval2lem  27482  lgsvalmod  27491  lgsmod  27498  lgsdirprm  27506  lgsdir  27507  lgsdilem2  27508  lgsdi  27509  lgsne0  27510  lgsprme0  27514  lgsqr  27526  gausslemma2dlem1a  27540  gausslemma2dlem4  27544  gausslemma2dlem5a  27545  lgseisenlem1  27550  lgseisenlem2  27551  lgseisenlem3  27552  lgseisenlem4  27553  lgseisen  27554  lgsquadlem2  27556  lgsquadlem3  27557  lgsquad2lem2  27560  m1lgs  27563  2lgslem1a  27566  2lgslem1  27569  2lgslem2  27570  2lgsoddprm  27591  2sqlem3  27595  2sqlem4  27596  2sqlem6  27598  2sqlem8  27601  2sqblem  27606  2sqb  27607  2sqmod  27611  rpvmasumlem  27662  dchrisum0flblem1  27683  dchrisum0flblem2  27684  dirith  27704  clwwlkndivn  30442  oddprm2  35051  nn0prpwlem  36861  nn0prpw  36862  flt4lem5elem  43411  prmunb2  45049  nzprmdif  45057  etransclem48  47024  sfprmdvdsmersenne  48383  sgprmdvdsmersenne  48384  oddprmALTV  48480  oddprmne2  48508  even3prm2  48512  mogoldbblem  48513  sbgoldbst  48571  sbgoldbaltlem1  48572  sbgoldbaltlem2  48573  nnsum3primesprm  48583  nnsum3primesgbe  48585  nnsum4primesodd  48589  nnsum4primesoddALTV  48590  nnsum4primeseven  48593  nnsum4primesevenALTV  48594  bgoldbtbndlem2  48599  bgoldbtbndlem3  48600  bgoldbtbndlem4  48601  bgoldbtbnd  48602  ztprmneprm  49155