Theorem 0nn0 9105

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 2157	. 2 ⊢ 0 = 0
2		elnn0 9092	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 132	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 726	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

Syntax hints:   ∨ wo 698   = wceq 1335   ∈ wcel 2128  0cc0 7732  ℕcn 8833  ℕ₀cn0 9090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139  ax-1cn 7825  ax-icn 7827  ax-addcl 7828  ax-mulcl 7830  ax-i2m1 7837

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-v 2714  df-un 3106  df-sn 3566  df-n0 9091

This theorem is referenced by:  0xnn0  9159  elnn0z  9180  nn0ind-raph  9281  10nn0  9312  declei  9330  numlti  9331  nummul1c  9343  decaddc2  9350  decrmanc  9351  decrmac  9352  decaddm10  9353  decaddi  9354  decaddci  9355  decaddci2  9356  decmul1  9358  decmulnc  9361  6p5e11  9367  7p4e11  9370  8p3e11  9375  9p2e11  9381  10p10e20  9389  fz01or  10013  0elfz  10020  4fvwrd4  10039  fvinim0ffz  10140  0tonninf  10338  exple1  10475  sq10  10586  bc0k  10630  bcn1  10632  bccl  10641  fihasheq0  10668  fsumnn0cl  11300  binom  11381  bcxmas  11386  isumnn0nn  11390  geoserap  11404  ef0lem  11557  ege2le3  11568  ef4p  11591  efgt1p2  11592  efgt1p  11593  nn0o  11798  ndvdssub  11821  gcdval  11843  gcdcl  11850  dfgcd3  11894  nn0seqcvgd  11918  algcvg  11925  eucalg  11936  lcmcl  11949  pw2dvdslemn  12040  ennnfonelemj0  12141  ennnfonelem0  12145  ennnfonelem1  12147  dveflem  13098  pilem3  13115  1kp2ke3k  13311  ex-fac  13315  012of  13578  isomninnlem  13612  iswomninnlem  13631  iswomni0  13633  ismkvnnlem  13634