Theorem 0nn0 9407

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 9394	. . . 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 8022  ℕcn 9133  ℕ₀cn0 9392

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 8115  ax-icn 8117  ax-addcl 8118  ax-mulcl 8120  ax-i2m1 8127

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 2802  df-un 3202  df-sn 3673  df-n0 9393

This theorem is referenced by:  0xnn0  9461  elnn0z  9482  nn0ind-raph  9587  10nn0  9618  declei  9636  numlti  9637  nummul1c  9649  decaddc2  9656  decrmanc  9657  decrmac  9658  decaddm10  9659  decaddi  9660  decaddci  9661  decaddci2  9662  decmul1  9664  decmulnc  9667  6p5e11  9673  7p4e11  9676  8p3e11  9681  9p2e11  9687  10p10e20  9695  fz01or  10336  0elfz  10343  4fvwrd4  10365  fvinim0ffz  10477  0tonninf  10692  exple1  10847  sq10  10964  bc0k  11008  bcn1  11010  bccl  11019  fihasheq0  11045  iswrdiz  11110  iswrddm0  11127  s1leng  11191  s1fv  11193  eqs1  11195  s111  11198  ccat2s1fstg  11215  pfx00g  11246  s2fv0g  11358  s3fv0g  11362  fsumnn0cl  11954  binom  12035  bcxmas  12040  isumnn0nn  12044  geoserap  12058  ef0lem  12211  ege2le3  12222  ef4p  12245  efgt1p2  12246  efgt1p  12247  nn0o  12458  ndvdssub  12481  5ndvds3  12485  bits0  12499  0bits  12510  gcdval  12520  gcdcl  12527  dfgcd3  12571  nn0seqcvgd  12603  algcvg  12610  eucalg  12621  lcmcl  12634  pw2dvdslemn  12727  pclem0  12849  pcpre1  12855  pcfac  12913  dec5dvds2  12976  2exp11  12999  2exp16  13000  ennnfonelemj0  13012  ennnfonelem0  13016  ennnfonelem1  13018  plendxnocndx  13287  slotsdifdsndx  13298  slotsdifunifndx  13305  imasvalstrd  13343  cnfldstr  14562  nn0subm  14587  znf1o  14655  fczpsrbag  14675  psr1clfi  14692  mplsubgfilemm  14702  dveflem  15440  plyconst  15459  plycolemc  15472  pilem3  15497  clwwlkn0  16203  clwwlk0on0  16226  1kp2ke3k  16256  ex-fac  16260  012of  16528  isomninnlem  16570  iswomninnlem  16589  iswomni0  16591  ismkvnnlem  16592