Theorem prmz 16732

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℤcz 12590  ℙcprime 16728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pr 5404  ax-un 7732  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-i2m1 11167  ax-1ne0 11168  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3368  df-rab 3415  df-v 3455  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 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  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 7413  df-om 7862  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-neg 11443  df-nn 12233  df-n0 12504  df-z 12591  df-prm 16729

This theorem is referenced by:  dvdsprime  16744  oddprmge3  16758  exprmfct  16762  prmdvdsfz  16763  isprm5  16765  isprm7  16766  maxprmfct  16767  coprm  16769  prmrp  16770  euclemma  16771  prmdvdsexpb  16774  prmexpb  16777  prmfac1  16778  rpexp  16780  cncongrprm  16787  phiprmpw  16834  phiprm  16835  fermltl  16842  prmdiv  16843  prmdiveq  16844  vfermltl  16860  vfermltlALT  16861  reumodprminv  16863  modprm0  16864  oddprm  16869  prm23lt5  16873  prm23ge5  16874  pcneg  16933  pcprmpw2  16941  pcprmpw  16942  difsqpwdvds  16946  pcprod  16954  prmpwdvds  16963  prmunb  16973  prmreclem3  16977  prmreclem5  16979  1arithlem4  16985  1arith  16986  4sqlem11  17014  4sqlem12  17015  4sqlem13  17016  4sqlem14  17017  4sqlem17  17020  prmdvdsprmo  17101  prmdvdsprmop  17102  fvprmselgcd1  17104  prmgaplem4  17113  prmgaplem5  17114  prmgaplem6  17115  prmgaplem8  17117  pgpfi  19674  sylow2alem2  19687  sylow2blem3  19691  gexexlem  19921  ablfacrplem  20136  ablfac1lem  20139  ablfac1b  20141  ablfac1eu  20144  pgpfac1lem2  20146  pgpfac1lem3a  20147  pgpfac1lem3  20148  pgpfac1lem4  20149  ablfaclem3  20158  prmirredlem  21601  rtprmirr  26901  wilthlem1  27208  wilthlem2  27209  ppisval  27244  vmappw  27256  muval1  27273  dvdssqf  27278  mumullem1  27319  mumul  27321  sqff1o  27322  dvdsppwf1o  27326  ppiublem1  27342  ppiublem2  27343  chtublem  27351  vmasum  27356  perfect1  27368  bposlem3  27426  bposlem6  27429  lgslem1  27437  lgsval2lem  27447  lgsvalmod  27456  lgsmod  27463  lgsdirprm  27471  lgsdir  27472  lgsdilem2  27473  lgsdi  27474  lgsne0  27475  lgsprme0  27479  lgsqr  27491  gausslemma2dlem1a  27505  gausslemma2dlem4  27509  gausslemma2dlem5a  27510  lgseisenlem1  27515  lgseisenlem2  27516  lgseisenlem3  27517  lgseisenlem4  27518  lgseisen  27519  lgsquadlem2  27521  lgsquadlem3  27522  lgsquad2lem2  27525  m1lgs  27528  2lgslem1a  27531  2lgslem1  27534  2lgslem2  27535  2lgsoddprm  27556  2sqlem3  27560  2sqlem4  27561  2sqlem6  27563  2sqlem8  27566  2sqblem  27571  2sqb  27572  2sqmod  27576  rpvmasumlem  27627  dchrisum0flblem1  27648  dchrisum0flblem2  27649  dirith  27669  clwwlkndivn  30397  oddprm2  35008  nn0prpwlem  36777  nn0prpw  36778  flt4lem5elem  43331  prmunb2  44969  nzprmdif  44977  etransclem48  46944  sfprmdvdsmersenne  48300  sgprmdvdsmersenne  48301  oddprmALTV  48397  oddprmne2  48425  even3prm2  48429  mogoldbblem  48430  sbgoldbst  48488  sbgoldbaltlem1  48489  sbgoldbaltlem2  48490  nnsum3primesprm  48500  nnsum3primesgbe  48502  nnsum4primesodd  48506  nnsum4primesoddALTV  48507  nnsum4primeseven  48510  nnsum4primesevenALTV  48511  bgoldbtbndlem2  48516  bgoldbtbndlem3  48517  bgoldbtbndlem4  48518  bgoldbtbnd  48519  ztprmneprm  49072