Theorem prmz 16758

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℤcz 12609  ℙcprime 16754

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-i2m1 11186  ax-1ne0 11187  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7426  df-om 7872  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-neg 11462  df-nn 12252  df-n0 12523  df-z 12610  df-prm 16755

This theorem is used by:  dvdsprime  16770  oddprmge3  16784  exprmfct  16788  prmdvdsfz  16789  isprm5  16791  isprm7  16792  maxprmfct  16793  coprm  16795  prmrp  16796  euclemma  16797  prmdvdsexpb  16800  prmexpb  16803  prmfac1  16804  rpexp  16806  cncongrprm  16813  phiprmpw  16860  phiprm  16861  fermltl  16868  prmdiv  16869  prmdiveq  16870  vfermltl  16886  vfermltlALT  16887  reumodprminv  16889  modprm0  16890  oddprm  16895  prm23lt5  16899  prm23ge5  16900  pcneg  16959  pcprmpw2  16967  pcprmpw  16968  difsqpwdvds  16972  pcprod  16980  prmpwdvds  16989  prmunb  16999  prmreclem3  17003  prmreclem5  17005  1arithlem4  17011  1arith  17012  4sqlem11  17040  4sqlem12  17041  4sqlem13  17042  4sqlem14  17043  4sqlem17  17046  prmdvdsprmo  17127  prmdvdsprmop  17128  fvprmselgcd1  17130  prmgaplem4  17139  prmgaplem5  17140  prmgaplem6  17141  prmgaplem8  17143  pgpfi  19700  sylow2alem2  19713  sylow2blem3  19717  gexexlem  19947  ablfacrplem  20162  ablfac1lem  20165  ablfac1b  20167  ablfac1eu  20170  pgpfac1lem2  20172  pgpfac1lem3a  20173  pgpfac1lem3  20174  pgpfac1lem4  20175  ablfaclem3  20184  prmirredlem  21652  rtprmirr  26955  wilthlem1  27262  wilthlem2  27263  ppisval  27298  vmappw  27310  muval1  27327  dvdssqf  27332  mumullem1  27373  mumul  27375  sqff1o  27376  dvdsppwf1o  27380  ppiublem1  27396  ppiublem2  27397  chtublem  27405  vmasum  27410  perfect1  27422  bposlem3  27480  bposlem6  27483  lgslem1  27491  lgsval2lem  27501  lgsvalmod  27510  lgsmod  27517  lgsdirprm  27525  lgsdir  27526  lgsdilem2  27527  lgsdi  27528  lgsne0  27529  lgsprme0  27533  lgsqr  27545  gausslemma2dlem1a  27559  gausslemma2dlem4  27563  gausslemma2dlem5a  27564  lgseisenlem1  27569  lgseisenlem2  27570  lgseisenlem3  27571  lgseisenlem4  27572  lgseisen  27573  lgsquadlem2  27575  lgsquadlem3  27576  lgsquad2lem2  27579  m1lgs  27582  2lgslem1a  27585  2lgslem1  27588  2lgslem2  27589  2lgsoddprm  27610  2sqlem3  27614  2sqlem4  27615  2sqlem6  27617  2sqlem8  27620  2sqblem  27625  2sqb  27626  2sqmod  27630  rpvmasumlem  27681  dchrisum0flblem1  27702  dchrisum0flblem2  27703  dirith  27723  clwwlkndivn  30461  oddprm2  35066  nn0prpwlem  36866  nn0prpw  36867  flt4lem5elem  43416  prmunb2  45054  nzprmdif  45062  etransclem48  47029  sfprmdvdsmersenne  48388  sgprmdvdsmersenne  48389  oddprmALTV  48485  oddprmne2  48513  even3prm2  48517  mogoldbblem  48518  sbgoldbst  48576  sbgoldbaltlem1  48577  sbgoldbaltlem2  48578  nnsum3primesprm  48588  nnsum3primesgbe  48590  nnsum4primesodd  48594  nnsum4primesoddALTV  48595  nnsum4primeseven  48598  nnsum4primesevenALTV  48599  bgoldbtbndlem2  48604  bgoldbtbndlem3  48605  bgoldbtbndlem4  48606  bgoldbtbnd  48607  ztprmneprm  49160