Theorem 0nn0 9583

Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
0nn0	⊢ 0 ∈ ℕ0

Proof of Theorem 0nn0

Step	Hyp	Ref	Expression
1		eqid 2238	. 2 ⊢ 0 = 0
2		elnn0 9570	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 133	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 748	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

This proof depends on syntax axioms:   ∨ wo 720   = wceq 1402   ∈ wcel 2209  0cc0 8180  ℕcn 9307  ℕ₀cn0 9568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1cn 8273  ax-icn 8275  ax-addcl 8276  ax-mulcl 8278  ax-i2m1 8285

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-n0 9569

This theorem is used by:  0xnn0  9641  elnn0z  9662  nn0ind-raph  9768  10nn0  9803  declei  9822  numlti  9823  nummul1c  9835  decaddc2  9842  decrmanc  9843  decrmac  9844  decaddm10  9845  decaddi  9846  decaddci  9847  decaddci2  9848  decmul1  9850  decmulnc  9853  6p5e11  9859  7p4e11  9862  8p3e11  9867  9p2e11  9873  10p10e20  9881  fz01or  10529  0elfz  10536  4fvwrd4  10558  fvinim0ffz  10671  0tonninf  10892  exple1  11047  sq10  11166  bc0k  11210  bcn1  11212  bccl  11221  fihasheq0  11248  hashfibc  11299  iswrdiz  11327  iswrddm0  11344  s1leng  11408  s1fv  11410  eqs1  11412  s111  11415  ccat2s1fstg  11432  pfx00g  11463  s2fv0g  11575  s3fv0g  11579  fsumnn0cl  12189  binom  12270  bcxmas  12275  isumnn0nn  12279  geoserap  12293  ef0lem  12446  ege2le3  12457  ef4p  12480  efgt1p2  12481  efgt1p  12482  nn0o  12693  ndvdssub  12716  5ndvds3  12720  bits0  12734  0bits  12745  gcdval  12755  gcdcl  12762  dfgcd3  12806  nn0seqcvgd  12838  algcvg  12845  eucalg  12856  lcmcl  12869  pwbdvdslemn  12963  pclem0  13088  pcpre1  13094  pcfac  13152  dec5dvds2  13215  2exp11  13239  2exp16  13240  10nprm  13251  11prm  13252  37prm  13258  43prm  13259  83prm  13260  139prm  13261  163prm  13262  317prm  13263  631prm  13264  1259lem1  13265  1259lem2  13266  1259lem3  13267  1259lem4  13268  1259lem5  13269  ennnfonelemj0  13344  ennnfonelem0  13348  ennnfonelem1  13350  plendxnocndx  13621  slotsdifdsndx  13632  slotsdifunifndx  13639  imasvalstrd  13672  gsum0cmn  14238  cnfldstr  14979  nn0subm  15004  znf1o  15070  fczpsrbag  15140  psr1clfi  15170  mplsubgfilemm  15180  dveflem  15918  plyconst  15937  plycolemc  15950  pilem3  15976  log2ublem3  16184  log2ublog2  16185  ppiublem2  16253  chtublem  16256  bclbnd  16268  bposlem8  16279  clwwlkn0  16815  clwwlk0on0  16838  konigsberglem2  16896  konigsberglem3  16897  konigsberglem5  16899  konigsberg  16900  1kp2ke3k  16904  ex-fac  16908  depindlem1  16913  012of  17189  isomninnlem  17245  iswomninnlem  17266  iswomni0  17268  ismkvnnlem  17269