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

Theorem elnn0 10682
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 10681 . . 3  |-  NN0  =  ( NN  u.  { 0 } )
21eleq2i 2529 . 2  |-  ( A  e.  NN0  <->  A  e.  ( NN  u.  { 0 } ) )
3 elun 3595 . 2  |-  ( A  e.  ( NN  u.  { 0 } )  <->  ( A  e.  NN  \/  A  e. 
{ 0 } ) )
4 c0ex 9481 . . . 4  |-  0  e.  _V
54elsnc2 4006 . . 3  |-  ( A  e.  { 0 }  <-> 
A  =  0 )
65orbi2i 519 . 2  |-  ( ( A  e.  NN  \/  A  e.  { 0 } )  <->  ( A  e.  NN  \/  A  =  0 ) )
72, 3, 63bitri 271 1  |-  ( A  e.  NN0  <->  ( A  e.  NN  \/  A  =  0 ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    \/ wo 368    = wceq 1370    e. wcel 1758    u. cun 3424   {csn 3975   0cc0 9383   NNcn 10423   NN0cn0 10680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-mulcl 9445  ax-i2m1 9451
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3070  df-un 3431  df-sn 3976  df-n0 10681
This theorem is referenced by:  0nn0  10695  nn0ge0  10706  nnnn0addcl  10711  nnm1nn0  10722  elnnnn0b  10725  nn0sub  10731  elnn0z  10760  elznn0nn  10761  elznn0  10762  elznn  10763  nn0ind-raph  10843  expp1  11973  expneg  11974  expcllem  11977  facp1  12157  faclbnd  12167  faclbnd3  12169  faclbnd4lem1  12170  faclbnd4lem3  12172  faclbnd4  12174  bcn1  12190  bcval5  12195  hashv01gt1  12217  hashnncl  12235  seqcoll2  12319  fz1f1o  13289  arisum  13424  arisum2  13425  geomulcvg  13438  ef0lem  13466  dvdseq  13682  bezoutlem3  13826  mulgcd  13832  eucalgf  13860  eucalginv  13861  eucalglt  13862  prmdvdsexpr  13904  rpexp1i  13909  nn0gcdsq  13932  odzdvds  13969  pceq0  14039  fldivp1  14061  pockthg  14069  1arith  14090  4sqlem17  14124  4sqlem19  14126  vdwmc2  14142  vdwlem13  14156  0ram  14183  ram0  14185  ramz  14188  ramcl  14192  mulgnn0p1  15740  mulgnn0subcl  15742  mulgneg  15747  mulgnn0z  15749  mulgnn0dir  15752  mulgnn0ass  15758  submmulg  15764  odcl  16143  mndodcongi  16150  oddvdsnn0  16151  odnncl  16152  oddvds  16154  dfod2  16169  odcl2  16170  gexcl  16183  gexdvds  16187  gexnnod  16191  sylow1lem1  16201  mulgnn0di  16417  torsubg  16440  ablfac1eu  16679  evlslem3  17707  gzrngunitlem  17986  zringlpirlem3  18014  zlpirlem3  18019  prmirredlem  18026  prmirred  18028  prmirredlemOLD  18029  prmirredOLD  18031  znf1o  18093  dscmet  20281  dvexp2  21544  tdeglem4  21645  coefv0  21831  dgreq0  21848  dgrcolem2  21857  dvply1  21866  aaliou2  21922  radcnv0  21997  logfac  22165  logtayl  22221  cxpexp  22229  leibpilem1  22451  birthdaylem2  22462  harmonicbnd3  22517  sqf11  22593  ppiltx  22631  sqff1o  22636  lgsdir  22785  lgsabs1  22789  lgseisenlem1  22804  2sqlem7  22825  2sqblem  22832  chebbnd1lem1  22834  gxnn0neg  23885  gxnn0suc  23886  xrsmulgzz  26273  ressmulgnn0  26279  nexple  26582  eulerpartlemsv2  26875  eulerpartlemv  26881  eulerpartlemb  26885  eulerpartlemf  26887  eulerpartlemgvv  26893  eulerpartlemgh  26895  fz0n  27523  fprodfac  27617  nn0prpw  28656  fzsplit1nn0  29230  pell1qrgaplem  29352  monotoddzzfi  29421  jm2.22  29482  jm2.23  29483  rmydioph  29501  expdioph  29510  dgrnznn  29630  wallispilem3  30000  ztprmneprm  30877
  Copyright terms: Public domain W3C validator