Theorem prmz 16719

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℤcz 12578  ℙcprime 16715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pr 5391  ax-un 7718  ax-1cn 11142  ax-icn 11143  ax-addcl 11144  ax-addrcl 11145  ax-mulcl 11146  ax-mulrcl 11147  ax-i2m1 11152  ax-1ne0 11153  ax-rnegex 11155  ax-rrecex 11156  ax-cnre 11157

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5102  df-opab 5164  df-mpt 5183  df-tr 5209  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-ov 7399  df-om 7847  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-neg 11428  df-nn 12221  df-n0 12492  df-z 12579  df-prm 16716

This theorem is referenced by:  dvdsprime  16731  oddprmge3  16745  exprmfct  16749  prmdvdsfz  16750  isprm5  16752  isprm7  16753  maxprmfct  16754  coprm  16756  prmrp  16757  euclemma  16758  prmdvdsexpb  16761  prmexpb  16764  prmfac1  16765  rpexp  16767  cncongrprm  16774  phiprmpw  16821  phiprm  16822  fermltl  16829  prmdiv  16830  prmdiveq  16831  vfermltl  16847  vfermltlALT  16848  reumodprminv  16850  modprm0  16851  oddprm  16856  prm23lt5  16860  prm23ge5  16861  pcneg  16920  pcprmpw2  16928  pcprmpw  16929  difsqpwdvds  16933  pcprod  16941  prmpwdvds  16950  prmunb  16960  prmreclem3  16964  prmreclem5  16966  1arithlem4  16972  1arith  16973  4sqlem11  17001  4sqlem12  17002  4sqlem13  17003  4sqlem14  17004  4sqlem17  17007  prmdvdsprmo  17088  prmdvdsprmop  17089  fvprmselgcd1  17091  prmgaplem4  17100  prmgaplem5  17101  prmgaplem6  17102  prmgaplem8  17104  pgpfi  19655  sylow2alem2  19668  sylow2blem3  19672  gexexlem  19902  ablfacrplem  20117  ablfac1lem  20120  ablfac1b  20122  ablfac1eu  20125  pgpfac1lem2  20127  pgpfac1lem3a  20128  pgpfac1lem3  20129  pgpfac1lem4  20130  ablfaclem3  20139  prmirredlem  21531  rtprmirr  26832  wilthlem1  27139  wilthlem2  27140  ppisval  27175  vmappw  27187  muval1  27204  dvdssqf  27209  mumullem1  27250  mumul  27252  sqff1o  27253  dvdsppwf1o  27257  ppiublem1  27273  ppiublem2  27274  chtublem  27282  vmasum  27287  perfect1  27299  bposlem3  27357  bposlem6  27360  lgslem1  27368  lgsval2lem  27378  lgsvalmod  27387  lgsmod  27394  lgsdirprm  27402  lgsdir  27403  lgsdilem2  27404  lgsdi  27405  lgsne0  27406  lgsprme0  27410  lgsqr  27422  gausslemma2dlem1a  27436  gausslemma2dlem4  27440  gausslemma2dlem5a  27441  lgseisenlem1  27446  lgseisenlem2  27447  lgseisenlem3  27448  lgseisenlem4  27449  lgseisen  27450  lgsquadlem2  27452  lgsquadlem3  27453  lgsquad2lem2  27456  m1lgs  27459  2lgslem1a  27462  2lgslem1  27465  2lgslem2  27466  2lgsoddprm  27487  2sqlem3  27491  2sqlem4  27492  2sqlem6  27494  2sqlem8  27497  2sqblem  27502  2sqb  27503  2sqmod  27507  rpvmasumlem  27558  dchrisum0flblem1  27579  dchrisum0flblem2  27580  dirith  27600  clwwlkndivn  30289  oddprm2  34951  nn0prpwlem  36687  nn0prpw  36688  flt4lem5elem  43238  prmunb2  44878  nzprmdif  44886  etransclem48  46847  sfprmdvdsmersenne  48203  sgprmdvdsmersenne  48204  oddprmALTV  48300  oddprmne2  48328  even3prm2  48332  mogoldbblem  48333  sbgoldbst  48391  sbgoldbaltlem1  48392  sbgoldbaltlem2  48393  nnsum3primesprm  48403  nnsum3primesgbe  48405  nnsum4primesodd  48409  nnsum4primesoddALTV  48410  nnsum4primeseven  48413  nnsum4primesevenALTV  48414  bgoldbtbndlem2  48419  bgoldbtbndlem3  48420  bgoldbtbndlem4  48421  bgoldbtbnd  48422  ztprmneprm  48960