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

Theorem elnn0 11137
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 11136 . . 3 0 = (ℕ ∪ {0})
21eleq2i 2675 . 2 (𝐴 ∈ ℕ0𝐴 ∈ (ℕ ∪ {0}))
3 elun 3710 . 2 (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4 c0ex 9886 . . . 4 0 ∈ V
54elsn2 4153 . . 3 (𝐴 ∈ {0} ↔ 𝐴 = 0)
65orbi2i 539 . 2 ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
72, 3, 63bitri 284 1 (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wo 381   = wceq 1474  wcel 1975  cun 3533  {csn 4120  0cc0 9788  cn 10863  0cn0 11135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-mulcl 9850  ax-i2m1 9856
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-un 3540  df-sn 4121  df-n0 11136
This theorem is referenced by:  0nn0  11150  nn0ge0  11161  nnnn0addcl  11166  nnm1nn0  11177  elnnnn0b  11180  nn0sub  11186  elnn0z  11219  elznn0nn  11220  elznn0  11221  elznn  11222  nn0lt10b  11268  nn0ind-raph  11305  nn0ledivnn  11769  expp1  12680  expneg  12681  expcllem  12684  facp1  12878  faclbnd  12890  faclbnd3  12892  faclbnd4lem1  12893  faclbnd4lem3  12895  faclbnd4  12897  bcn1  12913  bcval5  12918  hashv01gt1  12943  hashnncl  12966  seqcoll2  13054  relexpsucr  13559  relexpsucl  13563  relexpcnv  13565  relexprelg  13568  relexpdmg  13572  relexprng  13576  relexpfld  13579  relexpaddg  13583  fz1f1o  14230  arisum  14373  arisum2  14374  geomulcvg  14388  fprodfac  14484  ef0lem  14590  nn0enne  14874  nn0o1gt2  14877  bezoutlem3  15038  dfgcd2  15043  mulgcd  15045  eucalgf  15076  eucalginv  15077  eucalglt  15078  prmdvdsexpr  15209  rpexp1i  15213  nn0gcdsq  15240  odzdvds  15280  pceq0  15355  fldivp1  15381  pockthg  15390  1arith  15411  4sqlem17  15445  4sqlem19  15447  vdwmc2  15463  vdwlem13  15477  0ram  15504  ram0  15506  ramz  15509  ramcl  15513  mulgnn0p1  17317  mulgnn0subcl  17319  mulgneg  17325  mulgnn0z  17332  mulgnn0dir  17336  mulgnn0ass  17343  submmulg  17351  odcl  17720  mndodcongi  17727  oddvdsnn0  17728  odnncl  17729  oddvds  17731  dfod2  17746  odcl2  17747  gexcl  17760  gexdvds  17764  gexnnod  17768  sylow1lem1  17778  mulgnn0di  17996  torsubg  18022  ablfac1eu  18237  evlslem3  19277  gzrngunitlem  19572  zringlpirlem3  19595  prmirredlem  19601  prmirred  19603  znf1o  19660  dscmet  22124  dvexp2  23436  tdeglem4  23537  dgrnznn  23720  coefv0  23721  dgreq0  23738  dgrcolem2  23747  dvply1  23756  aaliou2  23812  radcnv0  23887  logfac  24064  logtayl  24119  cxpexp  24127  leibpilem1  24380  birthdaylem2  24392  harmonicbnd3  24447  sqf11  24578  ppiltx  24616  sqff1o  24621  lgsdir  24770  lgsabs1  24774  lgseisenlem1  24813  2sqlem7  24862  2sqblem  24869  chebbnd1lem1  24871  znsqcld  28702  xrsmulgzz  28811  ressmulgnn0  28817  nexple  29201  eulerpartlemsv2  29549  eulerpartlemv  29555  eulerpartlemb  29559  eulerpartlemf  29561  eulerpartlemgvv  29567  eulerpartlemgh  29569  fz0n  30671  bccolsum  30680  nn0prpw  31290  fzsplit1nn0  36134  pell1qrgaplem  36254  monotoddzzfi  36324  jm2.22  36379  jm2.23  36380  rmydioph  36398  expdioph  36407  rp-isfinite6  36682  relexpss1d  36815  relexpmulg  36820  iunrelexpmin2  36822  relexp0a  36826  relexpxpmin  36827  relexpaddss  36828  wallispilem3  38760  etransclem24  38951  pwdif  39840  lighneallem3  39863  lighneallem4  39866  nn0o1gt2ALTV  39944  nn0oALTV  39946  av-numclwwlkffin0  41511  ztprmneprm  41916  blennn0elnn  42167  blen1b  42178  nn0sumshdiglem1  42211
  Copyright terms: Public domain W3C validator