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

Theorem elnn0 10899
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 10898 . . 3  |-  NN0  =  ( NN  u.  { 0 } )
21eleq2i 2531 . 2  |-  ( A  e.  NN0  <->  A  e.  ( NN  u.  { 0 } ) )
3 elun 3585 . 2  |-  ( A  e.  ( NN  u.  { 0 } )  <->  ( A  e.  NN  \/  A  e. 
{ 0 } ) )
4 c0ex 9662 . . . 4  |-  0  e.  _V
54elsnc2 4010 . . 3  |-  ( A  e.  { 0 }  <-> 
A  =  0 )
65orbi2i 526 . 2  |-  ( ( A  e.  NN  \/  A  e.  { 0 } )  <->  ( A  e.  NN  \/  A  =  0 ) )
72, 3, 63bitri 279 1  |-  ( A  e.  NN0  <->  ( A  e.  NN  \/  A  =  0 ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    \/ wo 374    = wceq 1454    e. wcel 1897    u. cun 3413   {csn 3979   0cc0 9564   NNcn 10636   NN0cn0 10897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-mulcl 9626  ax-i2m1 9632
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-un 3420  df-sn 3980  df-n0 10898
This theorem is referenced by:  0nn0  10912  nn0ge0  10923  nnnn0addcl  10928  nnm1nn0  10939  elnnnn0b  10942  nn0sub  10948  elnn0z  10978  elznn0nn  10979  elznn0  10980  elznn  10981  nn0lt10b  11026  nn0ind-raph  11063  expp1  12310  expneg  12311  expcllem  12314  facp1  12495  faclbnd  12506  faclbnd3  12508  faclbnd4lem1  12509  faclbnd4lem3  12511  faclbnd4  12513  bcn1  12529  bcval5  12534  hashv01gt1  12559  hashnncl  12578  seqcoll2  12660  relexpsucr  13140  relexpsucl  13144  relexpcnv  13146  relexprelg  13149  relexpdmg  13153  relexprng  13157  relexpfld  13160  relexpaddg  13164  fz1f1o  13824  arisum  13966  arisum2  13967  geomulcvg  13980  fprodfac  14075  ef0lem  14181  dvdseq  14400  bezoutlem3OLD  14553  bezoutlem3  14556  mulgcd  14562  eucalgf  14590  eucalginv  14591  eucalglt  14592  prmdvdsexpr  14717  rpexp1i  14721  nn0gcdsq  14749  odzdvds  14788  odzdvdsOLD  14794  pceq0  14868  fldivp1  14890  pockthg  14898  1arith  14919  4sqlem17OLD  14953  4sqlem17  14959  4sqlem19  14961  vdwmc2  14977  vdwlem13  14991  0ram  15026  ram0  15028  ramz  15031  ramcl  15035  mulgnn0p1  16817  mulgnn0subcl  16819  mulgneg  16824  mulgnn0z  16826  mulgnn0dir  16829  mulgnn0ass  16835  submmulg  16841  odcl  17233  mndodcongi  17240  oddvdsnn0  17241  odnncl  17242  oddvds  17244  odclOLD  17249  dfod2  17263  odcl2  17264  gexcl  17279  gexdvds  17283  gexnnod  17288  sylow1lem1  17298  mulgnn0di  17514  torsubg  17540  ablfac1eu  17754  evlslem3  18785  gzrngunitlem  19080  zringlpirlem3OLD  19103  zringlpirlem3  19105  prmirredlem  19112  prmirred  19114  znf1o  19170  dscmet  21635  dvexp2  22956  tdeglem4  23057  dgrnznn  23249  coefv0  23250  dgreq0  23267  dgrcolem2  23276  dvply1  23285  aaliou2  23344  radcnv0  23419  logfac  23598  logtayl  23653  cxpexp  23661  leibpilem1  23914  birthdaylem2  23926  harmonicbnd3  23981  sqf11  24114  ppiltx  24152  sqff1o  24157  lgsdir  24306  lgsabs1  24310  lgseisenlem1  24325  2sqlem7  24346  2sqblem  24353  chebbnd1lem1  24355  gxnn0neg  26039  gxnn0suc  26040  znsqcld  28371  xrsmulgzz  28488  ressmulgnn0  28494  nexple  28879  eulerpartlemsv2  29239  eulerpartlemv  29245  eulerpartlemb  29249  eulerpartlemf  29251  eulerpartlemgvv  29257  eulerpartlemgh  29259  fz0n  30412  bccolsum  30423  nn0prpw  31027  fzsplit1nn0  35640  pell1qrgaplem  35763  monotoddzzfi  35834  jm2.22  35894  jm2.23  35895  rmydioph  35913  expdioph  35922  rp-isfinite6  36207  relexpss1d  36341  relexpmulg  36346  iunrelexpmin2  36348  relexp0a  36352  relexpxpmin  36353  relexpaddss  36354  wallispilem3  37966  etransclem24  38160  nn0o1gt2ALTV  38860  nn0oALTV  38862  ztprmneprm  40400  nn0enne  40598  nn0o1gt2  40599  blennn0elnn  40660  blen1b  40671  nn0sumshdiglem1  40704
  Copyright terms: Public domain W3C validator