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

Theorem nn0z 10533
Description: A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nn0z

Proof of Theorem nn0z
StepHypRef Expression
1 nn0ssz 10531 . 2
21sseli 3389 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  e.wcel 1732   cn0 10445   cz 10510
This theorem is referenced by:  nn0negz  10547  nn0ltp1le  10566  nn0leltp1  10567  nn0ltlem1  10568  nn0lt10b  10570  nn0lem1lt  10571  fnn0ind  10605  fz1n  11324  elfz2nn0  11336  elfzelfzadd  11362  fznn0  11376  fzctr  11381  fzossrbm1  11430  fzo1fzo0n0  11440  fzofzim  11445  elfzodifsumelfzo  11456  ubmelm1fzo  11472  elfznelfzo  11479  flmulnn0  11521  quoremnn0  11544  zmodidfzoimp  11587  expdiv  11763  faclbnd3  11917  bccmpl  11934  bcnp1n  11939  bcval5  11943  bcn2  11944  bcp1m1  11945  brfi1uzind  12066  wrdlenge1n0  12107  ccatval1lsw  12130  lswccat0lsw  12135  swrdspsleq  12189  swrdlsw  12193  2swrd1eqwrdeq  12195  swrdccatin12lem1  12222  swrdccatin12lem3  12228  swrdccat3  12230  swrdccat  12231  revlen  12249  repswswrd  12269  repswccat  12270  2cshw  12294  cshweqrep  12302  cats1fv  12333  swrd2lsw  12399  2swrd2eqwrdeq  12400  isercoll  12992  iseraltlem2  13007  bcxmas  13145  geo2sum2  13181  geomulcvg  13183  esum  13213  ege2le3  13222  eftlcl  13238  reeftlcl  13239  eftlub  13240  effsumlt  13242  eirrlem  13333  dvdseq  13427  dvds1  13428  dvdsext  13431  divalglem4  13447  divalglem5  13448  bitsinv1  13485  nn0gcdid0  13556  nn0seqcvgd  13592  algcvga  13601  eucalgf  13605  nonsq  13684  odzdvds  13714  coprimeprodsq  13723  coprimeprodsq2  13724  oddprm  13729  iserodd  13749  pcexp  13773  pcidlem  13785  pc11  13793  pcfac  13808  prmunb  13822  hashbc2  13914  cshwshashlem2  13970  mulgz  15482  mulgdirlem  15485  mulgass  15491  mndodcongi  15790  oddvdsnn0  15791  odeq  15797  odmulg  15801  efgsdmi  15973  cyggex2  16116  mulgass2  16325  chrrhm  17437  zncrng  17450  znzrh2  17451  zndvds  17455  znchr  17468  znunit  17469  clmmulg  20133  itgcnlem  20694  degltlem1  21010  plyco0  21126  dgreq0  21198  plydivex  21229  aannenlem1  21260  abelthlem1  21362  abelthlem3  21364  abelthlem8  21370  abelthlem9  21371  advlogexp  21566  cxpexp  21579  leibpilem1  21801  leibpi  21803  log2cnv  21805  log2tlbnd  21806  basellem2  21885  sgmnncl  21951  chpp1  21959  bcmono  22082  bcmax  22083  bcp1ctr  22084  lgsneg1  22125  lgsdirnn0  22144  lgsdinn0  22145  dchrisumlem1  22204  qabvle  22340  ostth2lem2  22349  redwlk  22627  fargshiftlem  22642  fargshiftfo  22646  gxcom  22878  gxinv  22879  gxid  22882  gxnn0add  22883  gxnn0mul  22886  gxdi  22905  nndiffz1  25205  xrge0mulgnn0  25281  hashf2  25713  eulerpartlemb  25925  fz0n  26541  risefacval2  26665  fallfacval2  26666  zrisefaccl  26675  zfallfaccl  26676  fallrisefac  26680  faclimlem3  26703  faclim  26704  iprodfac  26705  bpolylem  27433  fsumkthpow  27441  mblfinlem1  27608  mblfinlem2  27609  nacsfix  28196  fzsplit1nn0  28240  eldioph2lem1  28246  fz1eqin  28255  diophin  28259  eq0rabdioph  28263  rexrabdioph  28280  rexzrexnn0  28290  irrapxlem4  28314  pell14qrss1234  28345  pell1qrss14  28357  monotoddzz  28432  rmxypos  28438  ltrmynn0  28439  ltrmxnn0  28440  lermxnn0  28441  rmxnn  28442  rmynn0  28448  jm2.17a  28451  jm2.17b  28452  rmygeid  28455  jm2.18  28485  jm2.19lem3  28488  jm2.19lem4  28489  jm2.22  28492  rmxdiophlem  28512  hbt  28674  proot1ex  28751  lesubnn0  29360  nn0ge2m1nn  29363  nn0lt2  29365  nn0pzuz  29375  ige2m1fz  29385  elfzlble  29387  subsubelfzo0  29389  2ffzoeq  29393  fzossfzop1  29397  elfzom1elfzo  29398  zpnn0elfzo  29402  ccatw2s1p1  29450  ccatw2s1p2  29451  wlkv0  29472  wlkiswwlk2lem3  29508  wwlknred  29536  wwlknext  29537  wwlkm1edg  29548  clwlkisclwwlklem2a1  29622  clwlkisclwwlklem2a2  29623  clwlkisclwwlklem2fv1  29625  clwlkisclwwlklem2fv2  29626  clwlkisclwwlklem2a4  29627  clwlkisclwwlklem2a  29628  clwlkisclwwlklem1  29630  clwlkisclwwlk  29632  clwwisshclwwlem  29651  erclwwlksym0  29659  erclwwlktr0  29660  difelfzle  29668  clwlkfclwwlk2wrd  29694  clwlkfclwwlk  29698  clwlkf1clwwlklem3  29702  nbhashuvtx1  29714  wwlkextproplem1  29741  frgrawopreglem2  29819  numclwwlk5lem  29885  numclwwlk5  29886  numclwwlk7  29888  frgrareggt1  29890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-8 1734  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pow 4493  ax-pr 4554  ax-un 6382  ax-resscn 9218  ax-1cn 9219  ax-icn 9220  ax-addcl 9221  ax-addrcl 9222  ax-mulcl 9223  ax-mulrcl 9224  ax-mulcom 9225  ax-addass 9226  ax-mulass 9227  ax-distr 9228  ax-i2m1 9229  ax-1ne0 9230  ax-1rid 9231  ax-rnegex 9232  ax-rrecex 9233  ax-cnre 9234  ax-pre-lttri 9235  ax-pre-lttrn 9236  ax-pre-ltadd 9237  ax-pre-mulgt0 9238
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-nel 2655  df-ral 2764  df-rex 2765  df-reu 2766  df-rab 2768  df-v 3017  df-sbc 3225  df-csb 3326  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-pss 3381  df-nul 3674  df-if 3826  df-pw 3895  df-sn 3915  df-pr 3916  df-tp 3917  df-op 3918  df-uni 4118  df-iun 4199  df-br 4319  df-opab 4377  df-mpt 4378  df-tr 4412  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4868  df-rel 4869  df-cnv 4870  df-co 4871  df-dm 4872  df-rn 4873  df-res 4874  df-ima 4875  df-iota 5401  df-fun 5440  df-fn 5441  df-f 5442  df-f1 5443  df-fo 5444  df-f1o 5445  df-fv 5446  df-riota 6062  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-om 6487  df-recs 6795  df-rdg 6830  df-er 7067  df-en 7274  df-dom 7275  df-sdom 7276  df-pnf 9299  df-mnf 9300  df-xr 9301  df-ltxr 9302  df-le 9303  df-sub 9474  df-neg 9475  df-nn 10189  df-n0 10446  df-z 10511
  Copyright terms: Public domain W3C validator