Theorem 0nn0 9380

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

Syntax hints:   ∨ wo 713   = wceq 1395   ∈ wcel 2200  0cc0 7995  ℕcn 9106  ℕ₀cn0 9365

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1cn 8088  ax-icn 8090  ax-addcl 8091  ax-mulcl 8093  ax-i2m1 8100

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-n0 9366

This theorem is referenced by:  0xnn0  9434  elnn0z  9455  nn0ind-raph  9560  10nn0  9591  declei  9609  numlti  9610  nummul1c  9622  decaddc2  9629  decrmanc  9630  decrmac  9631  decaddm10  9632  decaddi  9633  decaddci  9634  decaddci2  9635  decmul1  9637  decmulnc  9640  6p5e11  9646  7p4e11  9649  8p3e11  9654  9p2e11  9660  10p10e20  9668  fz01or  10303  0elfz  10310  4fvwrd4  10332  fvinim0ffz  10442  0tonninf  10657  exple1  10812  sq10  10929  bc0k  10973  bcn1  10975  bccl  10984  fihasheq0  11010  iswrdiz  11073  iswrddm0  11090  s1leng  11152  s1fv  11154  eqs1  11156  s111  11159  pfx00g  11202  s2fv0g  11314  s3fv0g  11318  fsumnn0cl  11909  binom  11990  bcxmas  11995  isumnn0nn  11999  geoserap  12013  ef0lem  12166  ege2le3  12177  ef4p  12200  efgt1p2  12201  efgt1p  12202  nn0o  12413  ndvdssub  12436  5ndvds3  12440  bits0  12454  0bits  12465  gcdval  12475  gcdcl  12482  dfgcd3  12526  nn0seqcvgd  12558  algcvg  12565  eucalg  12576  lcmcl  12589  pw2dvdslemn  12682  pclem0  12804  pcpre1  12810  pcfac  12868  dec5dvds2  12931  2exp11  12954  2exp16  12955  ennnfonelemj0  12967  ennnfonelem0  12971  ennnfonelem1  12973  plendxnocndx  13242  slotsdifdsndx  13253  slotsdifunifndx  13260  imasvalstrd  13298  cnfldstr  14516  nn0subm  14541  znf1o  14609  fczpsrbag  14629  psr1clfi  14646  mplsubgfilemm  14656  dveflem  15394  plyconst  15413  plycolemc  15426  pilem3  15451  1kp2ke3k  16046  ex-fac  16050  012of  16316  isomninnlem  16357  iswomninnlem  16376  iswomni0  16378  ismkvnnlem  16379