Theorem 0nn0 9187

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

Syntax hints:   ∨ wo 708   = wceq 1353   ∈ wcel 2148  0cc0 7808  ℕcn 8915  ℕ₀cn0 9172

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1cn 7901  ax-icn 7903  ax-addcl 7904  ax-mulcl 7906  ax-i2m1 7913

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-n0 9173

This theorem is referenced by:  0xnn0  9241  elnn0z  9262  nn0ind-raph  9366  10nn0  9397  declei  9415  numlti  9416  nummul1c  9428  decaddc2  9435  decrmanc  9436  decrmac  9437  decaddm10  9438  decaddi  9439  decaddci  9440  decaddci2  9441  decmul1  9443  decmulnc  9446  6p5e11  9452  7p4e11  9455  8p3e11  9460  9p2e11  9466  10p10e20  9474  fz01or  10106  0elfz  10113  4fvwrd4  10135  fvinim0ffz  10236  0tonninf  10434  exple1  10571  sq10  10685  bc0k  10729  bcn1  10731  bccl  10740  fihasheq0  10766  fsumnn0cl  11404  binom  11485  bcxmas  11490  isumnn0nn  11494  geoserap  11508  ef0lem  11661  ege2le3  11672  ef4p  11695  efgt1p2  11696  efgt1p  11697  nn0o  11904  ndvdssub  11927  gcdval  11952  gcdcl  11959  dfgcd3  12003  nn0seqcvgd  12033  algcvg  12040  eucalg  12051  lcmcl  12064  pw2dvdslemn  12157  pclem0  12278  pcpre1  12284  pcfac  12340  ennnfonelemj0  12394  ennnfonelem0  12398  ennnfonelem1  12400  slotsdifdsndx  12668  slotsdifunifndx  12675  nn0subm  13346  dveflem  14058  pilem3  14075  1kp2ke3k  14336  ex-fac  14340  012of  14605  isomninnlem  14638  iswomninnlem  14657  iswomni0  14659  ismkvnnlem  14660