Theorem prmz 16850

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℤcz 12693  ℙcprime 16846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-i2m1 11268  ax-1ne0 11269  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  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 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-neg 11544  df-nn 12336  df-n0 12607  df-z 12694  df-prm 16847

This theorem is used by:  dvdsprime  16862  oddprmge3  16876  exprmfct  16880  prmdvdsfz  16881  isprm5  16883  isprm7  16884  maxprmfct  16885  coprm  16887  prmrp  16888  euclemma  16889  prmdvdsexpb  16892  prmexpb  16895  prmfac1  16896  rpexp  16898  cncongrprm  16905  phiprmpw  16953  phiprm  16954  fermltl  16961  prmdiv  16962  prmdiveq  16963  vfermltl  16979  vfermltlALT  16980  reumodprminv  16982  modprm0  16983  oddprm  16988  prm23lt5  16992  prm23ge5  16993  pcneg  17052  pcprmpw2  17060  pcprmpw  17061  difsqpwdvds  17065  pcprod  17073  prmpwdvds  17082  prmunb  17092  prmreclem3  17096  prmreclem5  17098  1arithlem4  17104  1arith  17105  4sqlem11  17133  4sqlem12  17134  4sqlem13  17135  4sqlem14  17136  4sqlem17  17139  prmdvdsprmo  17220  prmdvdsprmop  17221  fvprmselgcd1  17223  prmgaplem4  17232  prmgaplem5  17233  prmgaplem6  17234  prmgaplem8  17236  pgpfi  19819  sylow2alem2  19832  sylow2blem3  19836  gexexlem  20066  ablfacrplem  20281  ablfac1lem  20284  ablfac1b  20286  ablfac1eu  20289  pgpfac1lem2  20291  pgpfac1lem3a  20292  pgpfac1lem3  20293  pgpfac1lem4  20294  ablfaclem3  20303  prmirredlem  21778  rtprmirr  27088  wilthlem1  27395  wilthlem2  27396  ppisval  27431  vmappw  27443  muval1  27460  dvdssqf  27465  mumullem1  27506  mumul  27508  sqff1o  27509  dvdsppwf1o  27513  ppiublem1  27529  ppiublem2  27530  chtublem  27538  vmasum  27543  perfect1  27555  bposlem3  27613  bposlem6  27616  lgslem1  27624  lgsval2lem  27634  lgsvalmod  27643  lgsmod  27650  lgsdirprm  27658  lgsdir  27659  lgsdilem2  27660  lgsdi  27661  lgsne0  27662  lgsprme0  27666  lgsqr  27678  gausslemma2dlem1a  27692  gausslemma2dlem4  27696  gausslemma2dlem5a  27697  lgseisenlem1  27702  lgseisenlem2  27703  lgseisenlem3  27704  lgseisenlem4  27705  lgseisen  27706  lgsquadlem2  27708  lgsquadlem3  27709  lgsquad2lem2  27712  m1lgs  27715  2lgslem1a  27718  2lgslem1  27721  2lgslem2  27722  2lgsoddprm  27743  2sqlem3  27747  2sqlem4  27748  2sqlem6  27750  2sqlem8  27753  2sqblem  27758  2sqb  27759  2sqmod  27763  rpvmasumlem  27814  dchrisum0flblem1  27835  dchrisum0flblem2  27836  dirith  27856  flt4lem5elem  27981  fltoprmgt3  27996  clwwlkndivn  30671  oddprm2  35326  nn0prpwlem  37152  nn0prpw  37153  prmunb2  45338  nzprmdif  45346  etransclem48  47335  sfprmdvdsmersenne  48731  sgprmdvdsmersenne  48732  oddprmALTV  48828  oddprmne2  48856  even3prm2  48860  mogoldbblem  48861  sbgoldbst  48919  sbgoldbaltlem1  48920  sbgoldbaltlem2  48921  nnsum3primesprm  48931  nnsum3primesgbe  48933  nnsum4primesodd  48937  nnsum4primesoddALTV  48938  nnsum4primeseven  48941  nnsum4primesevenALTV  48942  bgoldbtbndlem2  48947  bgoldbtbndlem3  48948  bgoldbtbndlem4  48949  bgoldbtbnd  48950  ztprmneprm  49502