Theorem prmz 16013

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

Syntax hints:   → wi 4   ∈ wcel 2110  ℤcz 11975  ℙcprime 16009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-i2m1 10599  ax-1ne0 10600  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7153  df-om 7575  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-neg 10867  df-nn 11633  df-n0 11892  df-z 11976  df-prm 16010

This theorem is referenced by:  dvdsprime  16025  oddprmge3  16038  exprmfct  16042  prmdvdsfz  16043  isprm5  16045  isprm7  16046  maxprmfct  16047  coprm  16049  prmrp  16050  euclemma  16051  prmdvdsexpb  16054  prmexpb  16056  prmfac1  16057  rpexp  16058  cncongrprm  16063  phiprmpw  16107  phiprm  16108  fermltl  16115  prmdiv  16116  prmdiveq  16117  vfermltl  16132  vfermltlALT  16133  reumodprminv  16135  modprm0  16136  oddprm  16141  prm23lt5  16145  prm23ge5  16146  pcneg  16204  pcprmpw2  16212  pcprmpw  16213  difsqpwdvds  16217  pcprod  16225  prmpwdvds  16234  prmunb  16244  prmreclem3  16248  prmreclem5  16250  1arithlem4  16256  1arith  16257  4sqlem11  16285  4sqlem12  16286  4sqlem13  16287  4sqlem14  16288  4sqlem17  16291  prmdvdsprmo  16372  prmdvdsprmop  16373  fvprmselgcd1  16375  prmgaplem4  16384  prmgaplem5  16385  prmgaplem6  16386  prmgaplem8  16388  pgpfi  18724  sylow2alem2  18737  sylow2blem3  18741  gexexlem  18966  ablfacrplem  19181  ablfac1lem  19184  ablfac1b  19186  ablfac1eu  19189  pgpfac1lem2  19191  pgpfac1lem3a  19192  pgpfac1lem3  19193  pgpfac1lem4  19194  ablfaclem3  19203  prmirredlem  20634  wilthlem1  25639  wilthlem2  25640  ppisval  25675  vmappw  25687  muval1  25704  dvdssqf  25709  mumullem1  25750  mumul  25752  sqff1o  25753  dvdsppwf1o  25757  ppiublem1  25772  ppiublem2  25773  chtublem  25781  vmasum  25786  perfect1  25798  bposlem3  25856  bposlem6  25859  lgslem1  25867  lgsval2lem  25877  lgsvalmod  25886  lgsmod  25893  lgsdirprm  25901  lgsdir  25902  lgsdilem2  25903  lgsdi  25904  lgsne0  25905  lgsprme0  25909  lgsqr  25921  gausslemma2dlem1a  25935  gausslemma2dlem4  25939  gausslemma2dlem5a  25940  lgseisenlem1  25945  lgseisenlem2  25946  lgseisenlem3  25947  lgseisenlem4  25948  lgseisen  25949  lgsquadlem2  25951  lgsquadlem3  25952  lgsquad2lem2  25955  m1lgs  25958  2lgslem1a  25961  2lgslem1  25964  2lgslem2  25965  2lgsoddprm  25986  2sqlem3  25990  2sqlem4  25991  2sqlem6  25993  2sqlem8  25996  2sqblem  26001  2sqb  26002  2sqmod  26006  rpvmasumlem  26057  dchrisum0flblem1  26078  dchrisum0flblem2  26079  dirith  26099  clwwlkndivn  27853  oddprm2  31921  nn0prpwlem  33665  nn0prpw  33666  rtprmirr  39187  prmunb2  40636  nzprmdif  40644  etransclem48  42561  sfprmdvdsmersenne  43762  sgprmdvdsmersenne  43763  oddprmALTV  43846  oddprmne2  43874  even3prm2  43878  mogoldbblem  43879  sbgoldbst  43937  sbgoldbaltlem1  43938  sbgoldbaltlem2  43939  nnsum3primesprm  43949  nnsum3primesgbe  43951  nnsum4primesodd  43955  nnsum4primesoddALTV  43956  nnsum4primeseven  43959  nnsum4primesevenALTV  43960  bgoldbtbndlem2  43965  bgoldbtbndlem3  43966  bgoldbtbndlem4  43967  bgoldbtbnd  43968  ztprmneprm  44389