Theorem prmz 15798

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℤcz 11732  ℙcprime 15794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-i2m1 10342  ax-1ne0 10343  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-ov 6927  df-om 7346  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-neg 10611  df-nn 11379  df-n0 11647  df-z 11733  df-prm 15795

This theorem is referenced by:  dvdsprime  15809  oddprmge3  15821  exprmfct  15824  prmdvdsfz  15825  isprm5  15827  isprm7  15828  maxprmfct  15829  coprm  15831  prmrp  15832  euclemma  15833  prmdvdsexpb  15836  prmexpb  15838  prmfac1  15839  rpexp  15840  cncongrprm  15845  phiprmpw  15889  phiprm  15890  fermltl  15897  prmdiv  15898  prmdiveq  15899  vfermltl  15914  vfermltlALT  15915  reumodprminv  15917  modprm0  15918  oddprm  15923  prm23lt5  15927  prm23ge5  15928  pcneg  15986  pcprmpw2  15994  pcprmpw  15995  difsqpwdvds  15999  pcprod  16007  prmpwdvds  16016  prmunb  16026  prmreclem3  16030  prmreclem5  16032  1arithlem4  16038  1arith  16039  4sqlem11  16067  4sqlem12  16068  4sqlem13  16069  4sqlem14  16070  4sqlem17  16073  prmdvdsprmo  16154  prmdvdsprmop  16155  fvprmselgcd1  16157  prmgaplem4  16166  prmgaplem5  16167  prmgaplem6  16168  prmgaplem8  16170  pgpfi  18408  sylow2alem2  18421  sylow2blem3  18425  gexexlem  18645  ablfacrplem  18855  ablfac1lem  18858  ablfac1b  18860  ablfac1eu  18863  pgpfac1lem2  18865  pgpfac1lem3a  18866  pgpfac1lem3  18867  pgpfac1lem4  18868  ablfaclem3  18877  prmirredlem  20241  wilthlem1  25250  wilthlem2  25251  ppisval  25286  vmappw  25298  muval1  25315  dvdssqf  25320  mumullem1  25361  mumul  25363  sqff1o  25364  dvdsppwf1o  25368  musum  25373  ppiublem1  25383  ppiublem2  25384  chtublem  25392  vmasum  25397  perfect1  25409  bposlem3  25467  bposlem6  25470  lgslem1  25478  lgsval2lem  25488  lgsvalmod  25497  lgsmod  25504  lgsdirprm  25512  lgsdir  25513  lgsdilem2  25514  lgsdi  25515  lgsne0  25516  lgsprme0  25520  lgsqr  25532  gausslemma2dlem1a  25546  gausslemma2dlem4  25550  gausslemma2dlem5a  25551  lgseisenlem1  25556  lgseisenlem2  25557  lgseisenlem3  25558  lgseisenlem4  25559  lgseisen  25560  lgsquadlem2  25562  lgsquadlem3  25563  lgsquad2lem2  25566  m1lgs  25569  2lgslem1a  25572  2lgslem1  25575  2lgslem2  25576  2lgsoddprm  25597  2sqlem3  25601  2sqlem4  25602  2sqlem6  25604  2sqlem8  25607  2sqblem  25612  2sqb  25613  rpvmasumlem  25632  dchrisum0flblem1  25653  dchrisum0flblem2  25654  dirith  25674  clwwlkndivn  27482  2sqmod  30214  oddprm2  31339  nn0prpwlem  32909  nn0prpw  32910  rtprmirr  38178  prmunb2  39476  nzprmdif  39484  etransclem48  41436  sfprmdvdsmersenne  42551  sgprmdvdsmersenne  42552  oddprmALTV  42633  oddprmne2  42659  even3prm2  42663  mogoldbblem  42664  sbgoldbst  42701  sbgoldbaltlem1  42702  sbgoldbaltlem2  42703  nnsum3primesprm  42713  nnsum3primesgbe  42715  nnsum4primesodd  42719  nnsum4primesoddALTV  42720  nnsum4primeseven  42723  nnsum4primesevenALTV  42724  bgoldbtbndlem2  42729  bgoldbtbndlem3  42730  bgoldbtbndlem4  42731  bgoldbtbnd  42732  ztprmneprm  43150