Theorem 0nn0 9417

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

Syntax hints:   ∨ wo 715   = wceq 1397   ∈ wcel 2202  0cc0 8032  ℕcn 9143  ℕ₀cn0 9402

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1cn 8125  ax-icn 8127  ax-addcl 8128  ax-mulcl 8130  ax-i2m1 8137

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-n0 9403

This theorem is referenced by:  0xnn0  9471  elnn0z  9492  nn0ind-raph  9597  10nn0  9628  declei  9646  numlti  9647  nummul1c  9659  decaddc2  9666  decrmanc  9667  decrmac  9668  decaddm10  9669  decaddi  9670  decaddci  9671  decaddci2  9672  decmul1  9674  decmulnc  9677  6p5e11  9683  7p4e11  9686  8p3e11  9691  9p2e11  9697  10p10e20  9705  fz01or  10346  0elfz  10353  4fvwrd4  10375  fvinim0ffz  10488  0tonninf  10703  exple1  10858  sq10  10975  bc0k  11019  bcn1  11021  bccl  11030  fihasheq0  11056  iswrdiz  11124  iswrddm0  11141  s1leng  11205  s1fv  11207  eqs1  11209  s111  11212  ccat2s1fstg  11229  pfx00g  11260  s2fv0g  11372  s3fv0g  11376  fsumnn0cl  11969  binom  12050  bcxmas  12055  isumnn0nn  12059  geoserap  12073  ef0lem  12226  ege2le3  12237  ef4p  12260  efgt1p2  12261  efgt1p  12262  nn0o  12473  ndvdssub  12496  5ndvds3  12500  bits0  12514  0bits  12525  gcdval  12535  gcdcl  12542  dfgcd3  12586  nn0seqcvgd  12618  algcvg  12625  eucalg  12636  lcmcl  12649  pw2dvdslemn  12742  pclem0  12864  pcpre1  12870  pcfac  12928  dec5dvds2  12991  2exp11  13014  2exp16  13015  ennnfonelemj0  13027  ennnfonelem0  13031  ennnfonelem1  13033  plendxnocndx  13302  slotsdifdsndx  13313  slotsdifunifndx  13320  imasvalstrd  13358  cnfldstr  14578  nn0subm  14603  znf1o  14671  fczpsrbag  14691  psr1clfi  14708  mplsubgfilemm  14718  dveflem  15456  plyconst  15475  plycolemc  15488  pilem3  15513  clwwlkn0  16265  clwwlk0on0  16288  1kp2ke3k  16342  ex-fac  16346  depindlem1  16351  012of  16618  isomninnlem  16660  iswomninnlem  16680  iswomni0  16682  ismkvnnlem  16683  gfsum0  16709