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

Theorem elnn0 9983
Description: Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-2002.)
Assertion
Ref Expression
elnn0  |-  ( A  e.  NN0  <->  ( A  e.  NN  \/  A  =  0 ) )

Proof of Theorem elnn0
StepHypRef Expression
1 df-n0 9982 . . 3  |-  NN0  =  ( NN  u.  { 0 } )
21eleq2i 2360 . 2  |-  ( A  e.  NN0  <->  A  e.  ( NN  u.  { 0 } ) )
3 elun 3329 . 2  |-  ( A  e.  ( NN  u.  { 0 } )  <->  ( A  e.  NN  \/  A  e. 
{ 0 } ) )
4 c0ex 8848 . . . 4  |-  0  e.  _V
54elsnc2 3682 . . 3  |-  ( A  e.  { 0 }  <-> 
A  =  0 )
65orbi2i 505 . 2  |-  ( ( A  e.  NN  \/  A  e.  { 0 } )  <->  ( A  e.  NN  \/  A  =  0 ) )
72, 3, 63bitri 262 1  |-  ( A  e.  NN0  <->  ( A  e.  NN  \/  A  =  0 ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    \/ wo 357    = wceq 1632    e. wcel 1696    u. cun 3163   {csn 3653   0cc0 8753   NNcn 9762   NN0cn0 9981
This theorem is referenced by:  0nn0  9996  nn0ge0  10007  nnnn0addcl  10011  nnm1nn0  10021  elnnnn0b  10024  nn0sub  10030  elnn0z  10052  elznn0nn  10053  elznn0  10054  elznn  10055  nn0ind-raph  10128  expp1  11126  expneg  11127  expcllem  11130  facp1  11309  faclbnd  11319  faclbnd3  11321  faclbnd4lem1  11322  faclbnd4lem3  11324  faclbnd4  11326  bcn1  11341  bcval5  11346  hashnncl  11370  seqcoll2  11418  fz1f1o  12199  arisum  12334  arisum2  12335  geomulcvg  12348  ef0lem  12376  dvdseq  12592  bezoutlem3  12735  mulgcd  12741  eucalgf  12769  eucalginv  12770  eucalglt  12771  prmdvdsexpr  12811  rpexp1i  12816  nn0gcdsq  12839  odzdvds  12876  pceq0  12939  fldivp1  12961  pockthg  12969  1arith  12990  4sqlem17  13024  4sqlem19  13026  vdwmc2  13042  vdwlem13  13056  0ram  13083  ram0  13085  ramz  13088  ramcl  13092  mulgnn0p1  14594  mulgnn0subcl  14596  mulgneg  14601  mulgnn0z  14603  mulgnn0dir  14606  mulgnn0ass  14612  submmulg  14618  odcl  14867  mndodcongi  14874  oddvdsnn0  14875  odnncl  14876  oddvds  14878  dfod2  14893  odcl2  14894  gexcl  14907  gexdvds  14911  gexnnod  14915  sylow1lem1  14925  mulgnn0di  15141  torsubg  15162  ablfac1eu  15324  gzrngunitlem  16452  zlpirlem3  16459  prmirredlem  16462  prmirred  16464  znf1o  16521  dscmet  18111  dvexp2  19319  evlslem3  19414  tdeglem4  19462  coefv0  19645  dgreq0  19662  dgrcolem2  19671  dvply1  19680  aaliou2  19736  radcnv0  19808  logfac  19970  logtayl  20023  cxpexp  20031  leibpilem1  20252  birthdaylem2  20263  harmonicbnd3  20317  sqf11  20393  ppiltx  20431  sqff1o  20436  lgsdir  20585  lgsabs1  20589  lgseisenlem1  20604  2sqlem7  20625  2sqblem  20632  chebbnd1lem1  20634  gxnn0neg  20946  gxnn0suc  20947  xrsmulgzz  23322  ressmulgnn0  23324  fz0n  24112  nn0prpw  26342  fzsplit1nn0  26936  pell1qrgaplem  27061  monotoddzzfi  27130  jm2.22  27191  jm2.23  27192  rmydioph  27210  expdioph  27219  dgrnznn  27443  wallispilem3  27919
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-mulcl 8815  ax-i2m1 8821
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-sn 3659  df-n0 9982
  Copyright terms: Public domain W3C validator