Theorem 0nn0 9258

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

Syntax hints:   ∨ wo 709   = wceq 1364   ∈ wcel 2164  0cc0 7874  ℕcn 8984  ℕ₀cn0 9243

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-1cn 7967  ax-icn 7969  ax-addcl 7970  ax-mulcl 7972  ax-i2m1 7979

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-n0 9244

This theorem is referenced by:  0xnn0  9312  elnn0z  9333  nn0ind-raph  9437  10nn0  9468  declei  9486  numlti  9487  nummul1c  9499  decaddc2  9506  decrmanc  9507  decrmac  9508  decaddm10  9509  decaddi  9510  decaddci  9511  decaddci2  9512  decmul1  9514  decmulnc  9517  6p5e11  9523  7p4e11  9526  8p3e11  9531  9p2e11  9537  10p10e20  9545  fz01or  10180  0elfz  10187  4fvwrd4  10209  fvinim0ffz  10311  0tonninf  10514  exple1  10669  sq10  10786  bc0k  10830  bcn1  10832  bccl  10841  fihasheq0  10867  iswrdiz  10924  iswrddm0  10941  fsumnn0cl  11549  binom  11630  bcxmas  11635  isumnn0nn  11639  geoserap  11653  ef0lem  11806  ege2le3  11817  ef4p  11840  efgt1p2  11841  efgt1p  11842  nn0o  12051  ndvdssub  12074  gcdval  12099  gcdcl  12106  dfgcd3  12150  nn0seqcvgd  12182  algcvg  12189  eucalg  12200  lcmcl  12213  pw2dvdslemn  12306  pclem0  12427  pcpre1  12433  pcfac  12491  ennnfonelemj0  12561  ennnfonelem0  12565  ennnfonelem1  12567  slotsdifdsndx  12841  slotsdifunifndx  12848  cnfldstr  14057  nn0subm  14082  znf1o  14150  fczpsrbag  14168  dveflem  14905  plyconst  14924  plycolemc  14936  pilem3  14959  1kp2ke3k  15286  ex-fac  15290  012of  15556  isomninnlem  15590  iswomninnlem  15609  iswomni0  15611  ismkvnnlem  15612