Theorem 0nn0 9191

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

Syntax hints:   ∨ wo 708   = wceq 1353   ∈ wcel 2148  0cc0 7811  ℕcn 8919  ℕ₀cn0 9176

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1cn 7904  ax-icn 7906  ax-addcl 7907  ax-mulcl 7909  ax-i2m1 7916

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134  df-sn 3599  df-n0 9177

This theorem is referenced by:  0xnn0  9245  elnn0z  9266  nn0ind-raph  9370  10nn0  9401  declei  9419  numlti  9420  nummul1c  9432  decaddc2  9439  decrmanc  9440  decrmac  9441  decaddm10  9442  decaddi  9443  decaddci  9444  decaddci2  9445  decmul1  9447  decmulnc  9450  6p5e11  9456  7p4e11  9459  8p3e11  9464  9p2e11  9470  10p10e20  9478  fz01or  10111  0elfz  10118  4fvwrd4  10140  fvinim0ffz  10241  0tonninf  10439  exple1  10576  sq10  10692  bc0k  10736  bcn1  10738  bccl  10747  fihasheq0  10773  fsumnn0cl  11411  binom  11492  bcxmas  11497  isumnn0nn  11501  geoserap  11515  ef0lem  11668  ege2le3  11679  ef4p  11702  efgt1p2  11703  efgt1p  11704  nn0o  11912  ndvdssub  11935  gcdval  11960  gcdcl  11967  dfgcd3  12011  nn0seqcvgd  12041  algcvg  12048  eucalg  12059  lcmcl  12072  pw2dvdslemn  12165  pclem0  12286  pcpre1  12292  pcfac  12348  ennnfonelemj0  12402  ennnfonelem0  12406  ennnfonelem1  12408  slotsdifdsndx  12676  slotsdifunifndx  12683  nn0subm  13480  dveflem  14190  pilem3  14207  1kp2ke3k  14479  ex-fac  14483  012of  14748  isomninnlem  14781  iswomninnlem  14800  iswomni0  14802  ismkvnnlem  14803