Theorem 0nn0 9416

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

Syntax hints:   ∨ wo 715   = wceq 1397   ∈ wcel 2202  0cc0 8031  ℕcn 9142  ℕ₀cn0 9401

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1cn 8124  ax-icn 8126  ax-addcl 8127  ax-mulcl 8129  ax-i2m1 8136

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-n0 9402

This theorem is referenced by:  0xnn0  9470  elnn0z  9491  nn0ind-raph  9596  10nn0  9627  declei  9645  numlti  9646  nummul1c  9658  decaddc2  9665  decrmanc  9666  decrmac  9667  decaddm10  9668  decaddi  9669  decaddci  9670  decaddci2  9671  decmul1  9673  decmulnc  9676  6p5e11  9682  7p4e11  9685  8p3e11  9690  9p2e11  9696  10p10e20  9704  fz01or  10345  0elfz  10352  4fvwrd4  10374  fvinim0ffz  10486  0tonninf  10701  exple1  10856  sq10  10973  bc0k  11017  bcn1  11019  bccl  11028  fihasheq0  11054  iswrdiz  11119  iswrddm0  11136  s1leng  11200  s1fv  11202  eqs1  11204  s111  11207  ccat2s1fstg  11224  pfx00g  11255  s2fv0g  11367  s3fv0g  11371  fsumnn0cl  11963  binom  12044  bcxmas  12049  isumnn0nn  12053  geoserap  12067  ef0lem  12220  ege2le3  12231  ef4p  12254  efgt1p2  12255  efgt1p  12256  nn0o  12467  ndvdssub  12490  5ndvds3  12494  bits0  12508  0bits  12519  gcdval  12529  gcdcl  12536  dfgcd3  12580  nn0seqcvgd  12612  algcvg  12619  eucalg  12630  lcmcl  12643  pw2dvdslemn  12736  pclem0  12858  pcpre1  12864  pcfac  12922  dec5dvds2  12985  2exp11  13008  2exp16  13009  ennnfonelemj0  13021  ennnfonelem0  13025  ennnfonelem1  13027  plendxnocndx  13296  slotsdifdsndx  13307  slotsdifunifndx  13314  imasvalstrd  13352  cnfldstr  14571  nn0subm  14596  znf1o  14664  fczpsrbag  14684  psr1clfi  14701  mplsubgfilemm  14711  dveflem  15449  plyconst  15468  plycolemc  15481  pilem3  15506  clwwlkn0  16258  clwwlk0on0  16281  1kp2ke3k  16320  ex-fac  16324  012of  16592  isomninnlem  16634  iswomninnlem  16653  iswomni0  16655  ismkvnnlem  16656  gfsum0  16682