MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prmz Structured version   Visualization version   Unicode version

Theorem prmz 14705
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  |-  ( P  e.  Prime  ->  P  e.  ZZ )

Proof of Theorem prmz
StepHypRef Expression
1 prmnn 14704 . 2  |-  ( P  e.  Prime  ->  P  e.  NN )
21nnzd 11062 1  |-  ( P  e.  Prime  ->  P  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1904   ZZcz 10961   Primecprime 14701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-er 7381  df-en 7588  df-dom 7589  df-sdom 7590  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-nn 10632  df-n0 10894  df-z 10962  df-prm 14702
This theorem is referenced by:  dvdsprime  14716  prmn2uzge3  14723  exprmfct  14727  prmdvdsfz  14728  isprm5  14730  maxprmfct  14731  coprm  14736  prmrp  14737  euclemma  14744  prmdvdsexpb  14747  prmexpb  14749  prmfac1  14750  rpexp  14751  phiprmpw  14803  phiprm  14804  fermltl  14811  prmdiv  14812  prmdiveq  14813  vfermltl  14831  vfermltlALT  14832  reumodprminv  14834  modprm0  14835  oddprm  14844  pcneg  14902  pcprmpw2  14910  pcprmpw  14911  pcprod  14919  prmpwdvds  14927  prmunb  14937  prmreclem3  14941  prmreclem5  14943  1arithlem1  14946  1arithlem4  14949  1arith  14950  4sqlem11  14978  4sqlem12  14979  4sqlem13OLD  14980  4sqlem14OLD  14981  4sqlem17OLD  14984  4sqlem13  14986  4sqlem14  14987  4sqlem17  14990  prmdvdsprmo  15079  prmdvdsprmop  15080  fvprmselgcd1  15082  prmdvdsprmorOLD  15094  prmdvdsprmorpOLD  15095  prmgaplem4  15103  prmgaplem5  15104  prmgaplem6  15105  prmgaplem8  15107  pgpfi  17335  sylow2alem2  17348  sylow2blem3  17352  gexexlem  17568  ablfacrplem  17776  ablfac1lem  17779  ablfac1b  17781  ablfac1eu  17784  pgpfac1lem2  17786  pgpfac1lem3a  17787  pgpfac1lem3  17788  pgpfac1lem4  17789  ablfaclem3  17798  prmirredlem  19141  wilthlem1  24072  wilthlem2  24073  ppisval  24109  vmappw  24122  muval1  24139  dvdssqf  24144  mumullem1  24185  mumul  24187  sqff1o  24188  dvdsppwf1o  24194  musum  24199  ppiublem1  24209  ppiublem2  24210  chtublem  24218  vmasum  24223  perfect1  24235  bposlem3  24293  bposlem6  24296  lgslem1  24303  lgsval2lem  24313  lgsvalmod  24322  lgsmod  24328  lgsdirprm  24336  lgsdir  24337  lgsdilem2  24338  lgsdi  24339  lgsne0  24340  lgsqr  24353  lgseisenlem1  24356  lgseisenlem2  24357  lgseisenlem3  24358  lgseisenlem4  24359  lgseisen  24360  lgsquadlem2  24362  lgsquadlem3  24363  lgsquad2lem2  24366  m1lgs  24369  2sqlem3  24373  2sqlem4  24374  2sqlem6  24376  2sqlem8  24379  2sqblem  24384  2sqb  24385  rpvmasumlem  24404  dchrisum0flblem1  24425  dchrisum0flblem2  24426  dirith  24446  clwwlkndivn  25644  2sqmod  28484  nn0prpwlem  31049  nn0prpw  31050  prmunb2  36729  isprm7  36730  nzprmdif  36738  etransclem48OLD  38259  etransclem48  38260  oddprmALTV  38961  bgoldbst  39024  sgoldbaltlem1  39025  sgoldbaltlem2  39026  nnsum3primesprm  39030  nnsum3primesgbe  39032  nnsum4primesodd  39036  nnsum4primesoddALTV  39037  nnsum4primeseven  39040  nnsum4primesevenALTV  39041  bgoldbtbndlem2  39046  bgoldbtbndlem3  39047  bgoldbtbndlem4  39048  bgoldbtbnd  39049  ztprmneprm  40636
  Copyright terms: Public domain W3C validator