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

Theorem nn0z 11592
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 11590 . 2 0 ⊆ ℤ
21sseli 3740 1 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  0cn0 11484  cz 11569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-nn 11213  df-n0 11485  df-z 11570
This theorem is referenced by:  nn0negz  11607  nn0ltp1le  11627  nn0leltp1  11628  nn0ltlem1  11629  nn0lt2  11632  nn0le2is012  11633  nn0lem1lt  11634  fnn0ind  11668  nn0pzuz  11938  nn0ge2m1nnALT  11975  fz1n  12552  ige2m1fz  12623  elfz2nn0  12624  fznn0  12625  elfz0add  12632  fzctr  12645  difelfzle  12646  fzoun  12699  fzofzim  12709  fzo1fzo0n0  12713  elincfzoext  12720  elfzodifsumelfzo  12728  fz0add1fz1  12732  zpnn0elfzo  12735  fzossfzop1  12740  ubmelm1fzo  12758  elfznelfzo  12767  flmulnn0  12822  quoremnn0  12849  zmodidfzoimp  12894  modmuladdnn0  12908  modfzo0difsn  12936  expdiv  13105  faclbnd3  13273  bccmpl  13290  bcnp1n  13295  bcval5  13299  bcn2  13300  bcp1m1  13301  hashge2el2difr  13455  fi1uzind  13471  wrdred1  13536  wrdred1hash  13537  ccatalpha  13565  swrdfv2  13646  swrdsb0eq  13647  swrdsbslen  13648  swrdspsleq  13649  swrdlsw  13652  2swrd1eqwrdeq  13654  swrdccatin12lem1  13684  swrdccatin12lem3  13690  swrdccat3  13692  swrdccat  13693  revlen  13711  repswswrd  13731  repswccat  13732  cshwidxmodr  13750  cshf1  13756  2cshw  13759  cshweqrep  13767  cshwcshid  13773  cshwcsh2id  13774  cats1fv  13804  swrd2lsw  13896  2swrd2eqwrdeq  13897  isercoll  14597  iseraltlem2  14612  bcxmas  14766  geo2sum2  14804  geomulcvg  14806  risefacval2  14940  fallfacval2  14941  zrisefaccl  14950  zfallfaccl  14951  fallrisefac  14955  bpolylem  14978  fsumkthpow  14986  esum  15010  ege2le3  15019  eftlcl  15036  reeftlcl  15037  eftlub  15038  effsumlt  15040  eirrlem  15131  dvds1  15243  dvdsext  15245  addmodlteqALT  15249  oddnn02np1  15274  oddge22np1  15275  nn0ehalf  15297  nn0o1gt2  15299  nno  15300  nn0o  15301  nn0oddm1d2  15303  divalglem4  15321  divalglem5  15322  modremain  15334  bitsinv1  15366  nn0gcdid0  15444  nn0seqcvgd  15485  algcvga  15494  eucalgf  15498  nonsq  15669  odzdvds  15702  coprimeprodsq  15715  coprimeprodsq2  15716  oddprm  15717  iserodd  15742  pcexp  15766  pcidlem  15778  pc11  15786  dvdsprmpweqle  15792  difsqpwdvds  15793  pcfac  15805  prmunb  15820  hashbc2  15912  cshwshashlem2  16005  mulgaddcom  17765  mulginvcom  17766  mulgz  17769  mulgdirlem  17773  mulgass  17780  mndodcongi  18162  oddvdsnn0  18163  odeq  18169  odmulg  18173  efgsdmi  18345  cyggex2  18498  mulgass2  18801  chrrhm  20081  zncrng  20095  znzrh2  20096  zndvds  20100  znchr  20113  znunit  20114  chfacfisf  20861  chfacfisfcpmat  20862  chfacfscmulfsupp  20866  chfacfpmmulfsupp  20870  clmmulg  23101  itgcnlem  23755  degltlem1  24031  plyco0  24147  dgreq0  24220  plydivex  24251  aannenlem1  24282  abelthlem1  24384  abelthlem3  24386  abelthlem8  24392  abelthlem9  24393  advlogexp  24600  cxpexp  24613  leibpilem1  24866  leibpi  24868  log2cnv  24870  log2tlbnd  24871  basellem2  25007  sgmnncl  25072  chpp1  25080  bcmono  25201  bcmax  25202  bcp1ctr  25203  lgsneg1  25246  lgsdirnn0  25268  lgsdinn0  25269  2lgslem1c  25317  2lgslem3a1  25324  2lgslem3b1  25325  2lgslem3c1  25326  2lgsoddprmlem2  25333  dchrisumlem1  25377  qabvle  25513  ostth2lem2  25522  tgldimor  25596  upgrewlkle2  26712  wlkv0  26757  redwlk  26779  pthdadjvtx  26836  pthdlem1  26872  wwlknvtx  26948  wlkiswwlks2lem3  26980  wwlksm1edg  26990  wwlksnred  27010  wwlksnext  27011  clwlkclwwlklem2a1  27115  clwlkclwwlklem2a2  27116  clwlkclwwlklem2fv1  27118  clwlkclwwlklem2fv2  27119  clwlkclwwlklem2a4  27120  clwlkclwwlklem2a  27121  clwlkclwwlklem2  27123  clwlkclwwlk  27125  clwwisshclwwslem  27137  clwlksfclwwlk2wrdOLD  27212  clwlksfclwwlkOLD  27216  clwlksf1clwwlklem3OLD  27221  eucrctshift  27395  eucrct2eupth1  27396  eucrct2eupth  27397  numclwwlk5lem  27555  numclwwlk5  27556  numclwwlk7  27559  frgrreggt1  27561  nndiffz1  29857  xrge0mulgnn0  29998  hashf2  30455  signsvtn0  30956  fz0n  31923  bcneg1  31929  bccolsum  31932  faclimlem3  31938  faclim  31939  iprodfac  31940  poimirlem28  33750  mblfinlem1  33759  mblfinlem2  33760  nacsfix  37777  fzsplit1nn0  37819  eldioph2lem1  37825  fz1eqin  37834  diophin  37838  eq0rabdioph  37842  rexrabdioph  37860  rexzrexnn0  37870  irrapxlem4  37891  pell14qrss1234  37922  pell1qrss14  37934  monotoddzz  38010  rmxypos  38016  ltrmynn0  38017  ltrmxnn0  38018  lermxnn0  38019  rmxnn  38020  rmynn0  38026  jm2.17a  38029  jm2.17b  38030  rmygeid  38033  jm2.18  38057  jm2.19lem3  38060  jm2.19lem4  38061  jm2.22  38064  rmxdiophlem  38084  hbt  38202  proot1ex  38281  fzisoeu  40013  stirlinglem5  40798  elfzlble  41840  subsubelfzo0  41846  2ffzoeq  41848  fargshiftfo  41888  pfxnd  41905  pfxccat3  41936  pfxccat3a  41939  fmtnof1  41957  fmtnorec1  41959  goldbachthlem1  41967  odz2prm2pw  41985  flsqrt  42018  lighneallem4  42037  nn0eo  42832  nn0ofldiv2  42836  flnn0div2ge  42837  fllog2  42872  blenpw2  42882  blennngt2o2  42896  nn0digval  42904  dignn0fr  42905  digexp  42911  0dig2nn0e  42916  0dig2nn0o  42917  dig2bits  42918  dignn0flhalflem2  42920  dignn0ehalf  42921  dignn0flhalf  42922  nn0sumshdiglemB  42924
  Copyright terms: Public domain W3C validator