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

Theorem elnn0 10573
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 10572 . . 3  |-  NN0  =  ( NN  u.  { 0 } )
21eleq2i 2502 . 2  |-  ( A  e.  NN0  <->  A  e.  ( NN  u.  { 0 } ) )
3 elun 3492 . 2  |-  ( A  e.  ( NN  u.  { 0 } )  <->  ( A  e.  NN  \/  A  e. 
{ 0 } ) )
4 c0ex 9372 . . . 4  |-  0  e.  _V
54elsnc2 3903 . . 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 1369    e. wcel 1756    u. cun 3321   {csn 3872   0cc0 9274   NNcn 10314   NN0cn0 10571
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-mulcl 9336  ax-i2m1 9342
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-un 3328  df-sn 3873  df-n0 10572
This theorem is referenced by:  0nn0  10586  nn0ge0  10597  nnnn0addcl  10602  nnm1nn0  10613  elnnnn0b  10616  nn0sub  10622  elnn0z  10651  elznn0nn  10652  elznn0  10653  elznn  10654  nn0ind-raph  10734  expp1  11864  expneg  11865  expcllem  11868  facp1  12048  faclbnd  12058  faclbnd3  12060  faclbnd4lem1  12061  faclbnd4lem3  12063  faclbnd4  12065  bcn1  12081  bcval5  12086  hashv01gt1  12108  hashnncl  12126  seqcoll2  12209  fz1f1o  13179  arisum  13314  arisum2  13315  geomulcvg  13328  ef0lem  13356  dvdseq  13572  bezoutlem3  13716  mulgcd  13722  eucalgf  13750  eucalginv  13751  eucalglt  13752  prmdvdsexpr  13794  rpexp1i  13799  nn0gcdsq  13822  odzdvds  13859  pceq0  13929  fldivp1  13951  pockthg  13959  1arith  13980  4sqlem17  14014  4sqlem19  14016  vdwmc2  14032  vdwlem13  14046  0ram  14073  ram0  14075  ramz  14078  ramcl  14082  mulgnn0p1  15629  mulgnn0subcl  15631  mulgneg  15636  mulgnn0z  15638  mulgnn0dir  15641  mulgnn0ass  15647  submmulg  15653  odcl  16030  mndodcongi  16037  oddvdsnn0  16038  odnncl  16039  oddvds  16041  dfod2  16056  odcl2  16057  gexcl  16070  gexdvds  16074  gexnnod  16078  sylow1lem1  16088  mulgnn0di  16304  torsubg  16327  ablfac1eu  16564  evlslem3  17580  gzrngunitlem  17857  zringlpirlem3  17885  zlpirlem3  17890  prmirredlem  17897  prmirred  17899  prmirredlemOLD  17900  prmirredOLD  17902  znf1o  17964  dscmet  20145  dvexp2  21408  tdeglem4  21509  coefv0  21695  dgreq0  21712  dgrcolem2  21721  dvply1  21730  aaliou2  21786  radcnv0  21861  logfac  22029  logtayl  22085  cxpexp  22093  leibpilem1  22315  birthdaylem2  22326  harmonicbnd3  22381  sqf11  22457  ppiltx  22495  sqff1o  22500  lgsdir  22649  lgsabs1  22653  lgseisenlem1  22668  2sqlem7  22689  2sqblem  22696  chebbnd1lem1  22698  gxnn0neg  23718  gxnn0suc  23719  xrsmulgzz  26107  ressmulgnn0  26113  nexple  26417  eulerpartlemsv2  26710  eulerpartlemv  26716  eulerpartlemb  26720  eulerpartlemf  26722  eulerpartlemgvv  26728  eulerpartlemgh  26730  fz0n  27358  fprodfac  27452  nn0prpw  28489  fzsplit1nn0  29063  pell1qrgaplem  29185  monotoddzzfi  29254  jm2.22  29315  jm2.23  29316  rmydioph  29334  expdioph  29343  dgrnznn  29463  wallispilem3  29833  ztprmneprm  30709
  Copyright terms: Public domain W3C validator