Theorem 0nn0 8624

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 2085	. 2 ⊢ 0 = 0
2		elnn0 8611	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 131	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 688	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 7	1 ⊢ 0 ∈ ℕ0

Syntax hints:   ∨ wo 662   = wceq 1287   ∈ wcel 1436  0cc0 7297  ℕcn 8360  ℕ₀cn0 8609

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-1cn 7385  ax-icn 7387  ax-addcl 7388  ax-mulcl 7390  ax-i2m1 7397

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-un 2992  df-sn 3437  df-n0 8610

This theorem is referenced by:  0xnn0  8678  elnn0z  8699  nn0ind-raph  8799  10nn0  8829  declei  8847  numlti  8848  nummul1c  8860  decaddc2  8867  decrmanc  8868  decrmac  8869  decaddm10  8870  decaddi  8871  decaddci  8872  decaddci2  8873  decmul1  8875  decmulnc  8878  6p5e11  8884  7p4e11  8887  8p3e11  8892  9p2e11  8898  10p10e20  8906  fz01or  9458  0elfz  9463  4fvwrd4  9482  fvinim0ffz  9583  0tonninf  9776  exple1  9931  sq10  10039  bc0k  10082  bcn1  10084  bccl  10093  fihasheq0  10120  fsumnn0cl  10704  nn0o  10832  ndvdssub  10855  gcdval  10876  gcdcl  10883  dfgcd3  10924  nn0seqcvgd  10948  ialgcvg  10955  eucialg  10966  lcmcl  10979  pw2dvdslemn  11068  1kp2ke3k  11140  ex-fac  11143