Theorem prmz 16633

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℤcz 12513  ℙcprime 16629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pr 5364  ax-un 7678  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-i2m1 11095  ax-1ne0 11096  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-ral 3050  df-rex 3060  df-reu 3341  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-tr 5182  df-id 5515  df-eprel 5520  df-po 5528  df-so 5529  df-fr 5573  df-we 5575  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6254  df-ord 6315  df-on 6316  df-lim 6317  df-suc 6318  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-neg 11369  df-nn 12164  df-n0 12427  df-z 12514  df-prm 16630

This theorem is referenced by:  dvdsprime  16645  oddprmge3  16659  exprmfct  16663  prmdvdsfz  16664  isprm5  16666  isprm7  16667  maxprmfct  16668  coprm  16670  prmrp  16671  euclemma  16672  prmdvdsexpb  16675  prmexpb  16678  prmfac1  16679  rpexp  16681  cncongrprm  16688  phiprmpw  16735  phiprm  16736  fermltl  16743  prmdiv  16744  prmdiveq  16745  vfermltl  16761  vfermltlALT  16762  reumodprminv  16764  modprm0  16765  oddprm  16770  prm23lt5  16774  prm23ge5  16775  pcneg  16834  pcprmpw2  16842  pcprmpw  16843  difsqpwdvds  16847  pcprod  16855  prmpwdvds  16864  prmunb  16874  prmreclem3  16878  prmreclem5  16880  1arithlem4  16886  1arith  16887  4sqlem11  16915  4sqlem12  16916  4sqlem13  16917  4sqlem14  16918  4sqlem17  16921  prmdvdsprmo  17002  prmdvdsprmop  17003  fvprmselgcd1  17005  prmgaplem4  17014  prmgaplem5  17015  prmgaplem6  17016  prmgaplem8  17018  pgpfi  19569  sylow2alem2  19582  sylow2blem3  19586  gexexlem  19816  ablfacrplem  20031  ablfac1lem  20034  ablfac1b  20036  ablfac1eu  20039  pgpfac1lem2  20041  pgpfac1lem3a  20042  pgpfac1lem3  20043  pgpfac1lem4  20044  ablfaclem3  20053  prmirredlem  21441  rtprmirr  26712  wilthlem1  27019  wilthlem2  27020  ppisval  27055  vmappw  27067  muval1  27084  dvdssqf  27089  mumullem1  27130  mumul  27132  sqff1o  27133  dvdsppwf1o  27137  ppiublem1  27153  ppiublem2  27154  chtublem  27162  vmasum  27167  perfect1  27179  bposlem3  27237  bposlem6  27240  lgslem1  27248  lgsval2lem  27258  lgsvalmod  27267  lgsmod  27274  lgsdirprm  27282  lgsdir  27283  lgsdilem2  27284  lgsdi  27285  lgsne0  27286  lgsprme0  27290  lgsqr  27302  gausslemma2dlem1a  27316  gausslemma2dlem4  27320  gausslemma2dlem5a  27321  lgseisenlem1  27326  lgseisenlem2  27327  lgseisenlem3  27328  lgseisenlem4  27329  lgseisen  27330  lgsquadlem2  27332  lgsquadlem3  27333  lgsquad2lem2  27336  m1lgs  27339  2lgslem1a  27342  2lgslem1  27345  2lgslem2  27346  2lgsoddprm  27367  2sqlem3  27371  2sqlem4  27372  2sqlem6  27374  2sqlem8  27377  2sqblem  27382  2sqb  27383  2sqmod  27387  rpvmasumlem  27438  dchrisum0flblem1  27459  dchrisum0flblem2  27460  dirith  27480  clwwlkndivn  30138  oddprm2  34787  nn0prpwlem  36492  nn0prpw  36493  flt4lem5elem  43072  prmunb2  44726  nzprmdif  44734  etransclem48  46698  sfprmdvdsmersenne  48054  sgprmdvdsmersenne  48055  oddprmALTV  48151  oddprmne2  48179  even3prm2  48183  mogoldbblem  48184  sbgoldbst  48242  sbgoldbaltlem1  48243  sbgoldbaltlem2  48244  nnsum3primesprm  48254  nnsum3primesgbe  48256  nnsum4primesodd  48260  nnsum4primesoddALTV  48261  nnsum4primeseven  48264  nnsum4primesevenALTV  48265  bgoldbtbndlem2  48270  bgoldbtbndlem3  48271  bgoldbtbndlem4  48272  bgoldbtbnd  48273  ztprmneprm  48811