Theorem 0nn0 9395

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 2229	. 2 ⊢ 0 = 0
2		elnn0 9382	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 133	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 741	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

Syntax hints:   ∨ wo 713   = wceq 1395   ∈ wcel 2200  0cc0 8010  ℕcn 9121  ℕ₀cn0 9380

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1cn 8103  ax-icn 8105  ax-addcl 8106  ax-mulcl 8108  ax-i2m1 8115

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-n0 9381

This theorem is referenced by:  0xnn0  9449  elnn0z  9470  nn0ind-raph  9575  10nn0  9606  declei  9624  numlti  9625  nummul1c  9637  decaddc2  9644  decrmanc  9645  decrmac  9646  decaddm10  9647  decaddi  9648  decaddci  9649  decaddci2  9650  decmul1  9652  decmulnc  9655  6p5e11  9661  7p4e11  9664  8p3e11  9669  9p2e11  9675  10p10e20  9683  fz01or  10319  0elfz  10326  4fvwrd4  10348  fvinim0ffz  10459  0tonninf  10674  exple1  10829  sq10  10946  bc0k  10990  bcn1  10992  bccl  11001  fihasheq0  11027  iswrdiz  11091  iswrddm0  11108  s1leng  11172  s1fv  11174  eqs1  11176  s111  11179  pfx00g  11222  s2fv0g  11334  s3fv0g  11338  fsumnn0cl  11929  binom  12010  bcxmas  12015  isumnn0nn  12019  geoserap  12033  ef0lem  12186  ege2le3  12197  ef4p  12220  efgt1p2  12221  efgt1p  12222  nn0o  12433  ndvdssub  12456  5ndvds3  12460  bits0  12474  0bits  12485  gcdval  12495  gcdcl  12502  dfgcd3  12546  nn0seqcvgd  12578  algcvg  12585  eucalg  12596  lcmcl  12609  pw2dvdslemn  12702  pclem0  12824  pcpre1  12830  pcfac  12888  dec5dvds2  12951  2exp11  12974  2exp16  12975  ennnfonelemj0  12987  ennnfonelem0  12991  ennnfonelem1  12993  plendxnocndx  13262  slotsdifdsndx  13273  slotsdifunifndx  13280  imasvalstrd  13318  cnfldstr  14537  nn0subm  14562  znf1o  14630  fczpsrbag  14650  psr1clfi  14667  mplsubgfilemm  14677  dveflem  15415  plyconst  15434  plycolemc  15447  pilem3  15472  1kp2ke3k  16143  ex-fac  16147  012of  16416  isomninnlem  16458  iswomninnlem  16477  iswomni0  16479  ismkvnnlem  16480