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

Theorem nn0z 11438
Description: A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nn0z (𝑁 ∈ ℕ0𝑁 ∈ ℤ)

Proof of Theorem nn0z
StepHypRef Expression
1 nn0ssz 11436 . 2 0 ⊆ ℤ
21sseli 3632 1 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  0cn0 11330  cz 11415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416
This theorem is referenced by:  nn0negz  11453  nn0ltp1le  11473  nn0leltp1  11474  nn0ltlem1  11475  nn0lt2  11478  nn0le2is012  11479  nn0lem1lt  11480  fnn0ind  11514  nn0pzuz  11783  nn0ge2m1nnALT  11820  fz1n  12397  ige2m1fz  12468  elfz2nn0  12469  fznn0  12470  elfz0add  12477  fzctr  12490  difelfzle  12491  fzoun  12544  fzofzim  12554  fzo1fzo0n0  12558  elincfzoext  12565  elfzodifsumelfzo  12573  fz0add1fz1  12577  zpnn0elfzo  12580  fzossfzop1  12585  ubmelm1fzo  12604  elfznelfzo  12613  flmulnn0  12668  quoremnn0  12695  zmodidfzoimp  12740  modmuladdnn0  12754  modfzo0difsn  12782  expdiv  12951  faclbnd3  13119  bccmpl  13136  bcnp1n  13141  bcval5  13145  bcn2  13146  bcp1m1  13147  hashge2el2difr  13301  fi1uzind  13317  wrdred1  13382  wrdred1hash  13383  ccatalpha  13411  swrdfv2  13492  swrdsb0eq  13493  swrdsbslen  13494  swrdspsleq  13495  swrdlsw  13498  2swrd1eqwrdeq  13500  swrdccatin12lem1  13530  swrdccatin12lem3  13536  swrdccat3  13538  swrdccat  13539  revlen  13557  repswswrd  13577  repswccat  13578  cshwidxmodr  13596  cshf1  13602  2cshw  13605  cshweqrep  13613  cshwcshid  13619  cshwcsh2id  13620  cats1fv  13650  swrd2lsw  13741  2swrd2eqwrdeq  13742  isercoll  14442  iseraltlem2  14457  bcxmas  14611  geo2sum2  14649  geomulcvg  14651  risefacval2  14785  fallfacval2  14786  zrisefaccl  14795  zfallfaccl  14796  fallrisefac  14800  bpolylem  14823  fsumkthpow  14831  esum  14855  ege2le3  14864  eftlcl  14881  reeftlcl  14882  eftlub  14883  effsumlt  14885  eirrlem  14976  dvds1  15088  dvdsext  15090  addmodlteqALT  15094  oddnn02np1  15119  oddge22np1  15120  nn0ehalf  15142  nn0o1gt2  15144  nno  15145  nn0o  15146  nn0oddm1d2  15148  divalglem4  15166  divalglem5  15167  modremain  15179  bitsinv1  15211  nn0gcdid0  15289  nn0seqcvgd  15330  algcvga  15339  eucalgf  15343  nonsq  15514  odzdvds  15547  coprimeprodsq  15560  coprimeprodsq2  15561  oddprm  15562  iserodd  15587  pcexp  15611  pcidlem  15623  pc11  15631  dvdsprmpweqle  15637  difsqpwdvds  15638  pcfac  15650  prmunb  15665  hashbc2  15757  cshwshashlem2  15850  mulgaddcom  17611  mulginvcom  17612  mulgz  17615  mulgdirlem  17619  mulgass  17626  mndodcongi  18008  oddvdsnn0  18009  odeq  18015  odmulg  18019  efgsdmi  18191  cyggex2  18344  mulgass2  18647  chrrhm  19927  zncrng  19941  znzrh2  19942  zndvds  19946  znchr  19959  znunit  19960  chfacfisf  20707  chfacfisfcpmat  20708  chfacfscmulfsupp  20712  chfacfpmmulfsupp  20716  clmmulg  22947  itgcnlem  23601  degltlem1  23877  plyco0  23993  dgreq0  24066  plydivex  24097  aannenlem1  24128  abelthlem1  24230  abelthlem3  24232  abelthlem8  24238  abelthlem9  24239  advlogexp  24446  cxpexp  24459  leibpilem1  24712  leibpi  24714  log2cnv  24716  log2tlbnd  24717  basellem2  24853  sgmnncl  24918  chpp1  24926  bcmono  25047  bcmax  25048  bcp1ctr  25049  lgsneg1  25092  lgsdirnn0  25114  lgsdinn0  25115  2lgslem1c  25163  2lgslem3a1  25170  2lgslem3b1  25171  2lgslem3c1  25172  2lgsoddprmlem2  25179  dchrisumlem1  25223  qabvle  25359  ostth2lem2  25368  tgldimor  25442  upgrewlkle2  26558  wlkv0  26603  redwlk  26625  pthdadjvtx  26682  pthdlem1  26718  wwlknvtx  26793  wlkiswwlks2lem3  26825  wwlksm1edg  26835  wwlksnred  26855  wwlksnext  26856  clwlkclwwlklem2a1  26958  clwlkclwwlklem2a2  26959  clwlkclwwlklem2fv1  26961  clwlkclwwlklem2fv2  26962  clwlkclwwlklem2a4  26963  clwlkclwwlklem2a  26964  clwlkclwwlklem2  26966  clwlkclwwlk  26968  clwwisshclwwslem  26971  clwlksfclwwlk2wrd  27045  clwlksfclwwlk  27049  clwlksf1clwwlklem3  27054  eucrctshift  27221  eucrct2eupth1  27222  eucrct2eupth  27223  numclwwlk5lem  27374  numclwwlk5  27375  numclwwlk7  27378  frgrreggt1  27380  nndiffz1  29676  xrge0mulgnn0  29817  hashf2  30274  signsvtn0  30775  fz0n  31742  bcneg1  31748  bccolsum  31751  faclimlem3  31757  faclim  31758  iprodfac  31759  poimirlem28  33567  mblfinlem1  33576  mblfinlem2  33577  nacsfix  37592  fzsplit1nn0  37634  eldioph2lem1  37640  fz1eqin  37649  diophin  37653  eq0rabdioph  37657  rexrabdioph  37675  rexzrexnn0  37685  irrapxlem4  37706  pell14qrss1234  37737  pell1qrss14  37749  monotoddzz  37825  rmxypos  37831  ltrmynn0  37832  ltrmxnn0  37833  lermxnn0  37834  rmxnn  37835  rmynn0  37841  jm2.17a  37844  jm2.17b  37845  rmygeid  37848  jm2.18  37872  jm2.19lem3  37875  jm2.19lem4  37876  jm2.22  37879  rmxdiophlem  37899  hbt  38017  proot1ex  38096  fzisoeu  39828  stirlinglem5  40613  elfzlble  41655  subsubelfzo0  41661  2ffzoeq  41663  fargshiftfo  41703  pfxnd  41720  pfxccat3  41751  pfxccat3a  41754  fmtnof1  41772  fmtnorec1  41774  goldbachthlem1  41782  odz2prm2pw  41800  flsqrt  41833  lighneallem4  41852  nn0eo  42647  nn0ofldiv2  42651  flnn0div2ge  42652  fllog2  42687  blenpw2  42697  blennngt2o2  42711  nn0digval  42719  dignn0fr  42720  digexp  42726  0dig2nn0e  42731  0dig2nn0o  42732  dig2bits  42733  dignn0flhalflem2  42735  dignn0ehalf  42736  dignn0flhalf  42737  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator