Theorem 0nn0 9511

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

Syntax hints:   ∨ wo 716   = wceq 1398   ∈ wcel 2203  0cc0 8127  ℕcn 9237  ℕ₀cn0 9496

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-1cn 8220  ax-icn 8222  ax-addcl 8223  ax-mulcl 8225  ax-i2m1 8232

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-sn 3695  df-n0 9497

This theorem is referenced by:  0xnn0  9569  elnn0z  9590  nn0ind-raph  9695  10nn0  9726  declei  9744  numlti  9745  nummul1c  9757  decaddc2  9764  decrmanc  9765  decrmac  9766  decaddm10  9767  decaddi  9768  decaddci  9769  decaddci2  9770  decmul1  9772  decmulnc  9775  6p5e11  9781  7p4e11  9784  8p3e11  9789  9p2e11  9795  10p10e20  9803  fz01or  10445  0elfz  10452  4fvwrd4  10474  fvinim0ffz  10587  0tonninf  10802  exple1  10957  sq10  11074  bc0k  11118  bcn1  11120  bccl  11129  fihasheq0  11156  hashfibc  11207  iswrdiz  11231  iswrddm0  11248  s1leng  11312  s1fv  11314  eqs1  11316  s111  11319  ccat2s1fstg  11336  pfx00g  11367  s2fv0g  11479  s3fv0g  11483  fsumnn0cl  12089  binom  12170  bcxmas  12175  isumnn0nn  12179  geoserap  12193  ef0lem  12346  ege2le3  12357  ef4p  12380  efgt1p2  12381  efgt1p  12382  nn0o  12593  ndvdssub  12616  5ndvds3  12620  bits0  12634  0bits  12645  gcdval  12655  gcdcl  12662  dfgcd3  12706  nn0seqcvgd  12738  algcvg  12745  eucalg  12756  lcmcl  12769  pw2dvdslemn  12862  pclem0  12984  pcpre1  12990  pcfac  13048  dec5dvds2  13111  2exp11  13134  2exp16  13135  ennnfonelemj0  13152  ennnfonelem0  13156  ennnfonelem1  13158  plendxnocndx  13427  slotsdifdsndx  13438  slotsdifunifndx  13445  imasvalstrd  13483  cnfldstr  14706  nn0subm  14731  znf1o  14799  fczpsrbag  14820  psr1clfi  14843  mplsubgfilemm  14853  dveflem  15591  plyconst  15610  plycolemc  15623  pilem3  15648  clwwlkn0  16403  clwwlk0on0  16426  konigsberglem2  16484  konigsberglem3  16485  konigsberglem5  16487  konigsberg  16488  1kp2ke3k  16492  ex-fac  16496  depindlem1  16501  012of  16767  isomninnlem  16814  iswomninnlem  16834  iswomni0  16836  ismkvnnlem  16837  gfsum0  16864