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

Theorem elnn0 12349
Description: Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-2002.)
Assertion
Ref Expression
elnn0 (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))

Proof of Theorem elnn0
StepHypRef Expression
1 df-n0 12348 . . 3 0 = (ℕ ∪ {0})
21eleq2i 2830 . 2 (𝐴 ∈ ℕ0𝐴 ∈ (ℕ ∪ {0}))
3 elun 4107 . 2 (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4 c0ex 11083 . . . 4 0 ∈ V
54elsn2 4624 . . 3 (𝐴 ∈ {0} ↔ 𝐴 = 0)
65orbi2i 912 . 2 ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
72, 3, 63bitri 297 1 (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wo 846   = wceq 1542  wcel 2107  cun 3907  {csn 4585  0cc0 10985  cn 12087  0cn0 12347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-mulcl 11047  ax-i2m1 11053
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3446  df-un 3914  df-sn 4586  df-n0 12348
This theorem is referenced by:  0nn0  12362  nn0ge0  12372  nnnn0addcl  12377  nnm1nn0  12388  elnnnn0b  12391  nn0sub  12397  elnn0z  12446  elznn0nn  12447  elznn0  12448  elznn  12449  nn0lt10b  12499  nn0ind-raph  12537  nn0ledivnn  12958  expp1  13904  expneg  13905  expcllem  13908  znsqcld  13995  facp1  14107  faclbnd  14119  faclbnd3  14121  faclbnd4lem1  14122  faclbnd4lem3  14124  faclbnd4  14126  bcn1  14142  bcval5  14147  hashv01gt1  14174  hashnncl  14195  seqcoll2  14293  relexpsucl  14851  relexpsucr  14852  relexpcnv  14855  relexprelg  14858  relexpdmg  14862  relexprng  14866  relexpfld  14869  relexpaddg  14873  fz1f1o  15531  arisum  15681  arisum2  15682  pwdif  15689  geomulcvg  15697  fprodfac  15792  ef0lem  15897  nn0enne  16195  nn0o1gt2  16199  bezoutlem3  16358  dfgcd2  16363  mulgcd  16365  eucalgf  16395  eucalginv  16396  eucalglt  16397  prmdvdsexpr  16529  rpexp1i  16535  nn0gcdsq  16563  odzdvds  16603  pceq0  16679  fldivp1  16705  pockthg  16714  1arith  16735  4sqlem17  16769  4sqlem19  16771  vdwmc2  16787  vdwlem13  16801  0ram  16828  ram0  16830  ramz  16833  ramcl  16837  mulgnn0gsum  18817  mulgnn0p1  18822  mulgnn0subcl  18824  mulgneg  18829  mulgnn0z  18838  mulgnn0dir  18841  mulgnn0ass  18847  submmulg  18855  odcl  19253  mndodcongi  19260  oddvdsnn0  19261  odnncl  19262  oddvds  19264  dfod2  19281  odcl2  19282  gexcl  19297  gexdvds  19301  gexnnod  19305  sylow1lem1  19315  mulgnn0di  19539  torsubg  19567  ablfac1eu  19787  gzrngunitlem  20791  zringlpirlem3  20814  prmirredlem  20822  prmirred  20824  znf1o  20887  evlslem3  21418  dscmet  23856  dvexp2  25246  tdeglem4  25352  tdeglem4OLD  25353  dgrnznn  25536  coefv0  25537  dgreq0  25554  dgrcolem2  25563  dvply1  25572  aaliou2  25628  radcnv0  25703  logfac  25884  logtayl  25943  cxpexp  25951  birthdaylem2  26230  harmonicbnd3  26285  sqf11  26416  ppiltx  26454  sqff1o  26459  lgsdir  26608  lgsabs1  26612  lgseisenlem1  26651  2sqlem7  26700  2sqblem  26707  2sqnn  26715  chebbnd1lem1  26745  xrsmulgzz  31670  ressmulgnn0  31676  nexple  32388  eulerpartlemsv2  32738  eulerpartlemv  32744  eulerpartlemb  32748  eulerpartlemf  32750  eulerpartlemgvv  32756  eulerpartlemgh  32758  fz0n  34097  bccolsum  34106  nn0prpw  34726  aks4d1p1  40464  sticksstones13  40498  fsuppind  40667  negn0nposznnd  40698  nn0rppwr  40721  nn0expgcd  40723  dvdsexpnn0  40729  nn0addcom  40821  nn0mulcom  40825  zmulcomlem  40826  fzsplit1nn0  40979  pell1qrgaplem  41098  monotoddzzfi  41168  jm2.22  41221  jm2.23  41222  rmydioph  41240  expdioph  41249  rp-isfinite6  41589  relexpss1d  41776  relexpmulg  41781  iunrelexpmin2  41783  relexp0a  41787  relexpxpmin  41788  relexpaddss  41789  wallispilem3  44099  etransclem24  44290  lighneallem3  45590  lighneallem4  45593  nn0o1gt2ALTV  45677  nn0oALTV  45679  ztprmneprm  46214  blennn0elnn  46454  blen1b  46465  nn0sumshdiglem1  46498
  Copyright terms: Public domain W3C validator