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

Theorem elnn0 10803
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 10802 . . 3  |-  NN0  =  ( NN  u.  { 0 } )
21eleq2i 2521 . 2  |-  ( A  e.  NN0  <->  A  e.  ( NN  u.  { 0 } ) )
3 elun 3630 . 2  |-  ( A  e.  ( NN  u.  { 0 } )  <->  ( A  e.  NN  \/  A  e. 
{ 0 } ) )
4 c0ex 9593 . . . 4  |-  0  e.  _V
54elsnc2 4045 . . 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 1383    e. wcel 1804    u. cun 3459   {csn 4014   0cc0 9495   NNcn 10542   NN0cn0 10801
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-mulcl 9557  ax-i2m1 9563
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-sn 4015  df-n0 10802
This theorem is referenced by:  0nn0  10816  nn0ge0  10827  nnnn0addcl  10832  nnm1nn0  10843  elnnnn0b  10846  nn0sub  10852  elnn0z  10883  elznn0nn  10884  elznn0  10885  elznn  10886  nn0lt10b  10931  nn0ind-raph  10969  expp1  12152  expneg  12153  expcllem  12156  facp1  12337  faclbnd  12347  faclbnd3  12349  faclbnd4lem1  12350  faclbnd4lem3  12352  faclbnd4  12354  bcn1  12370  bcval5  12375  hashv01gt1  12397  hashnncl  12415  seqcoll2  12492  fz1f1o  13511  arisum  13650  arisum2  13651  geomulcvg  13664  ef0lem  13692  dvdseq  13910  bezoutlem3  14055  mulgcd  14061  eucalgf  14089  eucalginv  14090  eucalglt  14091  prmdvdsexpr  14134  rpexp1i  14139  nn0gcdsq  14162  odzdvds  14199  pceq0  14271  fldivp1  14293  pockthg  14301  1arith  14322  4sqlem17  14356  4sqlem19  14358  vdwmc2  14374  vdwlem13  14388  0ram  14415  ram0  14417  ramz  14420  ramcl  14424  mulgnn0p1  16027  mulgnn0subcl  16029  mulgneg  16034  mulgnn0z  16036  mulgnn0dir  16039  mulgnn0ass  16045  submmulg  16051  odcl  16434  mndodcongi  16441  oddvdsnn0  16442  odnncl  16443  oddvds  16445  dfod2  16460  odcl2  16461  gexcl  16474  gexdvds  16478  gexnnod  16482  sylow1lem1  16492  mulgnn0di  16708  torsubg  16734  ablfac1eu  16998  evlslem3  18057  gzrngunitlem  18356  zringlpirlem3  18384  zlpirlem3  18389  prmirredlem  18396  prmirred  18398  prmirredlemOLD  18399  prmirredOLD  18401  znf1o  18463  dscmet  20966  dvexp2  22230  tdeglem4  22331  coefv0  22517  dgreq0  22534  dgrcolem2  22543  dvply1  22552  aaliou2  22608  radcnv0  22683  logfac  22857  logtayl  22913  cxpexp  22921  leibpilem1  23143  birthdaylem2  23154  harmonicbnd3  23209  sqf11  23285  ppiltx  23323  sqff1o  23328  lgsdir  23477  lgsabs1  23481  lgseisenlem1  23496  2sqlem7  23517  2sqblem  23524  chebbnd1lem1  23526  gxnn0neg  25137  gxnn0suc  25138  znsqcld  27433  xrsmulgzz  27539  ressmulgnn0  27545  nexple  27878  eulerpartlemsv2  28170  eulerpartlemv  28176  eulerpartlemb  28180  eulerpartlemf  28182  eulerpartlemgvv  28188  eulerpartlemgh  28190  fz0n  28983  fprodfac  29077  nn0prpw  30116  fzsplit1nn0  30662  pell1qrgaplem  30784  monotoddzzfi  30853  jm2.22  30912  jm2.23  30913  rmydioph  30931  expdioph  30940  dgrnznn  31060  wallispilem3  31738  ztprmneprm  32669  rp-isfinite6  37447
  Copyright terms: Public domain W3C validator