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

Theorem elnn0 10872
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 10871 . . 3  |-  NN0  =  ( NN  u.  { 0 } )
21eleq2i 2500 . 2  |-  ( A  e.  NN0  <->  A  e.  ( NN  u.  { 0 } ) )
3 elun 3606 . 2  |-  ( A  e.  ( NN  u.  { 0 } )  <->  ( A  e.  NN  \/  A  e. 
{ 0 } ) )
4 c0ex 9638 . . . 4  |-  0  e.  _V
54elsnc2 4027 . . 3  |-  ( A  e.  { 0 }  <-> 
A  =  0 )
65orbi2i 521 . 2  |-  ( ( A  e.  NN  \/  A  e.  { 0 } )  <->  ( A  e.  NN  \/  A  =  0 ) )
72, 3, 63bitri 274 1  |-  ( A  e.  NN0  <->  ( A  e.  NN  \/  A  =  0 ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    \/ wo 369    = wceq 1437    e. wcel 1868    u. cun 3434   {csn 3996   0cc0 9540   NNcn 10610   NN0cn0 10870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-1cn 9598  ax-icn 9599  ax-addcl 9600  ax-mulcl 9602  ax-i2m1 9608
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-v 3083  df-un 3441  df-sn 3997  df-n0 10871
This theorem is referenced by:  0nn0  10885  nn0ge0  10896  nnnn0addcl  10901  nnm1nn0  10912  elnnnn0b  10915  nn0sub  10921  elnn0z  10951  elznn0nn  10952  elznn0  10953  elznn  10954  nn0lt10b  10999  nn0ind-raph  11036  expp1  12279  expneg  12280  expcllem  12283  facp1  12464  faclbnd  12475  faclbnd3  12477  faclbnd4lem1  12478  faclbnd4lem3  12480  faclbnd4  12482  bcn1  12498  bcval5  12503  hashv01gt1  12528  hashnncl  12547  seqcoll2  12626  relexpsucr  13081  relexpsucl  13085  relexpcnv  13087  relexprelg  13090  relexpdmg  13094  relexprng  13098  relexpfld  13101  relexpaddg  13105  fz1f1o  13764  arisum  13906  arisum2  13907  geomulcvg  13920  fprodfac  14015  ef0lem  14121  dvdseq  14340  bezoutlem3OLD  14493  bezoutlem3  14496  mulgcd  14502  eucalgf  14530  eucalginv  14531  eucalglt  14532  prmdvdsexpr  14657  rpexp1i  14661  nn0gcdsq  14689  odzdvds  14728  odzdvdsOLD  14734  pceq0  14808  fldivp1  14830  pockthg  14838  1arith  14859  4sqlem17OLD  14893  4sqlem17  14899  4sqlem19  14901  vdwmc2  14917  vdwlem13  14931  0ram  14966  ram0  14968  ramz  14971  ramcl  14975  mulgnn0p1  16757  mulgnn0subcl  16759  mulgneg  16764  mulgnn0z  16766  mulgnn0dir  16769  mulgnn0ass  16775  submmulg  16781  odcl  17173  mndodcongi  17180  oddvdsnn0  17181  odnncl  17182  oddvds  17184  odclOLD  17189  dfod2  17203  odcl2  17204  gexcl  17219  gexdvds  17223  gexnnod  17228  sylow1lem1  17238  mulgnn0di  17454  torsubg  17480  ablfac1eu  17694  evlslem3  18725  gzrngunitlem  19020  zringlpirlem3OLD  19042  zringlpirlem3  19044  prmirredlem  19051  prmirred  19053  znf1o  19109  dscmet  21574  dvexp2  22895  tdeglem4  22996  dgrnznn  23188  coefv0  23189  dgreq0  23206  dgrcolem2  23215  dvply1  23224  aaliou2  23283  radcnv0  23358  logfac  23537  logtayl  23592  cxpexp  23600  leibpilem1  23853  birthdaylem2  23865  harmonicbnd3  23920  sqf11  24053  ppiltx  24091  sqff1o  24096  lgsdir  24245  lgsabs1  24249  lgseisenlem1  24264  2sqlem7  24285  2sqblem  24292  chebbnd1lem1  24294  gxnn0neg  25977  gxnn0suc  25978  znsqcld  28317  xrsmulgzz  28435  ressmulgnn0  28441  nexple  28827  eulerpartlemsv2  29187  eulerpartlemv  29193  eulerpartlemb  29197  eulerpartlemf  29199  eulerpartlemgvv  29205  eulerpartlemgh  29207  fz0n  30359  bccolsum  30370  nn0prpw  30972  fzsplit1nn0  35515  pell1qrgaplem  35639  monotoddzzfi  35710  jm2.22  35770  jm2.23  35771  rmydioph  35789  expdioph  35798  rp-isfinite6  36083  relexpss1d  36157  relexpmulg  36162  iunrelexpmin2  36164  relexp0a  36168  relexpxpmin  36169  relexpaddss  36170  wallispilem3  37749  etransclem24  37943  nn0o1gt2ALTV  38535  nn0oALTV  38537  ztprmneprm  39402  nn0enne  39600  nn0o1gt2  39601  blennn0elnn  39662  blen1b  39673  nn0sumshdiglem1  39706
  Copyright terms: Public domain W3C validator