Theorem prmz 16709

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℤcz 12611  ℙcprime 16705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-i2m1 11221  ax-1ne0 11222  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-om 7888  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-neg 11493  df-nn 12265  df-n0 12525  df-z 12612  df-prm 16706

This theorem is referenced by:  dvdsprime  16721  oddprmge3  16734  exprmfct  16738  prmdvdsfz  16739  isprm5  16741  isprm7  16742  maxprmfct  16743  coprm  16745  prmrp  16746  euclemma  16747  prmdvdsexpb  16750  prmexpb  16753  prmfac1  16754  rpexp  16756  cncongrprm  16763  phiprmpw  16810  phiprm  16811  fermltl  16818  prmdiv  16819  prmdiveq  16820  vfermltl  16835  vfermltlALT  16836  reumodprminv  16838  modprm0  16839  oddprm  16844  prm23lt5  16848  prm23ge5  16849  pcneg  16908  pcprmpw2  16916  pcprmpw  16917  difsqpwdvds  16921  pcprod  16929  prmpwdvds  16938  prmunb  16948  prmreclem3  16952  prmreclem5  16954  1arithlem4  16960  1arith  16961  4sqlem11  16989  4sqlem12  16990  4sqlem13  16991  4sqlem14  16992  4sqlem17  16995  prmdvdsprmo  17076  prmdvdsprmop  17077  fvprmselgcd1  17079  prmgaplem4  17088  prmgaplem5  17089  prmgaplem6  17090  prmgaplem8  17092  pgpfi  19638  sylow2alem2  19651  sylow2blem3  19655  gexexlem  19885  ablfacrplem  20100  ablfac1lem  20103  ablfac1b  20105  ablfac1eu  20108  pgpfac1lem2  20110  pgpfac1lem3a  20111  pgpfac1lem3  20112  pgpfac1lem4  20113  ablfaclem3  20122  prmirredlem  21501  rtprmirr  26818  wilthlem1  27126  wilthlem2  27127  ppisval  27162  vmappw  27174  muval1  27191  dvdssqf  27196  mumullem1  27237  mumul  27239  sqff1o  27240  dvdsppwf1o  27244  ppiublem1  27261  ppiublem2  27262  chtublem  27270  vmasum  27275  perfect1  27287  bposlem3  27345  bposlem6  27348  lgslem1  27356  lgsval2lem  27366  lgsvalmod  27375  lgsmod  27382  lgsdirprm  27390  lgsdir  27391  lgsdilem2  27392  lgsdi  27393  lgsne0  27394  lgsprme0  27398  lgsqr  27410  gausslemma2dlem1a  27424  gausslemma2dlem4  27428  gausslemma2dlem5a  27429  lgseisenlem1  27434  lgseisenlem2  27435  lgseisenlem3  27436  lgseisenlem4  27437  lgseisen  27438  lgsquadlem2  27440  lgsquadlem3  27441  lgsquad2lem2  27444  m1lgs  27447  2lgslem1a  27450  2lgslem1  27453  2lgslem2  27454  2lgsoddprm  27475  2sqlem3  27479  2sqlem4  27480  2sqlem6  27482  2sqlem8  27485  2sqblem  27490  2sqb  27491  2sqmod  27495  rpvmasumlem  27546  dchrisum0flblem1  27567  dchrisum0flblem2  27568  dirith  27588  clwwlkndivn  30109  oddprm2  34649  nn0prpwlem  36305  nn0prpw  36306  flt4lem5elem  42638  prmunb2  44307  nzprmdif  44315  etransclem48  46238  sfprmdvdsmersenne  47528  sgprmdvdsmersenne  47529  oddprmALTV  47612  oddprmne2  47640  even3prm2  47644  mogoldbblem  47645  sbgoldbst  47703  sbgoldbaltlem1  47704  sbgoldbaltlem2  47705  nnsum3primesprm  47715  nnsum3primesgbe  47717  nnsum4primesodd  47721  nnsum4primesoddALTV  47722  nnsum4primeseven  47725  nnsum4primesevenALTV  47726  bgoldbtbndlem2  47731  bgoldbtbndlem3  47732  bgoldbtbndlem4  47733  bgoldbtbnd  47734  ztprmneprm  48192