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

Theorem elnn0 10786
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 10785 . . 3  |-  NN0  =  ( NN  u.  { 0 } )
21eleq2i 2538 . 2  |-  ( A  e.  NN0  <->  A  e.  ( NN  u.  { 0 } ) )
3 elun 3638 . 2  |-  ( A  e.  ( NN  u.  { 0 } )  <->  ( A  e.  NN  \/  A  e. 
{ 0 } ) )
4 c0ex 9579 . . . 4  |-  0  e.  _V
54elsnc2 4051 . . 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 1374    e. wcel 1762    u. cun 3467   {csn 4020   0cc0 9481   NNcn 10525   NN0cn0 10784
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-mulcl 9543  ax-i2m1 9549
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-un 3474  df-sn 4021  df-n0 10785
This theorem is referenced by:  0nn0  10799  nn0ge0  10810  nnnn0addcl  10815  nnm1nn0  10826  elnnnn0b  10829  nn0sub  10835  elnn0z  10866  elznn0nn  10867  elznn0  10868  elznn  10869  nn0ind-raph  10950  expp1  12129  expneg  12130  expcllem  12133  facp1  12313  faclbnd  12323  faclbnd3  12325  faclbnd4lem1  12326  faclbnd4lem3  12328  faclbnd4  12330  bcn1  12346  bcval5  12351  hashv01gt1  12373  hashnncl  12391  seqcoll2  12466  fz1f1o  13481  arisum  13623  arisum2  13624  geomulcvg  13637  ef0lem  13665  dvdseq  13881  bezoutlem3  14026  mulgcd  14032  eucalgf  14060  eucalginv  14061  eucalglt  14062  prmdvdsexpr  14105  rpexp1i  14110  nn0gcdsq  14133  odzdvds  14170  pceq0  14242  fldivp1  14264  pockthg  14272  1arith  14293  4sqlem17  14327  4sqlem19  14329  vdwmc2  14345  vdwlem13  14359  0ram  14386  ram0  14388  ramz  14391  ramcl  14395  mulgnn0p1  15946  mulgnn0subcl  15948  mulgneg  15953  mulgnn0z  15955  mulgnn0dir  15958  mulgnn0ass  15964  submmulg  15970  odcl  16349  mndodcongi  16356  oddvdsnn0  16357  odnncl  16358  oddvds  16360  dfod2  16375  odcl2  16376  gexcl  16389  gexdvds  16393  gexnnod  16397  sylow1lem1  16407  mulgnn0di  16623  torsubg  16646  ablfac1eu  16907  evlslem3  17947  gzrngunitlem  18243  zringlpirlem3  18271  zlpirlem3  18276  prmirredlem  18283  prmirred  18285  prmirredlemOLD  18286  prmirredOLD  18288  znf1o  18350  dscmet  20821  dvexp2  22085  tdeglem4  22186  coefv0  22372  dgreq0  22389  dgrcolem2  22398  dvply1  22407  aaliou2  22463  radcnv0  22538  logfac  22706  logtayl  22762  cxpexp  22770  leibpilem1  22992  birthdaylem2  23003  harmonicbnd3  23058  sqf11  23134  ppiltx  23172  sqff1o  23177  lgsdir  23326  lgsabs1  23330  lgseisenlem1  23345  2sqlem7  23366  2sqblem  23373  chebbnd1lem1  23375  gxnn0neg  24791  gxnn0suc  24792  xrsmulgzz  27178  ressmulgnn0  27184  nexple  27495  eulerpartlemsv2  27787  eulerpartlemv  27793  eulerpartlemb  27797  eulerpartlemf  27799  eulerpartlemgvv  27805  eulerpartlemgh  27807  fz0n  28435  fprodfac  28529  nn0prpw  29569  fzsplit1nn0  30142  pell1qrgaplem  30264  monotoddzzfi  30333  jm2.22  30394  jm2.23  30395  rmydioph  30413  expdioph  30422  dgrnznn  30542  wallispilem3  31186  ztprmneprm  31875
  Copyright terms: Public domain W3C validator