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

Theorem prmz 13707
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
StepHypRef Expression
1 prmnn 13706 . 2
21nnzd 10691 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1749   cz 10591   cprime 13703
This theorem is referenced by:  dvdsprime  13716  coprm  13726  prmrp  13727  euclemma  13734  exprmfct  13736  isprm5  13738  maxprmfct  13739  prmdvdsexpb  13741  prmexpb  13743  prmfac1  13744  rpexp  13746  phiprmpw  13791  phiprm  13792  fermltl  13799  prmdiv  13800  prmdiveq  13801  reumodprminv  13812  modprm0  13813  oddprm  13822  pcneg  13880  pcprmpw2  13888  pcprmpw  13889  pcprod  13897  prmpwdvds  13905  prmunb  13915  prmreclem3  13919  prmreclem5  13921  1arithlem1  13924  1arithlem4  13927  1arith  13928  4sqlem11  13956  4sqlem12  13957  4sqlem13  13958  4sqlem14  13959  4sqlem17  13962  pgpfi  16041  sylow2alem2  16054  sylow2blem3  16058  gexexlem  16270  ablfacrplem  16432  ablfac1lem  16435  ablfac1b  16437  ablfac1eu  16440  pgpfac1lem2  16442  pgpfac1lem3a  16443  pgpfac1lem3  16444  pgpfac1lem4  16445  ablfaclem3  16454  prmirredlem  17625  prmirredlemOLD  17628  wilthlem1  22147  wilthlem2  22148  ppisval  22182  vmappw  22195  muval1  22212  dvdssqf  22217  mumullem1  22258  mumul  22260  sqff1o  22261  dvdsppwf1o  22267  musum  22272  ppiublem1  22282  ppiublem2  22283  chtublem  22291  vmasum  22296  perfect1  22308  bposlem3  22366  bposlem6  22369  lgslem1  22376  lgsval2lem  22386  lgsvalmod  22395  lgsmod  22401  lgsdirprm  22409  lgsdir  22410  lgsdilem2  22411  lgsdi  22412  lgsne0  22413  lgsqr  22426  lgseisenlem1  22429  lgseisenlem2  22430  lgseisenlem3  22431  lgseisenlem4  22432  lgseisen  22433  lgsquadlem2  22435  lgsquadlem3  22436  lgsquad2lem2  22439  m1lgs  22442  2sqlem3  22446  2sqlem4  22447  2sqlem6  22449  2sqlem8  22452  2sqblem  22457  2sqb  22458  rpvmasumlem  22477  dchrisum0flblem1  22498  dchrisum0flblem2  22499  dirith  22519  nn0prpwlem  28188  nn0prpw  28189  prmn2uzge3  29923  clwwlkndivn  30185  ztprmneprm  30411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-8 1751  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-sep 4388  ax-nul 4396  ax-pow 4442  ax-pr 4503  ax-un 6342  ax-resscn 9285  ax-1cn 9286  ax-icn 9287  ax-addcl 9288  ax-addrcl 9289  ax-mulcl 9290  ax-mulrcl 9291  ax-mulcom 9292  ax-addass 9293  ax-mulass 9294  ax-distr 9295  ax-i2m1 9296  ax-1ne0 9297  ax-1rid 9298  ax-rnegex 9299  ax-rrecex 9300  ax-cnre 9301  ax-pre-lttri 9302  ax-pre-lttrn 9303  ax-pre-ltadd 9304  ax-pre-mulgt0 9305
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3or 951  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-eu 2248  df-mo 2249  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-nel 2588  df-ral 2699  df-rex 2700  df-reu 2701  df-rab 2703  df-v 2953  df-sbc 3165  df-csb 3266  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-pss 3321  df-nul 3615  df-if 3769  df-pw 3839  df-sn 3859  df-pr 3860  df-tp 3861  df-op 3862  df-uni 4067  df-iun 4148  df-br 4268  df-opab 4326  df-mpt 4327  df-tr 4361  df-eprel 4603  df-id 4607  df-po 4612  df-so 4613  df-fr 4650  df-we 4652  df-ord 4693  df-on 4694  df-lim 4695  df-suc 4696  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5353  df-fun 5392  df-fn 5393  df-f 5394  df-f1 5395  df-fo 5396  df-f1o 5397  df-fv 5398  df-riota 6020  df-ov 6064  df-oprab 6065  df-mpt2 6066  df-om 6447  df-recs 6791  df-rdg 6825  df-er 7062  df-en 7270  df-dom 7271  df-sdom 7272  df-pnf 9366  df-mnf 9367  df-xr 9368  df-ltxr 9369  df-le 9370  df-sub 9543  df-neg 9544  df-nn 10269  df-n0 10526  df-z 10592  df-prm 13704
  Copyright terms: Public domain W3C validator