Theorem 0nn0 9528

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 2234	. 2 ⊢ 0 = 0
2		elnn0 9515	. . . 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 2205  0cc0 8143  ℕcn 9254  ℕ₀cn0 9513

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 2216  ax-1cn 8236  ax-icn 8238  ax-addcl 8239  ax-mulcl 8241  ax-i2m1 8248

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3700  df-n0 9514

This theorem is referenced by:  0xnn0  9586  elnn0z  9607  nn0ind-raph  9713  10nn0  9744  declei  9762  numlti  9763  nummul1c  9775  decaddc2  9782  decrmanc  9783  decrmac  9784  decaddm10  9785  decaddi  9786  decaddci  9787  decaddci2  9788  decmul1  9790  decmulnc  9793  6p5e11  9799  7p4e11  9802  8p3e11  9807  9p2e11  9813  10p10e20  9821  fz01or  10467  0elfz  10474  4fvwrd4  10496  fvinim0ffz  10609  0tonninf  10826  exple1  10981  sq10  11099  bc0k  11143  bcn1  11145  bccl  11154  fihasheq0  11181  hashfibc  11232  iswrdiz  11256  iswrddm0  11273  s1leng  11337  s1fv  11339  eqs1  11341  s111  11344  ccat2s1fstg  11361  pfx00g  11392  s2fv0g  11504  s3fv0g  11508  fsumnn0cl  12114  binom  12195  bcxmas  12200  isumnn0nn  12204  geoserap  12218  ef0lem  12371  ege2le3  12382  ef4p  12405  efgt1p2  12406  efgt1p  12407  nn0o  12618  ndvdssub  12641  5ndvds3  12645  bits0  12659  0bits  12670  gcdval  12680  gcdcl  12687  dfgcd3  12731  nn0seqcvgd  12763  algcvg  12770  eucalg  12781  lcmcl  12794  pw2dvdslemn  12887  pclem0  13009  pcpre1  13015  pcfac  13073  dec5dvds2  13136  2exp11  13159  2exp16  13160  ennnfonelemj0  13236  ennnfonelem0  13240  ennnfonelem1  13242  plendxnocndx  13511  slotsdifdsndx  13522  slotsdifunifndx  13529  imasvalstrd  13562  gfsum0  14104  cnfldstr  14832  nn0subm  14857  znf1o  14925  fczpsrbag  14946  psr1clfi  14969  mplsubgfilemm  14979  dveflem  15717  plyconst  15736  plycolemc  15749  pilem3  15774  clwwlkn0  16529  clwwlk0on0  16552  konigsberglem2  16610  konigsberglem3  16611  konigsberglem5  16613  konigsberg  16614  1kp2ke3k  16618  ex-fac  16622  depindlem1  16627  012of  16893  isomninnlem  16940  iswomninnlem  16960  iswomni0  16962  ismkvnnlem  16963