Theorem prmz 16722

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℤcz 12639  ℙcprime 16718

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-neg 11523  df-nn 12294  df-n0 12554  df-z 12640  df-prm 16719

This theorem is referenced by:  dvdsprime  16734  oddprmge3  16747  exprmfct  16751  prmdvdsfz  16752  isprm5  16754  isprm7  16755  maxprmfct  16756  coprm  16758  prmrp  16759  euclemma  16760  prmdvdsexpb  16763  prmexpb  16766  prmfac1  16767  rpexp  16769  cncongrprm  16776  phiprmpw  16823  phiprm  16824  fermltl  16831  prmdiv  16832  prmdiveq  16833  vfermltl  16848  vfermltlALT  16849  reumodprminv  16851  modprm0  16852  oddprm  16857  prm23lt5  16861  prm23ge5  16862  pcneg  16921  pcprmpw2  16929  pcprmpw  16930  difsqpwdvds  16934  pcprod  16942  prmpwdvds  16951  prmunb  16961  prmreclem3  16965  prmreclem5  16967  1arithlem4  16973  1arith  16974  4sqlem11  17002  4sqlem12  17003  4sqlem13  17004  4sqlem14  17005  4sqlem17  17008  prmdvdsprmo  17089  prmdvdsprmop  17090  fvprmselgcd1  17092  prmgaplem4  17101  prmgaplem5  17102  prmgaplem6  17103  prmgaplem8  17105  pgpfi  19647  sylow2alem2  19660  sylow2blem3  19664  gexexlem  19894  ablfacrplem  20109  ablfac1lem  20112  ablfac1b  20114  ablfac1eu  20117  pgpfac1lem2  20119  pgpfac1lem3a  20120  pgpfac1lem3  20121  pgpfac1lem4  20122  ablfaclem3  20131  prmirredlem  21506  rtprmirr  26821  wilthlem1  27129  wilthlem2  27130  ppisval  27165  vmappw  27177  muval1  27194  dvdssqf  27199  mumullem1  27240  mumul  27242  sqff1o  27243  dvdsppwf1o  27247  ppiublem1  27264  ppiublem2  27265  chtublem  27273  vmasum  27278  perfect1  27290  bposlem3  27348  bposlem6  27351  lgslem1  27359  lgsval2lem  27369  lgsvalmod  27378  lgsmod  27385  lgsdirprm  27393  lgsdir  27394  lgsdilem2  27395  lgsdi  27396  lgsne0  27397  lgsprme0  27401  lgsqr  27413  gausslemma2dlem1a  27427  gausslemma2dlem4  27431  gausslemma2dlem5a  27432  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem3  27439  lgseisenlem4  27440  lgseisen  27441  lgsquadlem2  27443  lgsquadlem3  27444  lgsquad2lem2  27447  m1lgs  27450  2lgslem1a  27453  2lgslem1  27456  2lgslem2  27457  2lgsoddprm  27478  2sqlem3  27482  2sqlem4  27483  2sqlem6  27485  2sqlem8  27488  2sqblem  27493  2sqb  27494  2sqmod  27498  rpvmasumlem  27549  dchrisum0flblem1  27570  dchrisum0flblem2  27571  dirith  27591  clwwlkndivn  30112  oddprm2  34632  nn0prpwlem  36288  nn0prpw  36289  flt4lem5elem  42606  prmunb2  44280  nzprmdif  44288  etransclem48  46203  sfprmdvdsmersenne  47477  sgprmdvdsmersenne  47478  oddprmALTV  47561  oddprmne2  47589  even3prm2  47593  mogoldbblem  47594  sbgoldbst  47652  sbgoldbaltlem1  47653  sbgoldbaltlem2  47654  nnsum3primesprm  47664  nnsum3primesgbe  47666  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbndlem4  47682  bgoldbtbnd  47683  ztprmneprm  48072