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

Theorem nn0z 11994
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 11992 . 2 0 ⊆ ℤ
21sseli 3962 1 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  0cn0 11886  cz 11970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-i2m1 10594  ax-1ne0 10595  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7148  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-neg 10862  df-nn 11628  df-n0 11887  df-z 11971
This theorem is referenced by:  nn0negz  12009  nn0ltp1le  12029  nn0leltp1  12030  nn0ltlem1  12031  nn0lt2  12034  nn0le2is012  12035  nn0lem1lt  12036  fnn0ind  12070  nn0pzuz  12294  nn0ge2m1nnALT  12331  fz1n  12915  ige2m1fz  12987  elfz2nn0  12988  fznn0  12989  elfz0add  12996  fzctr  13009  difelfzle  13010  fzoun  13064  fzofzim  13074  fzo1fzo0n0  13078  elincfzoext  13085  elfzodifsumelfzo  13093  fz0add1fz1  13097  zpnn0elfzo  13100  fzossfzop1  13105  ubmelm1fzo  13123  elfznelfzo  13132  flmulnn0  13187  quoremnn0  13214  zmodidfzoimp  13259  modmuladdnn0  13273  modfzo0difsn  13301  expdiv  13470  expnngt1  13592  faclbnd3  13642  bccmpl  13659  bcnp1n  13664  bcval5  13668  bcn2  13669  bcp1m1  13670  hashge2el2difr  13829  fi1uzind  13845  wrdred1  13902  wrdred1hash  13903  ccatalpha  13937  swrdnd0  14009  swrdfv2  14013  swrdsb0eq  14015  swrdsbslen  14016  swrdspsleq  14017  swrdlsw  14019  pfxnd  14039  pfxccatin12lem4  14078  pfxccatin12lem3  14084  pfxccat3  14086  swrdccat  14087  pfxccat3a  14090  revlen  14114  repswswrd  14136  repswccat  14138  cshwidxmodr  14156  cshf1  14162  2cshw  14165  cshweqrep  14173  cshwcshid  14179  cshwcsh2id  14180  cats1fv  14211  swrd2lsw  14304  2swrd2eqwrdeq  14305  isercoll  15014  iseraltlem2  15029  bcxmas  15180  geo2sum2  15220  geomulcvg  15222  risefacval2  15354  fallfacval2  15355  zrisefaccl  15364  zfallfaccl  15365  fallrisefac  15369  bpolylem  15392  fsumkthpow  15400  esum  15424  ege2le3  15433  eftlcl  15450  reeftlcl  15451  eftlub  15452  effsumlt  15454  eirrlem  15547  dvds1  15659  dvdsext  15661  addmodlteqALT  15665  oddnn02np1  15687  oddge22np1  15688  nn0ehalf  15719  nn0o1gt2  15722  nno  15723  nn0o  15724  nn0oddm1d2  15726  divalglem4  15737  divalglem5  15738  modremain  15749  bitsinv1  15781  nn0gcdid0  15859  nn0seqcvgd  15904  algcvga  15913  eucalgf  15917  nonsq  16089  odzdvds  16122  coprimeprodsq  16135  coprimeprodsq2  16136  oddprm  16137  iserodd  16162  pcexp  16186  pcidlem  16198  pc11  16206  dvdsprmpweqle  16212  difsqpwdvds  16213  pcfac  16225  prmunb  16240  hashbc2  16332  cshwshashlem2  16420  mulgaddcom  18191  mulginvcom  18192  mulgz  18195  mulgdirlem  18198  mulgass  18204  mndodcongi  18602  oddvdsnn0  18603  odeq  18609  odmulg  18614  efgsdmi  18789  cyggex2  18948  fincygsubgodd  19165  mulgass2  19282  chrrhm  20608  zncrng  20621  znzrh2  20622  zndvds  20626  znchr  20639  znunit  20640  chfacfisf  21392  chfacfisfcpmat  21393  chfacfscmulfsupp  21397  chfacfpmmulfsupp  21401  clmmulg  23634  itgcnlem  24319  degltlem1  24595  plyco0  24711  dgreq0  24784  plydivex  24815  aannenlem1  24846  abelthlem1  24948  abelthlem3  24950  abelthlem8  24956  abelthlem9  24957  advlogexp  25165  cxpexp  25178  leibpilem1OLD  25446  leibpi  25448  log2cnv  25450  log2tlbnd  25451  basellem2  25587  sgmnncl  25652  chpp1  25660  bcmono  25781  bcmax  25782  bcp1ctr  25783  lgsneg1  25826  lgsdirnn0  25848  lgsdinn0  25849  2lgslem1c  25897  2lgslem3a1  25904  2lgslem3b1  25905  2lgslem3c1  25906  2lgsoddprmlem2  25913  2sq2  25937  2sqreultlem  25951  dchrisumlem1  25993  qabvle  26129  ostth2lem2  26138  tgldimor  26216  upgrewlkle2  27316  wlkv0  27360  redwlk  27382  pthdadjvtx  27439  pthdlem1  27475  wwlknvtx  27551  wlkiswwlks2lem3  27577  wwlksm1edg  27587  wwlksnred  27598  wwlksnext  27599  clwlkclwwlklem2a1  27698  clwlkclwwlklem2a2  27699  clwlkclwwlklem2fv1  27701  clwlkclwwlklem2fv2  27702  clwlkclwwlklem2a4  27703  clwlkclwwlklem2a  27704  clwlkclwwlklem2  27706  clwlkclwwlk  27708  clwwisshclwwslem  27720  eucrctshift  27950  eucrct2eupth1  27951  eucrct2eupth  27952  numclwwlk5lem  28094  numclwwlk5  28095  numclwwlk7  28098  frgrreggt1  28100  nndiffz1  30436  xrge0mulgnn0  30604  hashf2  31243  signsvtn0  31740  nn0ltp1ne  32248  0nn0m1nnn0  32249  pthhashvtx  32272  fz0n  32860  bcneg1  32866  bccolsum  32869  faclimlem3  32875  faclim  32876  iprodfac  32877  poimirlem28  34802  mblfinlem1  34811  mblfinlem2  34812  numdenexp  39066  negexpidd  39159  nacsfix  39189  fzsplit1nn0  39231  eldioph2lem1  39237  fz1eqin  39246  diophin  39249  eq0rabdioph  39253  rexrabdioph  39271  rexzrexnn0  39281  irrapxlem4  39302  pell14qrss1234  39333  pell1qrss14  39345  monotoddzz  39420  rmxypos  39424  ltrmynn0  39425  ltrmxnn0  39426  lermxnn0  39427  rmxnn  39428  rmynn0  39434  jm2.17a  39437  jm2.17b  39438  rmygeid  39441  jm2.18  39465  jm2.19lem3  39468  jm2.19lem4  39469  jm2.22  39472  rmxdiophlem  39492  hbt  39610  proot1ex  39681  fzisoeu  41447  stirlinglem5  42244  elfzlble  43401  subsubelfzo0  43407  2ffzoeq  43409  fargshiftfo  43449  fmtnof1  43544  fmtnorec1  43546  goldbachthlem1  43554  odz2prm2pw  43572  flsqrt  43603  lighneallem4  43622  smndex1ibas  43970  smndex1iidm  43971  smndex2dnrinv  43985  smndex2dlinvh  43987  nn0eo  44486  nn0ofldiv2  44490  flnn0div2ge  44491  fllog2  44526  blenpw2  44536  blennngt2o2  44550  nn0digval  44558  dignn0fr  44559  digexp  44565  0dig2nn0e  44570  0dig2nn0o  44571  dig2bits  44572  dignn0flhalflem2  44574  dignn0ehalf  44575  dignn0flhalf  44576  nn0sumshdiglemB  44578
  Copyright terms: Public domain W3C validator