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

Theorem nn0z 10476
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 10474 . 2
21sseli 3377 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  e.wcel 1724   cn0 10388   cz 10453
This theorem is referenced by:  nn0negz  10490  nn0ltp1le  10509  nn0leltp1  10510  nn0ltlem1  10511  nn0lt10b  10513  nn0lem1lt  10514  fnn0ind  10548  fz1n  11267  elfz2nn0  11279  elfzelfzadd  11305  fznn0  11319  fzctr  11324  fzossrbm1  11373  fzo1fzo0n0  11383  fzofzim  11388  elfzodifsumelfzo  11399  ubmelm1fzo  11415  elfznelfzo  11422  flmulnn0  11464  quoremnn0  11487  zmodidfzoimp  11530  expdiv  11706  faclbnd3  11860  bccmpl  11877  bcnp1n  11882  bcval5  11886  bcn2  11887  bcp1m1  11888  brfi1uzind  12006  wrdlenge1n0  12047  ccatval1lsw  12070  lswccat0lsw  12075  swrdspsleq  12129  swrdlsw  12133  2swrd1eqwrdeq  12135  swrdccatin12lem1  12161  swrdccatin12lem3  12167  swrdccat3  12169  swrdccat  12170  revlen  12188  repswswrd  12208  repswccat  12209  2cshw  12233  cshweqrep  12241  cats1fv  12272  swrd2lsw  12338  2swrd2eqwrdeq  12339  isercoll  12931  iseraltlem2  12946  bcxmas  13084  geo2sum2  13120  geomulcvg  13122  esum  13152  ege2le3  13161  eftlcl  13177  reeftlcl  13178  eftlub  13179  effsumlt  13181  eirrlem  13272  dvdseq  13366  dvds1  13367  dvdsext  13370  divalglem4  13386  divalglem5  13387  bitsinv1  13424  nn0gcdid0  13495  nn0seqcvgd  13531  algcvga  13540  eucalgf  13544  nonsq  13623  odzdvds  13653  coprimeprodsq  13662  coprimeprodsq2  13663  oddprm  13668  iserodd  13688  pcexp  13712  pcidlem  13724  pc11  13732  pcfac  13747  prmunb  13761  hashbc2  13853  cshwshashlem2  13909  mulgz  15414  mulgdirlem  15417  mulgass  15423  mndodcongi  15684  oddvdsnn0  15685  odeq  15691  odmulg  15695  efgsdmi  15867  cyggex2  16009  mulgass2  16213  chrrhm  17315  zncrng  17328  znzrh2  17329  zndvds  17333  znchr  17346  znunit  17347  clmmulg  19622  itgcnlem  20183  degltlem1  20499  plyco0  20615  dgreq0  20687  plydivex  20718  aannenlem1  20749  abelthlem1  20851  abelthlem3  20853  abelthlem8  20859  abelthlem9  20860  advlogexp  21055  cxpexp  21068  leibpilem1  21289  leibpi  21291  log2cnv  21293  log2tlbnd  21294  basellem2  21373  sgmnncl  21439  chpp1  21447  bcmono  21570  bcmax  21571  bcp1ctr  21572  lgsneg1  21613  lgsdirnn0  21632  lgsdinn0  21633  dchrisumlem1  21692  qabvle  21828  ostth2lem2  21837  redwlk  22115  fargshiftlem  22130  fargshiftfo  22134  gxcom  22366  gxinv  22367  gxid  22370  gxnn0add  22371  gxnn0mul  22374  gxdi  22393  nndiffz1  24696  xrge0mulgnn0  24772  hashf2  25204  eulerpartlemb  25416  fz0n  26032  risefacval2  26156  fallfacval2  26157  zrisefaccl  26166  zfallfaccl  26167  fallrisefac  26171  faclimlem3  26194  faclim  26195  iprodfac  26196  bpolylem  26924  fsumkthpow  26932  mblfinlem1  27099  mblfinlem2  27100  nacsfix  27697  fzsplit1nn0  27743  eldioph2lem1  27749  fz1eqin  27758  diophin  27762  eq0rabdioph  27766  rexrabdioph  27783  rexzrexnn0  27793  irrapxlem4  27817  pell14qrss1234  27848  pell1qrss14  27860  monotoddzz  27935  rmxypos  27941  ltrmynn0  27942  ltrmxnn0  27943  lermxnn0  27944  rmxnn  27945  rmynn0  27951  jm2.17a  27954  jm2.17b  27955  rmygeid  27958  jm2.18  27988  jm2.19lem3  27991  jm2.19lem4  27992  jm2.22  27995  rmxdiophlem  28015  hbt  28240  proot1ex  28426  lesubnn0  29038  nn0ge2m1nn  29041  nn0lt2  29043  nn0pzuz  29053  ige2m1fz  29063  elfzlble  29065  subsubelfzo0  29067  2ffzoeq  29071  fzossfzop1  29075  elfzom1elfzo  29076  zpnn0elfzo  29080  ccatw2s1p1  29128  ccatw2s1p2  29129  wlkv0  29150  wlkiswwlk2lem3  29186  wwlknred  29214  wwlknext  29215  wwlkm1edg  29226  clwlkisclwwlklem2a1  29300  clwlkisclwwlklem2a2  29301  clwlkisclwwlklem2fv1  29303  clwlkisclwwlklem2fv2  29304  clwlkisclwwlklem2a4  29305  clwlkisclwwlklem2a  29306  clwlkisclwwlklem1  29308  clwlkisclwwlk  29310  clwwisshclwwlem  29329  erclwwlksym0  29337  erclwwlktr0  29338  difelfzle  29346  clwlkfclwwlk2wrd  29372  clwlkfclwwlk  29376  clwlkf1clwwlklem3  29380  nbhashuvtx1  29392  wwlkextproplem1  29419  frgrawopreglem2  29497  numclwwlk5lem  29563  numclwwlk5  29564  numclwwlk7  29566  frgrareggt1  29568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-8 1726  ax-9 1728  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462  ax-sep 4423  ax-nul 4431  ax-pow 4477  ax-pr 4538  ax-un 6338  ax-resscn 9161  ax-1cn 9162  ax-icn 9163  ax-addcl 9164  ax-addrcl 9165  ax-mulcl 9166  ax-mulrcl 9167  ax-mulcom 9168  ax-addass 9169  ax-mulass 9170  ax-distr 9171  ax-i2m1 9172  ax-1ne0 9173  ax-1rid 9174  ax-rnegex 9175  ax-rrecex 9176  ax-cnre 9177  ax-pre-lttri 9178  ax-pre-lttrn 9179  ax-pre-ltadd 9180  ax-pre-mulgt0 9181
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-eu 2309  df-mo 2310  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-ne 2646  df-nel 2647  df-ral 2756  df-rex 2757  df-reu 2758  df-rab 2760  df-v 3008  df-sbc 3213  df-csb 3314  df-dif 3356  df-un 3358  df-in 3360  df-ss 3367  df-pss 3369  df-nul 3661  df-if 3813  df-pw 3880  df-sn 3900  df-pr 3901  df-tp 3902  df-op 3903  df-uni 4102  df-iun 4183  df-br 4303  df-opab 4361  df-mpt 4362  df-tr 4396  df-eprel 4635  df-id 4639  df-po 4644  df-so 4645  df-fr 4682  df-we 4684  df-ord 4725  df-on 4726  df-lim 4727  df-suc 4728  df-xp 4850  df-rel 4851  df-cnv 4852  df-co 4853  df-dm 4854  df-rn 4855  df-res 4856  df-ima 4857  df-iota 5380  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-riota 6026  df-ov 6070  df-oprab 6071  df-mpt2 6072  df-om 6442  df-recs 6745  df-rdg 6780  df-er 7017  df-en 7222  df-dom 7223  df-sdom 7224  df-pnf 9242  df-mnf 9243  df-xr 9244  df-ltxr 9245  df-le 9246  df-sub 9417  df-neg 9418  df-nn 10132  df-n0 10389  df-z 10454
  Copyright terms: Public domain W3C validator