Theorem 0nn0 9283

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 2196	. 2 ⊢ 0 = 0
2		elnn0 9270	. . . 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 2167  0cc0 7898  ℕcn 9009  ℕ₀cn0 9268

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-1cn 7991  ax-icn 7993  ax-addcl 7994  ax-mulcl 7996  ax-i2m1 8003

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-n0 9269

This theorem is referenced by:  0xnn0  9337  elnn0z  9358  nn0ind-raph  9462  10nn0  9493  declei  9511  numlti  9512  nummul1c  9524  decaddc2  9531  decrmanc  9532  decrmac  9533  decaddm10  9534  decaddi  9535  decaddci  9536  decaddci2  9537  decmul1  9539  decmulnc  9542  6p5e11  9548  7p4e11  9551  8p3e11  9556  9p2e11  9562  10p10e20  9570  fz01or  10205  0elfz  10212  4fvwrd4  10234  fvinim0ffz  10336  0tonninf  10551  exple1  10706  sq10  10823  bc0k  10867  bcn1  10869  bccl  10878  fihasheq0  10904  iswrdiz  10961  iswrddm0  10978  fsumnn0cl  11587  binom  11668  bcxmas  11673  isumnn0nn  11677  geoserap  11691  ef0lem  11844  ege2le3  11855  ef4p  11878  efgt1p2  11879  efgt1p  11880  nn0o  12091  ndvdssub  12114  5ndvds3  12118  bits0  12132  0bits  12143  gcdval  12153  gcdcl  12160  dfgcd3  12204  nn0seqcvgd  12236  algcvg  12243  eucalg  12254  lcmcl  12267  pw2dvdslemn  12360  pclem0  12482  pcpre1  12488  pcfac  12546  dec5dvds2  12609  2exp11  12632  2exp16  12633  ennnfonelemj0  12645  ennnfonelem0  12649  ennnfonelem1  12651  plendxnocndx  12918  slotsdifdsndx  12929  slotsdifunifndx  12936  imasvalstrd  12974  cnfldstr  14192  nn0subm  14217  znf1o  14285  fczpsrbag  14305  psr1clfi  14322  mplsubgfilemm  14332  dveflem  15070  plyconst  15089  plycolemc  15102  pilem3  15127  1kp2ke3k  15478  ex-fac  15482  012of  15748  isomninnlem  15787  iswomninnlem  15806  iswomni0  15808  ismkvnnlem  15809