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

Theorem nn0z 12482
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 12480 . 2 0 ⊆ ℤ
21sseli 3938 1 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  0cn0 12371  cz 12457
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5254  ax-nul 5261  ax-pr 5382  ax-un 7664  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-i2m1 11077  ax-1ne0 11078  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7354  df-om 7795  df-2nd 7914  df-frecs 8204  df-wrecs 8235  df-recs 8309  df-rdg 8348  df-neg 11346  df-nn 12112  df-n0 12372  df-z 12458
This theorem is referenced by:  nn0negz  12499  nn0ltp1le  12519  nn0leltp1  12520  nn0ltlem1  12521  nn0lt2  12524  nn0le2is012  12525  nn0lem1lt  12526  fnn0ind  12560  nn0pzuz  12784  nn0ge2m1nnALT  12821  fz1n  13413  ige2m1fz  13485  elfz2nn0  13486  fznn0  13487  elfz0add  13494  fzctr  13507  difelfzle  13508  fzoun  13563  fzofzim  13573  fzo1fzo0n0  13577  elincfzoext  13584  elfzodifsumelfzo  13592  fz0add1fz1  13596  zpnn0elfzo  13599  fzossfzop1  13604  ubmelm1fzo  13622  elfznelfzo  13631  flmulnn0  13686  quoremnn0  13715  zmodidfzoimp  13760  modmuladdnn0  13774  modfzo0difsn  13802  expdiv  13973  expnngt1  14098  faclbnd3  14146  bccmpl  14163  bcnp1n  14168  bcval5  14172  bcn2  14173  bcp1m1  14174  hashge2el2difr  14334  fi1uzind  14350  wrdred1  14402  wrdred1hash  14403  ccatalpha  14435  swrdnd0  14503  swrdfv2  14507  swrdsb0eq  14509  swrdsbslen  14510  swrdspsleq  14511  swrdlsw  14513  pfxnd  14533  pfxccatin12lem4  14572  pfxccatin12lem3  14578  pfxccat3  14580  swrdccat  14581  pfxccat3a  14584  revlen  14608  repswswrd  14630  repswccat  14632  cshwidxmodr  14650  cshf1  14656  2cshw  14659  cshweqrep  14667  cshwcshid  14674  cshwcsh2id  14675  cats1fv  14706  swrd2lsw  14799  2swrd2eqwrdeq  14800  isercoll  15512  iseraltlem2  15527  bcxmas  15680  geo2sum2  15719  geomulcvg  15721  risefacval2  15853  fallfacval2  15854  zrisefaccl  15863  zfallfaccl  15864  fallrisefac  15868  bpolylem  15891  fsumkthpow  15899  esum  15923  ege2le3  15932  eftlcl  15949  reeftlcl  15950  eftlub  15951  effsumlt  15953  eirrlem  16046  dvds1  16161  dvdsext  16163  addmodlteqALT  16167  oddnn02np1  16190  oddge22np1  16191  nn0ehalf  16220  nn0o1gt2  16223  nno  16224  nn0o  16225  nn0oddm1d2  16227  divalglem4  16238  divalglem5  16239  modremain  16250  bitsinv1  16282  nn0gcdid0  16361  nn0seqcvgd  16406  algcvga  16415  eucalgf  16419  nonsq  16594  odzdvds  16627  coprimeprodsq  16640  coprimeprodsq2  16641  oddprm  16642  iserodd  16667  pcexp  16691  pcidlem  16704  pc11  16712  dvdsprmpweqle  16718  difsqpwdvds  16719  pcfac  16731  prmunb  16746  hashbc2  16838  cshwshashlem2  16929  smndex1ibas  18670  smndex1iidm  18671  smndex2dnrinv  18685  smndex2dlinvh  18687  mulgaddcom  18859  mulginvcom  18860  mulgz  18863  mulgdirlem  18866  mulgass  18872  mndodcongi  19284  oddvdsnn0  19285  odeq  19291  odmulg  19297  efgsdmi  19473  cyggex2  19633  fincygsubgodd  19850  mulgass2  19978  chrrhm  20887  zncrng  20904  znzrh2  20905  zndvds  20909  znchr  20922  znunit  20923  chfacfisf  22155  chfacfisfcpmat  22156  chfacfscmulfsupp  22160  chfacfpmmulfsupp  22164  clmmulg  24416  itgcnlem  25106  degltlem1  25389  plyco0  25505  dgreq0  25578  plydivex  25609  aannenlem1  25640  abelthlem1  25742  abelthlem3  25744  abelthlem8  25750  abelthlem9  25751  advlogexp  25962  cxpexp  25975  leibpi  26244  log2cnv  26246  log2tlbnd  26247  basellem2  26383  sgmnncl  26448  chpp1  26456  bcmono  26577  bcmax  26578  bcp1ctr  26579  lgsneg1  26622  lgsdirnn0  26644  lgsdinn0  26645  2lgslem1c  26693  2lgslem3a1  26700  2lgslem3b1  26701  2lgslem3c1  26702  2lgsoddprmlem2  26709  2sq2  26733  2sqreultlem  26747  dchrisumlem1  26789  qabvle  26925  ostth2lem2  26934  tgldimor  27273  upgrewlkle2  28383  wlkv0  28428  redwlk  28449  pthdadjvtx  28507  pthdlem1  28543  wwlknvtx  28619  wlkiswwlks2lem3  28645  wwlksm1edg  28655  wwlksnred  28666  wwlksnext  28667  clwlkclwwlklem2a1  28765  clwlkclwwlklem2a2  28766  clwlkclwwlklem2fv1  28768  clwlkclwwlklem2fv2  28769  clwlkclwwlklem2a4  28770  clwlkclwwlklem2a  28771  clwlkclwwlklem2  28773  clwlkclwwlk  28775  clwwisshclwwslem  28787  eucrctshift  29016  eucrct2eupth1  29017  eucrct2eupth  29018  numclwwlk5lem  29160  numclwwlk5  29161  numclwwlk7  29164  frgrreggt1  29166  nndiffz1  31515  xrge0mulgnn0  31706  hashf2  32495  signsvtn0  32994  nn0ltp1ne  33514  0nn0m1nnn0  33515  pthhashvtx  33533  fz0n  34119  bcneg1  34125  bccolsum  34128  faclimlem3  34134  faclim  34135  iprodfac  34136  poimirlem28  36044  mblfinlem1  36053  mblfinlem2  36054  lcmineqlem2  40425  sticksstones22  40514  gcdnn0id  40724  numdenexp  40732  negexpidd  40914  nacsfix  40944  fzsplit1nn0  40986  eldioph2lem1  40992  fz1eqin  41001  diophin  41004  eq0rabdioph  41008  rexrabdioph  41026  rexzrexnn0  41036  irrapxlem4  41057  pell14qrss1234  41088  pell1qrss14  41100  monotoddzz  41176  rmxypos  41180  ltrmynn0  41181  ltrmxnn0  41182  lermxnn0  41183  rmxnn  41184  rmynn0  41190  jm2.17a  41193  jm2.17b  41194  rmygeid  41197  jm2.18  41221  jm2.19lem3  41224  jm2.19lem4  41225  jm2.22  41228  rmxdiophlem  41248  hbt  41366  proot1ex  41437  fzisoeu  43439  stirlinglem5  44220  elfzlble  45453  subsubelfzo0  45459  2ffzoeq  45461  fargshiftfo  45535  fmtnof1  45628  fmtnorec1  45630  goldbachthlem1  45638  odz2prm2pw  45656  flsqrt  45686  lighneallem4  45703  nn0eo  46515  nn0ofldiv2  46519  flnn0div2ge  46520  fllog2  46555  blenpw2  46565  blennngt2o2  46579  nn0digval  46587  dignn0fr  46588  digexp  46594  0dig2nn0e  46599  0dig2nn0o  46600  dig2bits  46601  dignn0flhalflem2  46603  dignn0ehalf  46604  dignn0flhalf  46605  nn0sumshdiglemB  46607
  Copyright terms: Public domain W3C validator