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

Theorem elnn0 11891
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 11890 . . 3 0 = (ℕ ∪ {0})
21eleq2i 2908 . 2 (𝐴 ∈ ℕ0𝐴 ∈ (ℕ ∪ {0}))
3 elun 4128 . 2 (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4 c0ex 10627 . . . 4 0 ∈ V
54elsn2 4600 . . 3 (𝐴 ∈ {0} ↔ 𝐴 = 0)
65orbi2i 908 . 2 ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
72, 3, 63bitri 298 1 (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wo 843   = wceq 1530  wcel 2107  cun 3937  {csn 4563  0cc0 10529  cn 11630  0cn0 11889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-mulcl 10591  ax-i2m1 10597
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-v 3501  df-un 3944  df-sn 4564  df-n0 11890
This theorem is referenced by:  0nn0  11904  nn0ge0  11914  nnnn0addcl  11919  nnm1nn0  11930  elnnnn0b  11933  nn0sub  11939  elnn0z  11986  elznn0nn  11987  elznn0  11988  elznn  11989  nn0lt10b  12036  nn0ind-raph  12074  nn0ledivnn  12495  expp1  13429  expneg  13430  expcllem  13433  znsqcld  13519  facp1  13631  faclbnd  13643  faclbnd3  13645  faclbnd4lem1  13646  faclbnd4lem3  13648  faclbnd4  13650  bcn1  13666  bcval5  13671  hashv01gt1  13698  hashnncl  13720  seqcoll2  13816  relexpsucr  14381  relexpsucl  14385  relexpcnv  14387  relexprelg  14390  relexpdmg  14394  relexprng  14398  relexpfld  14401  relexpaddg  14405  fz1f1o  15059  arisum  15207  arisum2  15208  pwdif  15215  geomulcvg  15224  fprodfac  15319  ef0lem  15424  nn0enne  15720  nn0o1gt2  15724  bezoutlem3  15881  dfgcd2  15886  mulgcd  15888  eucalgf  15919  eucalginv  15920  eucalglt  15921  prmdvdsexpr  16053  rpexp1i  16057  nn0gcdsq  16084  odzdvds  16124  pceq0  16199  fldivp1  16225  pockthg  16234  1arith  16255  4sqlem17  16289  4sqlem19  16291  vdwmc2  16307  vdwlem13  16321  0ram  16348  ram0  16350  ramz  16353  ramcl  16357  mulgnn0gsum  18166  mulgnn0p1  18171  mulgnn0subcl  18173  mulgneg  18178  mulgnn0z  18186  mulgnn0dir  18189  mulgnn0ass  18195  submmulg  18203  odcl  18586  mndodcongi  18593  oddvdsnn0  18594  odnncl  18595  oddvds  18597  dfod2  18613  odcl2  18614  gexcl  18627  gexdvds  18631  gexnnod  18635  sylow1lem1  18645  mulgnn0di  18868  torsubg  18896  ablfac1eu  19117  evlslem3  20213  gzrngunitlem  20526  zringlpirlem3  20549  prmirredlem  20556  prmirred  20558  znf1o  20614  dscmet  23097  dvexp2  24466  tdeglem4  24569  dgrnznn  24752  coefv0  24753  dgreq0  24770  dgrcolem2  24779  dvply1  24788  aaliou2  24844  radcnv0  24919  logfac  25097  logtayl  25156  cxpexp  25164  leibpilem1OLD  25432  birthdaylem2  25444  harmonicbnd3  25499  sqf11  25630  ppiltx  25668  sqff1o  25673  lgsdir  25822  lgsabs1  25826  lgseisenlem1  25865  2sqlem7  25914  2sqblem  25921  2sqnn  25929  chebbnd1lem1  25959  xrsmulgzz  30579  ressmulgnn0  30585  nexple  31154  eulerpartlemsv2  31502  eulerpartlemv  31508  eulerpartlemb  31512  eulerpartlemf  31514  eulerpartlemgvv  31520  eulerpartlemgh  31522  fz0n  32846  bccolsum  32855  nn0prpw  33555  negn0nposznnd  39031  nn0rppwr  39045  nn0expgcd  39047  fzsplit1nn0  39212  pell1qrgaplem  39331  monotoddzzfi  39400  jm2.22  39453  jm2.23  39454  rmydioph  39472  expdioph  39481  rp-isfinite6  39745  relexpss1d  39911  relexpmulg  39916  iunrelexpmin2  39918  relexp0a  39922  relexpxpmin  39923  relexpaddss  39924  wallispilem3  42214  etransclem24  42405  lighneallem3  43600  lighneallem4  43603  nn0o1gt2ALTV  43687  nn0oALTV  43689  ztprmneprm  44223  blennn0elnn  44465  blen1b  44476  nn0sumshdiglem1  44509
  Copyright terms: Public domain W3C validator