Theorem prmz 16019

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℤcz 11982  ℙcprime 16015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-i2m1 10605  ax-1ne0 10606  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  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 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-neg 10873  df-nn 11639  df-n0 11899  df-z 11983  df-prm 16016

This theorem is referenced by:  dvdsprime  16031  oddprmge3  16044  exprmfct  16048  prmdvdsfz  16049  isprm5  16051  isprm7  16052  maxprmfct  16053  coprm  16055  prmrp  16056  euclemma  16057  prmdvdsexpb  16060  prmexpb  16062  prmfac1  16063  rpexp  16064  cncongrprm  16069  phiprmpw  16113  phiprm  16114  fermltl  16121  prmdiv  16122  prmdiveq  16123  vfermltl  16138  vfermltlALT  16139  reumodprminv  16141  modprm0  16142  oddprm  16147  prm23lt5  16151  prm23ge5  16152  pcneg  16210  pcprmpw2  16218  pcprmpw  16219  difsqpwdvds  16223  pcprod  16231  prmpwdvds  16240  prmunb  16250  prmreclem3  16254  prmreclem5  16256  1arithlem4  16262  1arith  16263  4sqlem11  16291  4sqlem12  16292  4sqlem13  16293  4sqlem14  16294  4sqlem17  16297  prmdvdsprmo  16378  prmdvdsprmop  16379  fvprmselgcd1  16381  prmgaplem4  16390  prmgaplem5  16391  prmgaplem6  16392  prmgaplem8  16394  pgpfi  18730  sylow2alem2  18743  sylow2blem3  18747  gexexlem  18972  ablfacrplem  19187  ablfac1lem  19190  ablfac1b  19192  ablfac1eu  19195  pgpfac1lem2  19197  pgpfac1lem3a  19198  pgpfac1lem3  19199  pgpfac1lem4  19200  ablfaclem3  19209  prmirredlem  20640  wilthlem1  25645  wilthlem2  25646  ppisval  25681  vmappw  25693  muval1  25710  dvdssqf  25715  mumullem1  25756  mumul  25758  sqff1o  25759  dvdsppwf1o  25763  ppiublem1  25778  ppiublem2  25779  chtublem  25787  vmasum  25792  perfect1  25804  bposlem3  25862  bposlem6  25865  lgslem1  25873  lgsval2lem  25883  lgsvalmod  25892  lgsmod  25899  lgsdirprm  25907  lgsdir  25908  lgsdilem2  25909  lgsdi  25910  lgsne0  25911  lgsprme0  25915  lgsqr  25927  gausslemma2dlem1a  25941  gausslemma2dlem4  25945  gausslemma2dlem5a  25946  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem3  25953  lgseisenlem4  25954  lgseisen  25955  lgsquadlem2  25957  lgsquadlem3  25958  lgsquad2lem2  25961  m1lgs  25964  2lgslem1a  25967  2lgslem1  25970  2lgslem2  25971  2lgsoddprm  25992  2sqlem3  25996  2sqlem4  25997  2sqlem6  25999  2sqlem8  26002  2sqblem  26007  2sqb  26008  2sqmod  26012  rpvmasumlem  26063  dchrisum0flblem1  26084  dchrisum0flblem2  26085  dirith  26105  clwwlkndivn  27859  oddprm2  31926  nn0prpwlem  33670  nn0prpw  33671  rtprmirr  39214  prmunb2  40663  nzprmdif  40671  etransclem48  42587  sfprmdvdsmersenne  43788  sgprmdvdsmersenne  43789  oddprmALTV  43872  oddprmne2  43900  even3prm2  43904  mogoldbblem  43905  sbgoldbst  43963  sbgoldbaltlem1  43964  sbgoldbaltlem2  43965  nnsum3primesprm  43975  nnsum3primesgbe  43977  nnsum4primesodd  43981  nnsum4primesoddALTV  43982  nnsum4primeseven  43985  nnsum4primesevenALTV  43986  bgoldbtbndlem2  43991  bgoldbtbndlem3  43992  bgoldbtbndlem4  43993  bgoldbtbnd  43994  ztprmneprm  44415