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

Theorem elnn0 11332
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 11331 . . 3 0 = (ℕ ∪ {0})
21eleq2i 2722 . 2 (𝐴 ∈ ℕ0𝐴 ∈ (ℕ ∪ {0}))
3 elun 3786 . 2 (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4 c0ex 10072 . . . 4 0 ∈ V
54elsn2 4244 . . 3 (𝐴 ∈ {0} ↔ 𝐴 = 0)
65orbi2i 540 . 2 ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
72, 3, 63bitri 286 1 (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 382   = wceq 1523  wcel 2030  cun 3605  {csn 4210  0cc0 9974  cn 11058  0cn0 11330
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-mulcl 10036  ax-i2m1 10042
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-sn 4211  df-n0 11331
This theorem is referenced by:  0nn0  11345  nn0ge0  11356  nnnn0addcl  11361  nnm1nn0  11372  elnnnn0b  11375  nn0sub  11381  elnn0z  11428  elznn0nn  11429  elznn0  11430  elznn  11431  nn0lt10b  11477  nn0ind-raph  11515  nn0ledivnn  11979  expp1  12907  expneg  12908  expcllem  12911  facp1  13105  faclbnd  13117  faclbnd3  13119  faclbnd4lem1  13120  faclbnd4lem3  13122  faclbnd4  13124  bcn1  13140  bcval5  13145  hashv01gt1  13173  hashnncl  13195  seqcoll2  13287  relexpsucr  13813  relexpsucl  13817  relexpcnv  13819  relexprelg  13822  relexpdmg  13826  relexprng  13830  relexpfld  13833  relexpaddg  13837  fz1f1o  14485  arisum  14636  arisum2  14637  geomulcvg  14651  fprodfac  14747  ef0lem  14853  nn0enne  15141  nn0o1gt2  15144  bezoutlem3  15305  dfgcd2  15310  mulgcd  15312  eucalgf  15343  eucalginv  15344  eucalglt  15345  prmdvdsexpr  15476  rpexp1i  15480  nn0gcdsq  15507  odzdvds  15547  pceq0  15622  fldivp1  15648  pockthg  15657  1arith  15678  4sqlem17  15712  4sqlem19  15714  vdwmc2  15730  vdwlem13  15744  0ram  15771  ram0  15773  ramz  15776  ramcl  15780  mulgnn0p1  17599  mulgnn0subcl  17601  mulgneg  17607  mulgnn0z  17614  mulgnn0dir  17618  mulgnn0ass  17625  submmulg  17633  odcl  18001  mndodcongi  18008  oddvdsnn0  18009  odnncl  18010  oddvds  18012  dfod2  18027  odcl2  18028  gexcl  18041  gexdvds  18045  gexnnod  18049  sylow1lem1  18059  mulgnn0di  18277  torsubg  18303  ablfac1eu  18518  evlslem3  19562  gzrngunitlem  19859  zringlpirlem3  19882  prmirredlem  19889  prmirred  19891  znf1o  19948  dscmet  22424  dvexp2  23762  tdeglem4  23865  dgrnznn  24048  coefv0  24049  dgreq0  24066  dgrcolem2  24075  dvply1  24084  aaliou2  24140  radcnv0  24215  logfac  24392  logtayl  24451  cxpexp  24459  leibpilem1  24712  birthdaylem2  24724  harmonicbnd3  24779  sqf11  24910  ppiltx  24948  sqff1o  24953  lgsdir  25102  lgsabs1  25106  lgseisenlem1  25145  2sqlem7  25194  2sqblem  25201  chebbnd1lem1  25203  znsqcld  29640  xrsmulgzz  29806  ressmulgnn0  29812  nexple  30199  eulerpartlemsv2  30548  eulerpartlemv  30554  eulerpartlemb  30558  eulerpartlemf  30560  eulerpartlemgvv  30566  eulerpartlemgh  30568  fz0n  31742  bccolsum  31751  nn0prpw  32443  fzsplit1nn0  37634  pell1qrgaplem  37754  monotoddzzfi  37824  jm2.22  37879  jm2.23  37880  rmydioph  37898  expdioph  37907  rp-isfinite6  38181  relexpss1d  38314  relexpmulg  38319  iunrelexpmin2  38321  relexp0a  38325  relexpxpmin  38326  relexpaddss  38327  wallispilem3  40602  etransclem24  40793  pwdif  41826  lighneallem3  41849  lighneallem4  41852  nn0o1gt2ALTV  41930  nn0oALTV  41932  ztprmneprm  42450  blennn0elnn  42696  blen1b  42707  nn0sumshdiglem1  42740
  Copyright terms: Public domain W3C validator