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

Theorem nn0z 10306
Description: A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nn0z  |-  ( N  e.  NN0  ->  N  e.  ZZ )

Proof of Theorem nn0z
StepHypRef Expression
1 nn0ssz 10304 . 2  |-  NN0  C_  ZZ
21sseli 3346 1  |-  ( N  e.  NN0  ->  N  e.  ZZ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   NN0cn0 10223   ZZcz 10284
This theorem is referenced by:  nn0negz  10317  nn0ltp1le  10334  nn0leltp1  10335  nn0ltlem1  10336  nn0lt10b  10338  nn0lem1lt  10339  fnn0ind  10371  fz1n  11075  elfz2nn0  11084  fznn0  11115  fzctr  11119  fzossrbm1  11166  elfznelfzo  11194  flmulnn0  11231  quoremnn0  11239  expdiv  11432  faclbnd3  11585  bccmpl  11602  bcnp1n  11607  bcval5  11611  bcn2  11612  bcp1m1  11613  brfi1uzind  11717  revlen  11796  cats1fv  11825  isercoll  12463  iseraltlem2  12478  bcxmas  12617  geo2sum2  12653  geomulcvg  12655  esum  12685  ege2le3  12694  eftlcl  12710  reeftlcl  12711  eftlub  12712  effsumlt  12714  eirrlem  12805  dvdseq  12899  dvds1  12900  dvdsext  12902  divalglem4  12918  divalglem5  12919  bitsinv1  12956  nn0gcdid0  13027  nn0seqcvgd  13063  algcvga  13072  eucalgf  13076  nonsq  13153  odzdvds  13183  coprimeprodsq  13185  coprimeprodsq2  13186  oddprm  13191  iserodd  13211  pcexp  13235  pcidlem  13247  pc11  13255  pcfac  13270  prmunb  13284  hashbc2  13376  mulgz  14913  mulgdirlem  14916  mulgass  14922  mndodcongi  15183  oddvdsnn0  15184  odeq  15190  odmulg  15194  efgsdmi  15366  cyggex2  15508  mulgass2  15712  chrrhm  16814  zncrng  16827  znzrh2  16828  zndvds  16832  znchr  16845  znunit  16846  clmmulg  19120  itgcnlem  19683  degltlem1  19997  plyco0  20113  dgreq0  20185  plydivex  20216  aannenlem1  20247  abelthlem1  20349  abelthlem3  20351  abelthlem8  20357  abelthlem9  20358  advlogexp  20548  cxpexp  20561  leibpilem1  20782  leibpi  20784  log2cnv  20786  log2tlbnd  20787  basellem2  20866  sgmnncl  20932  chpp1  20940  bcmono  21063  bcmax  21064  bcp1ctr  21065  lgsneg1  21106  lgsdirnn0  21125  lgsdinn0  21126  dchrisumlem1  21185  qabvle  21321  ostth2lem2  21330  redwlk  21608  fargshiftlem  21623  fargshiftfo  21627  gxcom  21859  gxinv  21860  gxid  21863  gxnn0add  21864  gxnn0mul  21867  gxdi  21886  xrge0mulgnn0  24212  hashf2  24476  fz0n  25204  risefacval2  25328  fallfacval2  25329  zrisefaccl  25338  zfallfaccl  25339  fallrisefac  25343  faclimlem3  25366  faclim  25367  iprodfac  25368  bpolylem  26096  fsumkthpow  26104  mblfinlem1  26245  mblfinlem2  26246  nacsfix  26768  fzsplit1nn0  26814  eldioph2lem1  26820  fz1eqin  26829  diophin  26833  eq0rabdioph  26837  rexrabdioph  26856  rexzrexnn0  26866  irrapxlem4  26890  pell14qrss1234  26921  pell1qrss14  26933  monotoddzz  27008  rmxypos  27014  ltrmynn0  27015  ltrmxnn0  27016  lermxnn0  27017  rmxnn  27018  rmynn0  27024  jm2.17a  27027  jm2.17b  27028  rmygeid  27031  jm2.18  27061  jm2.19lem3  27064  jm2.19lem4  27065  jm2.22  27068  rmxdiophlem  27088  hbt  27313  proot1ex  27499  lesubnn0  28107  elfzelfzadd  28121  ubmelfzo  28137  ubmelm1fzo  28138  fzo1fzo0n0  28139  subsubelfzo0  28146  fzofzim  28147  2ffzoeq  28151  swrd0swrd  28219  swrdccatin12lem2  28229  swrdccatin12lem4  28235  swrdccat3  28237  swrdccat  28238  cshwoor  28259  cshwidx  28264  2cshw1lem1  28270  2cshw1lem2  28271  2cshw2lem1  28274  2cshw2lem2  28275  swrdtrcfvl  28287  cshweqrep  28296  cshwssizelem4a  28305  wlkiswwlk2lem3  28363  nbhashuvtx1  28419  frgrawopreglem2  28496
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703  ax-resscn 9049  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-addrcl 9053  ax-mulcl 9054  ax-mulrcl 9055  ax-mulcom 9056  ax-addass 9057  ax-mulass 9058  ax-distr 9059  ax-i2m1 9060  ax-1ne0 9061  ax-1rid 9062  ax-rnegex 9063  ax-rrecex 9064  ax-cnre 9065  ax-pre-lttri 9066  ax-pre-lttrn 9067  ax-pre-ltadd 9068  ax-pre-mulgt0 9069
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-iun 4097  df-br 4215  df-opab 4269  df-mpt 4270  df-tr 4305  df-eprel 4496  df-id 4500  df-po 4505  df-so 4506  df-fr 4543  df-we 4545  df-ord 4586  df-on 4587  df-lim 4588  df-suc 4589  df-om 4848  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-riota 6551  df-recs 6635  df-rdg 6670  df-er 6907  df-en 7112  df-dom 7113  df-sdom 7114  df-pnf 9124  df-mnf 9125  df-xr 9126  df-ltxr 9127  df-le 9128  df-sub 9295  df-neg 9296  df-nn 10003  df-n0 10224  df-z 10285
  Copyright terms: Public domain W3C validator