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

Theorem elnn0 10822
Description: Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-2002.)
Assertion
Ref Expression
elnn0

Proof of Theorem elnn0
StepHypRef Expression
1 df-n0 10821 . . 3
21eleq2i 2535 . 2
3 elun 3644 . 2
4 c0ex 9611 . . . 4
54elsnc2 4060 . . 3
65orbi2i 519 . 2
72, 3, 63bitri 271 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  \/wo 368  =wceq 1395  e.wcel 1818  u.cun 3473  {csn 4029  0cc0 9513   cn 10561   cn0 10820
This theorem is referenced by:  0nn0  10835  nn0ge0  10846  nnnn0addcl  10851  nnm1nn0  10862  elnnnn0b  10865  nn0sub  10871  elnn0z  10902  elznn0nn  10903  elznn0  10904  elznn  10905  nn0lt10b  10950  nn0ind-raph  10989  expp1  12173  expneg  12174  expcllem  12177  facp1  12358  faclbnd  12368  faclbnd3  12370  faclbnd4lem1  12371  faclbnd4lem3  12373  faclbnd4  12375  bcn1  12391  bcval5  12396  hashv01gt1  12418  hashnncl  12436  seqcoll2  12513  fz1f1o  13532  arisum  13671  arisum2  13672  geomulcvg  13685  fprodfac  13777  ef0lem  13814  dvdseq  14033  bezoutlem3  14178  mulgcd  14184  eucalgf  14212  eucalginv  14213  eucalglt  14214  prmdvdsexpr  14257  rpexp1i  14262  nn0gcdsq  14285  odzdvds  14322  pceq0  14394  fldivp1  14416  pockthg  14424  1arith  14445  4sqlem17  14479  4sqlem19  14481  vdwmc2  14497  vdwlem13  14511  0ram  14538  ram0  14540  ramz  14543  ramcl  14547  mulgnn0p1  16153  mulgnn0subcl  16155  mulgneg  16160  mulgnn0z  16162  mulgnn0dir  16165  mulgnn0ass  16171  submmulg  16177  odcl  16560  mndodcongi  16567  oddvdsnn0  16568  odnncl  16569  oddvds  16571  dfod2  16586  odcl2  16587  gexcl  16600  gexdvds  16604  gexnnod  16608  sylow1lem1  16618  mulgnn0di  16834  torsubg  16860  ablfac1eu  17124  evlslem3  18183  gzrngunitlem  18482  zringlpirlem3  18511  zlpirlem3  18516  prmirredlem  18523  prmirred  18525  prmirredlemOLD  18526  prmirredOLD  18528  znf1o  18590  dscmet  21093  dvexp2  22357  tdeglem4  22458  dgrnznn  22644  coefv0  22645  dgreq0  22662  dgrcolem2  22671  dvply1  22680  aaliou2  22736  radcnv0  22811  logfac  22985  logtayl  23041  cxpexp  23049  leibpilem1  23271  birthdaylem2  23282  harmonicbnd3  23337  sqf11  23413  ppiltx  23451  sqff1o  23456  lgsdir  23605  lgsabs1  23609  lgseisenlem1  23624  2sqlem7  23645  2sqblem  23652  chebbnd1lem1  23654  gxnn0neg  25265  gxnn0suc  25266  znsqcld  27561  xrsmulgzz  27666  ressmulgnn0  27672  nexple  28005  eulerpartlemsv2  28297  eulerpartlemv  28303  eulerpartlemb  28307  eulerpartlemf  28309  eulerpartlemgvv  28315  eulerpartlemgh  28317  fz0n  29110  nn0prpw  30141  fzsplit1nn0  30687  pell1qrgaplem  30809  monotoddzzfi  30878  jm2.22  30937  jm2.23  30938  rmydioph  30956  expdioph  30965  wallispilem3  31849  etransclem24  32041  ztprmneprm  32936  rp-isfinite6  37744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-mulcl 9575  ax-i2m1 9581
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-sn 4030  df-n0 10821
  Copyright terms: Public domain W3C validator