Theorem 0nn0 9222

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 2189	. 2 ⊢ 0 = 0
2		elnn0 9209	. . . 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 2160  0cc0 7842  ℕcn 8950  ℕ₀cn0 9207

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 2171  ax-1cn 7935  ax-icn 7937  ax-addcl 7938  ax-mulcl 7940  ax-i2m1 7947

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-sn 3613  df-n0 9208

This theorem is referenced by:  0xnn0  9276  elnn0z  9297  nn0ind-raph  9401  10nn0  9432  declei  9450  numlti  9451  nummul1c  9463  decaddc2  9470  decrmanc  9471  decrmac  9472  decaddm10  9473  decaddi  9474  decaddci  9475  decaddci2  9476  decmul1  9478  decmulnc  9481  6p5e11  9487  7p4e11  9490  8p3e11  9495  9p2e11  9501  10p10e20  9509  fz01or  10143  0elfz  10150  4fvwrd4  10172  fvinim0ffz  10273  0tonninf  10472  exple1  10610  sq10  10727  bc0k  10771  bcn1  10773  bccl  10782  fihasheq0  10808  fsumnn0cl  11446  binom  11527  bcxmas  11532  isumnn0nn  11536  geoserap  11550  ef0lem  11703  ege2le3  11714  ef4p  11737  efgt1p2  11738  efgt1p  11739  nn0o  11947  ndvdssub  11970  gcdval  11995  gcdcl  12002  dfgcd3  12046  nn0seqcvgd  12076  algcvg  12083  eucalg  12094  lcmcl  12107  pw2dvdslemn  12200  pclem0  12321  pcpre1  12327  pcfac  12385  ennnfonelemj0  12455  ennnfonelem0  12459  ennnfonelem1  12461  slotsdifdsndx  12735  slotsdifunifndx  12742  nn0subm  13903  fczpsrbag  13966  dveflem  14664  pilem3  14681  1kp2ke3k  14954  ex-fac  14958  012of  15224  isomninnlem  15257  iswomninnlem  15276  iswomni0  15278  ismkvnnlem  15279