Theorem 0nn0 9459

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

Syntax hints:   ∨ wo 716   = wceq 1398   ∈ wcel 2202  0cc0 8075  ℕcn 9185  ℕ₀cn0 9444

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-1cn 8168  ax-icn 8170  ax-addcl 8171  ax-mulcl 8173  ax-i2m1 8180

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-n0 9445

This theorem is referenced by:  0xnn0  9515  elnn0z  9536  nn0ind-raph  9641  10nn0  9672  declei  9690  numlti  9691  nummul1c  9703  decaddc2  9710  decrmanc  9711  decrmac  9712  decaddm10  9713  decaddi  9714  decaddci  9715  decaddci2  9716  decmul1  9718  decmulnc  9721  6p5e11  9727  7p4e11  9730  8p3e11  9735  9p2e11  9741  10p10e20  9749  fz01or  10391  0elfz  10398  4fvwrd4  10420  fvinim0ffz  10533  0tonninf  10748  exple1  10903  sq10  11020  bc0k  11064  bcn1  11066  bccl  11075  fihasheq0  11101  iswrdiz  11169  iswrddm0  11186  s1leng  11250  s1fv  11252  eqs1  11254  s111  11257  ccat2s1fstg  11274  pfx00g  11305  s2fv0g  11417  s3fv0g  11421  fsumnn0cl  12027  binom  12108  bcxmas  12113  isumnn0nn  12117  geoserap  12131  ef0lem  12284  ege2le3  12295  ef4p  12318  efgt1p2  12319  efgt1p  12320  nn0o  12531  ndvdssub  12554  5ndvds3  12558  bits0  12572  0bits  12583  gcdval  12593  gcdcl  12600  dfgcd3  12644  nn0seqcvgd  12676  algcvg  12683  eucalg  12694  lcmcl  12707  pw2dvdslemn  12800  pclem0  12922  pcpre1  12928  pcfac  12986  dec5dvds2  13049  2exp11  13072  2exp16  13073  ennnfonelemj0  13085  ennnfonelem0  13089  ennnfonelem1  13091  plendxnocndx  13360  slotsdifdsndx  13371  slotsdifunifndx  13378  imasvalstrd  13416  cnfldstr  14637  nn0subm  14662  znf1o  14730  fczpsrbag  14750  psr1clfi  14772  mplsubgfilemm  14782  dveflem  15520  plyconst  15539  plycolemc  15552  pilem3  15577  clwwlkn0  16332  clwwlk0on0  16355  konigsberglem2  16413  konigsberglem3  16414  konigsberglem5  16416  konigsberg  16417  1kp2ke3k  16421  ex-fac  16425  depindlem1  16430  012of  16696  isomninnlem  16745  iswomninnlem  16765  iswomni0  16767  ismkvnnlem  16768  gfsum0  16794