Theorem 0nn0 9150

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 2170	. 2 ⊢ 0 = 0
2		elnn0 9137	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 132	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 731	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

Syntax hints:   ∨ wo 703   = wceq 1348   ∈ wcel 2141  0cc0 7774  ℕcn 8878  ℕ₀cn0 9135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-1cn 7867  ax-icn 7869  ax-addcl 7870  ax-mulcl 7872  ax-i2m1 7879

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-n0 9136

This theorem is referenced by:  0xnn0  9204  elnn0z  9225  nn0ind-raph  9329  10nn0  9360  declei  9378  numlti  9379  nummul1c  9391  decaddc2  9398  decrmanc  9399  decrmac  9400  decaddm10  9401  decaddi  9402  decaddci  9403  decaddci2  9404  decmul1  9406  decmulnc  9409  6p5e11  9415  7p4e11  9418  8p3e11  9423  9p2e11  9429  10p10e20  9437  fz01or  10067  0elfz  10074  4fvwrd4  10096  fvinim0ffz  10197  0tonninf  10395  exple1  10532  sq10  10646  bc0k  10690  bcn1  10692  bccl  10701  fihasheq0  10728  fsumnn0cl  11366  binom  11447  bcxmas  11452  isumnn0nn  11456  geoserap  11470  ef0lem  11623  ege2le3  11634  ef4p  11657  efgt1p2  11658  efgt1p  11659  nn0o  11866  ndvdssub  11889  gcdval  11914  gcdcl  11921  dfgcd3  11965  nn0seqcvgd  11995  algcvg  12002  eucalg  12013  lcmcl  12026  pw2dvdslemn  12119  pclem0  12240  pcpre1  12246  pcfac  12302  ennnfonelemj0  12356  ennnfonelem0  12360  ennnfonelem1  12362  dveflem  13481  pilem3  13498  1kp2ke3k  13759  ex-fac  13763  012of  14028  isomninnlem  14062  iswomninnlem  14081  iswomni0  14083  ismkvnnlem  14084