Theorem 0nn0 8999

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

Syntax hints:   ∨ wo 697   = wceq 1331   ∈ wcel 1480  0cc0 7627  ℕcn 8727  ℕ₀cn0 8984

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-1cn 7720  ax-icn 7722  ax-addcl 7723  ax-mulcl 7725  ax-i2m1 7732

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-n0 8985

This theorem is referenced by:  0xnn0  9053  elnn0z  9074  nn0ind-raph  9175  10nn0  9206  declei  9224  numlti  9225  nummul1c  9237  decaddc2  9244  decrmanc  9245  decrmac  9246  decaddm10  9247  decaddi  9248  decaddci  9249  decaddci2  9250  decmul1  9252  decmulnc  9255  6p5e11  9261  7p4e11  9264  8p3e11  9269  9p2e11  9275  10p10e20  9283  fz01or  9898  0elfz  9905  4fvwrd4  9924  fvinim0ffz  10025  0tonninf  10219  exple1  10356  sq10  10466  bc0k  10509  bcn1  10511  bccl  10520  fihasheq0  10547  fsumnn0cl  11179  binom  11260  bcxmas  11265  isumnn0nn  11269  geoserap  11283  ef0lem  11373  ege2le3  11384  ef4p  11407  efgt1p2  11408  efgt1p  11409  nn0o  11611  ndvdssub  11634  gcdval  11655  gcdcl  11662  dfgcd3  11705  nn0seqcvgd  11729  algcvg  11736  eucalg  11747  lcmcl  11760  pw2dvdslemn  11850  ennnfonelemj0  11921  ennnfonelem0  11925  ennnfonelem1  11927  dveflem  12865  pilem3  12874  1kp2ke3k  12946  ex-fac  12950  isomninnlem  13235