Theorem 0nn0 9309

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

Syntax hints:   ∨ wo 709   = wceq 1372   ∈ wcel 2175  0cc0 7924  ℕcn 9035  ℕ₀cn0 9294

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-1cn 8017  ax-icn 8019  ax-addcl 8020  ax-mulcl 8022  ax-i2m1 8029

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-n0 9295

This theorem is referenced by:  0xnn0  9363  elnn0z  9384  nn0ind-raph  9489  10nn0  9520  declei  9538  numlti  9539  nummul1c  9551  decaddc2  9558  decrmanc  9559  decrmac  9560  decaddm10  9561  decaddi  9562  decaddci  9563  decaddci2  9564  decmul1  9566  decmulnc  9569  6p5e11  9575  7p4e11  9578  8p3e11  9583  9p2e11  9589  10p10e20  9597  fz01or  10232  0elfz  10239  4fvwrd4  10261  fvinim0ffz  10368  0tonninf  10583  exple1  10738  sq10  10855  bc0k  10899  bcn1  10901  bccl  10910  fihasheq0  10936  iswrdiz  10999  iswrddm0  11016  fsumnn0cl  11656  binom  11737  bcxmas  11742  isumnn0nn  11746  geoserap  11760  ef0lem  11913  ege2le3  11924  ef4p  11947  efgt1p2  11948  efgt1p  11949  nn0o  12160  ndvdssub  12183  5ndvds3  12187  bits0  12201  0bits  12212  gcdval  12222  gcdcl  12229  dfgcd3  12273  nn0seqcvgd  12305  algcvg  12312  eucalg  12323  lcmcl  12336  pw2dvdslemn  12429  pclem0  12551  pcpre1  12557  pcfac  12615  dec5dvds2  12678  2exp11  12701  2exp16  12702  ennnfonelemj0  12714  ennnfonelem0  12718  ennnfonelem1  12720  plendxnocndx  12988  slotsdifdsndx  12999  slotsdifunifndx  13006  imasvalstrd  13044  cnfldstr  14262  nn0subm  14287  znf1o  14355  fczpsrbag  14375  psr1clfi  14392  mplsubgfilemm  14402  dveflem  15140  plyconst  15159  plycolemc  15172  pilem3  15197  1kp2ke3k  15593  ex-fac  15597  012of  15863  isomninnlem  15902  iswomninnlem  15921  iswomni0  15923  ismkvnnlem  15924