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

Theorem elnn0 9967
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 9966 . . 3  |-  NN0  =  ( NN  u.  { 0 } )
21eleq2i 2347 . 2  |-  ( A  e.  NN0  <->  A  e.  ( NN  u.  { 0 } ) )
3 elun 3316 . 2  |-  ( A  e.  ( NN  u.  { 0 } )  <->  ( A  e.  NN  \/  A  e. 
{ 0 } ) )
4 c0ex 8832 . . . 4  |-  0  e.  _V
54elsnc2 3669 . . 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 1623    e. wcel 1684    u. cun 3150   {csn 3640   0cc0 8737   NNcn 9746   NN0cn0 9965
This theorem is referenced by:  0nn0  9980  nn0ge0  9991  nnnn0addcl  9995  nnm1nn0  10005  elnnnn0b  10008  nn0sub  10014  elnn0z  10036  elznn0nn  10037  elznn0  10038  elznn  10039  nn0ind-raph  10112  expp1  11110  expneg  11111  expcllem  11114  facp1  11293  faclbnd  11303  faclbnd3  11305  faclbnd4lem1  11306  faclbnd4lem3  11308  faclbnd4  11310  bcn1  11325  bcval5  11330  hashnncl  11354  seqcoll2  11402  fz1f1o  12183  arisum  12318  arisum2  12319  geomulcvg  12332  ef0lem  12360  dvdseq  12576  bezoutlem3  12719  mulgcd  12725  eucalgf  12753  eucalginv  12754  eucalglt  12755  prmdvdsexpr  12795  rpexp1i  12800  nn0gcdsq  12823  odzdvds  12860  pceq0  12923  fldivp1  12945  pockthg  12953  1arith  12974  4sqlem17  13008  4sqlem19  13010  vdwmc2  13026  vdwlem13  13040  0ram  13067  ram0  13069  ramz  13072  ramcl  13076  mulgnn0p1  14578  mulgnn0subcl  14580  mulgneg  14585  mulgnn0z  14587  mulgnn0dir  14590  mulgnn0ass  14596  submmulg  14602  odcl  14851  mndodcongi  14858  oddvdsnn0  14859  odnncl  14860  oddvds  14862  dfod2  14877  odcl2  14878  gexcl  14891  gexdvds  14895  gexnnod  14899  sylow1lem1  14909  mulgnn0di  15125  torsubg  15146  ablfac1eu  15308  gzrngunitlem  16436  zlpirlem3  16443  prmirredlem  16446  prmirred  16448  znf1o  16505  dscmet  18095  dvexp2  19303  evlslem3  19398  tdeglem4  19446  coefv0  19629  dgreq0  19646  dgrcolem2  19655  dvply1  19664  aaliou2  19720  radcnv0  19792  logfac  19954  logtayl  20007  cxpexp  20015  leibpilem1  20236  birthdaylem2  20247  harmonicbnd3  20301  sqf11  20377  ppiltx  20415  sqff1o  20420  lgsdir  20569  lgsabs1  20573  lgseisenlem1  20588  2sqlem7  20609  2sqblem  20616  chebbnd1lem1  20618  gxnn0neg  20930  gxnn0suc  20931  xrsmulgzz  23307  ressmulgnn0  23309  fz0n  24097  nn0prpw  26239  fzsplit1nn0  26833  pell1qrgaplem  26958  monotoddzzfi  27027  jm2.22  27088  jm2.23  27089  rmydioph  27107  expdioph  27116  dgrnznn  27340  wallispilem3  27816
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-mulcl 8799  ax-i2m1 8805
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-sn 3646  df-n0 9966
  Copyright terms: Public domain W3C validator