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

Theorem elnn0 11279
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 11278 . . 3 0 = (ℕ ∪ {0})
21eleq2i 2691 . 2 (𝐴 ∈ ℕ0𝐴 ∈ (ℕ ∪ {0}))
3 elun 3745 . 2 (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4 c0ex 10019 . . . 4 0 ∈ V
54elsn2 4202 . . 3 (𝐴 ∈ {0} ↔ 𝐴 = 0)
65orbi2i 541 . 2 ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
72, 3, 63bitri 286 1 (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 383   = wceq 1481  wcel 1988  cun 3565  {csn 4168  0cc0 9921  cn 11005  0cn0 11277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-mulcl 9983  ax-i2m1 9989
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-un 3572  df-sn 4169  df-n0 11278
This theorem is referenced by:  0nn0  11292  nn0ge0  11303  nnnn0addcl  11308  nnm1nn0  11319  elnnnn0b  11322  nn0sub  11328  elnn0z  11375  elznn0nn  11376  elznn0  11377  elznn  11378  nn0lt10b  11424  nn0ind-raph  11462  nn0ledivnn  11926  expp1  12850  expneg  12851  expcllem  12854  facp1  13048  faclbnd  13060  faclbnd3  13062  faclbnd4lem1  13063  faclbnd4lem3  13065  faclbnd4  13067  bcn1  13083  bcval5  13088  hashv01gt1  13116  hashnncl  13140  seqcoll2  13232  relexpsucr  13750  relexpsucl  13754  relexpcnv  13756  relexprelg  13759  relexpdmg  13763  relexprng  13767  relexpfld  13770  relexpaddg  13774  fz1f1o  14422  arisum  14573  arisum2  14574  geomulcvg  14588  fprodfac  14684  ef0lem  14790  nn0enne  15075  nn0o1gt2  15078  bezoutlem3  15239  dfgcd2  15244  mulgcd  15246  eucalgf  15277  eucalginv  15278  eucalglt  15279  prmdvdsexpr  15410  rpexp1i  15414  nn0gcdsq  15441  odzdvds  15481  pceq0  15556  fldivp1  15582  pockthg  15591  1arith  15612  4sqlem17  15646  4sqlem19  15648  vdwmc2  15664  vdwlem13  15678  0ram  15705  ram0  15707  ramz  15710  ramcl  15714  mulgnn0p1  17533  mulgnn0subcl  17535  mulgneg  17541  mulgnn0z  17548  mulgnn0dir  17552  mulgnn0ass  17559  submmulg  17567  odcl  17936  mndodcongi  17943  oddvdsnn0  17944  odnncl  17945  oddvds  17947  dfod2  17962  odcl2  17963  gexcl  17976  gexdvds  17980  gexnnod  17984  sylow1lem1  17994  mulgnn0di  18212  torsubg  18238  ablfac1eu  18453  evlslem3  19495  gzrngunitlem  19792  zringlpirlem3  19815  prmirredlem  19822  prmirred  19824  znf1o  19881  dscmet  22358  dvexp2  23698  tdeglem4  23801  dgrnznn  23984  coefv0  23985  dgreq0  24002  dgrcolem2  24011  dvply1  24020  aaliou2  24076  radcnv0  24151  logfac  24328  logtayl  24387  cxpexp  24395  leibpilem1  24648  birthdaylem2  24660  harmonicbnd3  24715  sqf11  24846  ppiltx  24884  sqff1o  24889  lgsdir  25038  lgsabs1  25042  lgseisenlem1  25081  2sqlem7  25130  2sqblem  25137  chebbnd1lem1  25139  numclwwlkffin0  27187  znsqcld  29486  xrsmulgzz  29652  ressmulgnn0  29658  nexple  30045  eulerpartlemsv2  30394  eulerpartlemv  30400  eulerpartlemb  30404  eulerpartlemf  30406  eulerpartlemgvv  30412  eulerpartlemgh  30414  fz0n  31591  bccolsum  31600  nn0prpw  32293  fzsplit1nn0  37136  pell1qrgaplem  37256  monotoddzzfi  37326  jm2.22  37381  jm2.23  37382  rmydioph  37400  expdioph  37409  rp-isfinite6  37683  relexpss1d  37816  relexpmulg  37821  iunrelexpmin2  37823  relexp0a  37827  relexpxpmin  37828  relexpaddss  37829  wallispilem3  40047  etransclem24  40238  pwdif  41266  lighneallem3  41289  lighneallem4  41292  nn0o1gt2ALTV  41370  nn0oALTV  41372  ztprmneprm  41890  blennn0elnn  42136  blen1b  42147  nn0sumshdiglem1  42180
  Copyright terms: Public domain W3C validator