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

Theorem elnn0 10225
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 10224 . . 3  |-  NN0  =  ( NN  u.  { 0 } )
21eleq2i 2502 . 2  |-  ( A  e.  NN0  <->  A  e.  ( NN  u.  { 0 } ) )
3 elun 3490 . 2  |-  ( A  e.  ( NN  u.  { 0 } )  <->  ( A  e.  NN  \/  A  e. 
{ 0 } ) )
4 c0ex 9087 . . . 4  |-  0  e.  _V
54elsnc2 3845 . . 3  |-  ( A  e.  { 0 }  <-> 
A  =  0 )
65orbi2i 507 . 2  |-  ( ( A  e.  NN  \/  A  e.  { 0 } )  <->  ( A  e.  NN  \/  A  =  0 ) )
72, 3, 63bitri 264 1  |-  ( A  e.  NN0  <->  ( A  e.  NN  \/  A  =  0 ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    \/ wo 359    = wceq 1653    e. wcel 1726    u. cun 3320   {csn 3816   0cc0 8992   NNcn 10002   NN0cn0 10223
This theorem is referenced by:  0nn0  10238  nn0ge0  10249  nnnn0addcl  10253  nnm1nn0  10263  elnnnn0b  10266  nn0sub  10272  elnn0z  10296  elznn0nn  10297  elznn0  10298  elznn  10299  nn0ind-raph  10372  expp1  11390  expneg  11391  expcllem  11394  facp1  11573  faclbnd  11583  faclbnd3  11585  faclbnd4lem1  11586  faclbnd4lem3  11588  faclbnd4  11590  bcn1  11606  bcval5  11611  hashv01gt1  11631  hashnncl  11647  seqcoll2  11715  fz1f1o  12506  arisum  12641  arisum2  12642  geomulcvg  12655  ef0lem  12683  dvdseq  12899  bezoutlem3  13042  mulgcd  13048  eucalgf  13076  eucalginv  13077  eucalglt  13078  prmdvdsexpr  13118  rpexp1i  13123  nn0gcdsq  13146  odzdvds  13183  pceq0  13246  fldivp1  13268  pockthg  13276  1arith  13297  4sqlem17  13331  4sqlem19  13333  vdwmc2  13349  vdwlem13  13363  0ram  13390  ram0  13392  ramz  13395  ramcl  13399  mulgnn0p1  14903  mulgnn0subcl  14905  mulgneg  14910  mulgnn0z  14912  mulgnn0dir  14915  mulgnn0ass  14921  submmulg  14927  odcl  15176  mndodcongi  15183  oddvdsnn0  15184  odnncl  15185  oddvds  15187  dfod2  15202  odcl2  15203  gexcl  15216  gexdvds  15220  gexnnod  15224  sylow1lem1  15234  mulgnn0di  15450  torsubg  15471  ablfac1eu  15633  gzrngunitlem  16765  zlpirlem3  16772  prmirredlem  16775  prmirred  16777  znf1o  16834  dscmet  18622  dvexp2  19842  evlslem3  19937  tdeglem4  19985  coefv0  20168  dgreq0  20185  dgrcolem2  20194  dvply1  20203  aaliou2  20259  radcnv0  20334  logfac  20497  logtayl  20553  cxpexp  20561  leibpilem1  20782  birthdaylem2  20793  harmonicbnd3  20848  sqf11  20924  ppiltx  20962  sqff1o  20967  lgsdir  21116  lgsabs1  21120  lgseisenlem1  21135  2sqlem7  21156  2sqblem  21163  chebbnd1lem1  21165  gxnn0neg  21853  gxnn0suc  21854  xrsmulgzz  24202  ressmulgnn0  24208  fz0n  25204  fprodfac  25298  nn0prpw  26328  fzsplit1nn0  26814  pell1qrgaplem  26938  monotoddzzfi  27007  jm2.22  27068  jm2.23  27069  rmydioph  27087  expdioph  27096  dgrnznn  27319  wallispilem3  27794
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-mulcl 9054  ax-i2m1 9060
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-un 3327  df-sn 3822  df-n0 10224
  Copyright terms: Public domain W3C validator