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

Theorem elnn0 10569
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 10568 . . 3  |-  NN0  =  ( NN  u.  { 0 } )
21eleq2i 2497 . 2  |-  ( A  e.  NN0  <->  A  e.  ( NN  u.  { 0 } ) )
3 elun 3485 . 2  |-  ( A  e.  ( NN  u.  { 0 } )  <->  ( A  e.  NN  \/  A  e. 
{ 0 } ) )
4 c0ex 9368 . . . 4  |-  0  e.  _V
54elsnc2 3896 . . 3  |-  ( A  e.  { 0 }  <-> 
A  =  0 )
65orbi2i 516 . 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 1362    e. wcel 1755    u. cun 3314   {csn 3865   0cc0 9270   NNcn 10310   NN0cn0 10567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-mulcl 9332  ax-i2m1 9338
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-un 3321  df-sn 3866  df-n0 10568
This theorem is referenced by:  0nn0  10582  nn0ge0  10593  nnnn0addcl  10598  nnm1nn0  10609  elnnnn0b  10612  nn0sub  10618  elnn0z  10647  elznn0nn  10648  elznn0  10649  elznn  10650  nn0ind-raph  10730  expp1  11856  expneg  11857  expcllem  11860  facp1  12040  faclbnd  12050  faclbnd3  12052  faclbnd4lem1  12053  faclbnd4lem3  12055  faclbnd4  12057  bcn1  12073  bcval5  12078  hashv01gt1  12100  hashnncl  12118  seqcoll2  12201  fz1f1o  13171  arisum  13305  arisum2  13306  geomulcvg  13319  ef0lem  13347  dvdseq  13563  bezoutlem3  13707  mulgcd  13713  eucalgf  13741  eucalginv  13742  eucalglt  13743  prmdvdsexpr  13785  rpexp1i  13790  nn0gcdsq  13813  odzdvds  13850  pceq0  13920  fldivp1  13942  pockthg  13950  1arith  13971  4sqlem17  14005  4sqlem19  14007  vdwmc2  14023  vdwlem13  14037  0ram  14064  ram0  14066  ramz  14069  ramcl  14073  mulgnn0p1  15618  mulgnn0subcl  15620  mulgneg  15625  mulgnn0z  15627  mulgnn0dir  15630  mulgnn0ass  15636  submmulg  15642  odcl  16019  mndodcongi  16026  oddvdsnn0  16027  odnncl  16028  oddvds  16030  dfod2  16045  odcl2  16046  gexcl  16059  gexdvds  16063  gexnnod  16067  sylow1lem1  16077  mulgnn0di  16293  torsubg  16316  ablfac1eu  16548  gzrngunitlem  17721  zringlpirlem3  17747  zlpirlem3  17752  prmirredlem  17759  prmirred  17761  prmirredlemOLD  17762  prmirredOLD  17764  znf1o  17826  dscmet  20007  dvexp2  21270  evlslem3  21366  tdeglem4  21414  coefv0  21600  dgreq0  21617  dgrcolem2  21626  dvply1  21635  aaliou2  21691  radcnv0  21766  logfac  21934  logtayl  21990  cxpexp  21998  leibpilem1  22220  birthdaylem2  22231  harmonicbnd3  22286  sqf11  22362  ppiltx  22400  sqff1o  22405  lgsdir  22554  lgsabs1  22558  lgseisenlem1  22573  2sqlem7  22594  2sqblem  22601  chebbnd1lem1  22603  gxnn0neg  23573  gxnn0suc  23574  xrsmulgzz  25962  ressmulgnn0  25968  nexple  26302  eulerpartlemsv2  26589  eulerpartlemv  26595  eulerpartlemb  26599  eulerpartlemf  26601  eulerpartlemgvv  26607  eulerpartlemgh  26609  fz0n  27236  fprodfac  27330  nn0prpw  28362  fzsplit1nn0  28937  pell1qrgaplem  29059  monotoddzzfi  29128  jm2.22  29189  jm2.23  29190  rmydioph  29208  expdioph  29217  dgrnznn  29337  wallispilem3  29708  ztprmneprm  30583
  Copyright terms: Public domain W3C validator