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

Theorem elnn0 11171
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 11170 . . 3 0 = (ℕ ∪ {0})
21eleq2i 2680 . 2 (𝐴 ∈ ℕ0𝐴 ∈ (ℕ ∪ {0}))
3 elun 3715 . 2 (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4 c0ex 9913 . . . 4 0 ∈ V
54elsn2 4158 . . 3 (𝐴 ∈ {0} ↔ 𝐴 = 0)
65orbi2i 540 . 2 ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
72, 3, 63bitri 285 1 (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wo 382   = wceq 1475  wcel 1977  cun 3538  {csn 4125  0cc0 9815  cn 10897  0cn0 11169
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-mulcl 9877  ax-i2m1 9883
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-sn 4126  df-n0 11170
This theorem is referenced by:  0nn0  11184  nn0ge0  11195  nnnn0addcl  11200  nnm1nn0  11211  elnnnn0b  11214  nn0sub  11220  elnn0z  11267  elznn0nn  11268  elznn0  11269  elznn  11270  nn0lt10b  11316  nn0ind-raph  11353  nn0ledivnn  11817  expp1  12729  expneg  12730  expcllem  12733  facp1  12927  faclbnd  12939  faclbnd3  12941  faclbnd4lem1  12942  faclbnd4lem3  12944  faclbnd4  12946  bcn1  12962  bcval5  12967  hashv01gt1  12995  hashnncl  13018  seqcoll2  13106  relexpsucr  13617  relexpsucl  13621  relexpcnv  13623  relexprelg  13626  relexpdmg  13630  relexprng  13634  relexpfld  13637  relexpaddg  13641  fz1f1o  14288  arisum  14431  arisum2  14432  geomulcvg  14446  fprodfac  14542  ef0lem  14648  nn0enne  14932  nn0o1gt2  14935  bezoutlem3  15096  dfgcd2  15101  mulgcd  15103  eucalgf  15134  eucalginv  15135  eucalglt  15136  prmdvdsexpr  15267  rpexp1i  15271  nn0gcdsq  15298  odzdvds  15338  pceq0  15413  fldivp1  15439  pockthg  15448  1arith  15469  4sqlem17  15503  4sqlem19  15505  vdwmc2  15521  vdwlem13  15535  0ram  15562  ram0  15564  ramz  15567  ramcl  15571  mulgnn0p1  17375  mulgnn0subcl  17377  mulgneg  17383  mulgnn0z  17390  mulgnn0dir  17394  mulgnn0ass  17401  submmulg  17409  odcl  17778  mndodcongi  17785  oddvdsnn0  17786  odnncl  17787  oddvds  17789  dfod2  17804  odcl2  17805  gexcl  17818  gexdvds  17822  gexnnod  17826  sylow1lem1  17836  mulgnn0di  18054  torsubg  18080  ablfac1eu  18295  evlslem3  19335  gzrngunitlem  19630  zringlpirlem3  19653  prmirredlem  19660  prmirred  19662  znf1o  19719  dscmet  22187  dvexp2  23523  tdeglem4  23624  dgrnznn  23807  coefv0  23808  dgreq0  23825  dgrcolem2  23834  dvply1  23843  aaliou2  23899  radcnv0  23974  logfac  24151  logtayl  24206  cxpexp  24214  leibpilem1  24467  birthdaylem2  24479  harmonicbnd3  24534  sqf11  24665  ppiltx  24703  sqff1o  24708  lgsdir  24857  lgsabs1  24861  lgseisenlem1  24900  2sqlem7  24949  2sqblem  24956  chebbnd1lem1  24958  znsqcld  28900  xrsmulgzz  29009  ressmulgnn0  29015  nexple  29399  eulerpartlemsv2  29747  eulerpartlemv  29753  eulerpartlemb  29757  eulerpartlemf  29759  eulerpartlemgvv  29765  eulerpartlemgh  29767  fz0n  30869  bccolsum  30878  nn0prpw  31488  fzsplit1nn0  36335  pell1qrgaplem  36455  monotoddzzfi  36525  jm2.22  36580  jm2.23  36581  rmydioph  36599  expdioph  36608  rp-isfinite6  36883  relexpss1d  37016  relexpmulg  37021  iunrelexpmin2  37023  relexp0a  37027  relexpxpmin  37028  relexpaddss  37029  wallispilem3  38960  etransclem24  39151  pwdif  40039  lighneallem3  40062  lighneallem4  40065  nn0o1gt2ALTV  40143  nn0oALTV  40145  av-numclwwlkffin0  41513  ztprmneprm  41918  blennn0elnn  42169  blen1b  42180  nn0sumshdiglem1  42213
  Copyright terms: Public domain W3C validator