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

Theorem elnn0 12416
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 12415 . . 3 0 = (ℕ ∪ {0})
21eleq2i 2830 . 2 (𝐴 ∈ ℕ0𝐴 ∈ (ℕ ∪ {0}))
3 elun 4109 . 2 (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}))
4 c0ex 11150 . . . 4 0 ∈ V
54elsn2 4626 . . 3 (𝐴 ∈ {0} ↔ 𝐴 = 0)
65orbi2i 912 . 2 ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
72, 3, 63bitri 297 1 (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wo 846   = wceq 1542  wcel 2107  cun 3909  {csn 4587  0cc0 11052  cn 12154  0cn0 12414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-mulcl 11114  ax-i2m1 11120
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-un 3916  df-sn 4588  df-n0 12415
This theorem is referenced by:  0nn0  12429  nn0ge0  12439  nnnn0addcl  12444  nnm1nn0  12455  elnnnn0b  12458  nn0sub  12464  elnn0z  12513  elznn0nn  12514  elznn0  12515  elznn  12516  nn0lt10b  12566  nn0ind-raph  12604  nn0ledivnn  13029  expp1  13975  expneg  13976  expcllem  13979  znsqcld  14068  facp1  14179  faclbnd  14191  faclbnd3  14193  faclbnd4lem1  14194  faclbnd4lem3  14196  faclbnd4  14198  bcn1  14214  bcval5  14219  hashv01gt1  14246  hashnncl  14267  seqcoll2  14365  relexpsucl  14917  relexpsucr  14918  relexpcnv  14921  relexprelg  14924  relexpdmg  14928  relexprng  14932  relexpfld  14935  relexpaddg  14939  fz1f1o  15596  arisum  15746  arisum2  15747  pwdif  15754  geomulcvg  15762  fprodfac  15857  ef0lem  15962  nn0enne  16260  nn0o1gt2  16264  bezoutlem3  16423  dfgcd2  16428  mulgcd  16430  eucalgf  16460  eucalginv  16461  eucalglt  16462  prmdvdsexpr  16594  rpexp1i  16600  nn0gcdsq  16628  odzdvds  16668  pceq0  16744  fldivp1  16770  pockthg  16779  1arith  16800  4sqlem17  16834  4sqlem19  16836  vdwmc2  16852  vdwlem13  16866  0ram  16893  ram0  16895  ramz  16898  ramcl  16902  mulgnn0gsum  18883  mulgnn0p1  18888  mulgnn0subcl  18890  mulgneg  18895  mulgnn0z  18904  mulgnn0dir  18907  mulgnn0ass  18913  submmulg  18921  odcl  19319  mndodcongi  19326  oddvdsnn0  19327  odnncl  19328  oddvds  19330  dfod2  19347  odcl2  19348  gexcl  19363  gexdvds  19367  gexnnod  19371  sylow1lem1  19381  mulgnn0di  19605  torsubg  19633  ablfac1eu  19853  gzrngunitlem  20865  zringlpirlem3  20888  prmirredlem  20896  prmirred  20898  znf1o  20961  evlslem3  21493  dscmet  23931  dvexp2  25321  tdeglem4  25427  tdeglem4OLD  25428  dgrnznn  25611  coefv0  25612  dgreq0  25629  dgrcolem2  25638  dvply1  25647  aaliou2  25703  radcnv0  25778  logfac  25959  logtayl  26018  cxpexp  26026  birthdaylem2  26305  harmonicbnd3  26360  sqf11  26491  ppiltx  26529  sqff1o  26534  lgsdir  26683  lgsabs1  26687  lgseisenlem1  26726  2sqlem7  26775  2sqblem  26782  2sqnn  26790  chebbnd1lem1  26820  xrsmulgzz  31872  ressmulgnn0  31878  nexple  32611  eulerpartlemsv2  32961  eulerpartlemv  32967  eulerpartlemb  32971  eulerpartlemf  32973  eulerpartlemgvv  32979  eulerpartlemgh  32981  fz0n  34306  bccolsum  34315  nn0prpw  34798  aks4d1p1  40536  sticksstones13  40570  fsuppind  40768  negn0nposznnd  40799  nn0rppwr  40822  nn0expgcd  40824  dvdsexpnn0  40830  nn0addcom  40922  nn0mulcom  40926  zmulcomlem  40927  fzsplit1nn0  41080  pell1qrgaplem  41199  monotoddzzfi  41269  jm2.22  41322  jm2.23  41323  rmydioph  41341  expdioph  41350  rp-isfinite6  41797  relexpss1d  41984  relexpmulg  41989  iunrelexpmin2  41991  relexp0a  41995  relexpxpmin  41996  relexpaddss  41997  wallispilem3  44315  etransclem24  44506  lighneallem3  45806  lighneallem4  45809  nn0o1gt2ALTV  45893  nn0oALTV  45895  ztprmneprm  46430  blennn0elnn  46670  blen1b  46681  nn0sumshdiglem1  46714
  Copyright terms: Public domain W3C validator