ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  0nn0 GIF version

Theorem 0nn0 8254
Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
Assertion
Ref Expression
0nn0 0 ∈ ℕ0

Proof of Theorem 0nn0
StepHypRef Expression
1 eqid 2056 . 2 0 = 0
2 elnn0 8241 . . . 4 (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
32biimpri 128 . . 3 ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
43olcs 665 . 2 (0 = 0 → 0 ∈ ℕ0)
51, 4ax-mp 7 1 0 ∈ ℕ0
Colors of variables: wff set class
Syntax hints:  wo 639   = wceq 1259  wcel 1409  0cc0 6947  cn 7990  0cn0 8239
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-1cn 7035  ax-icn 7037  ax-addcl 7038  ax-mulcl 7040  ax-i2m1 7047
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-v 2576  df-un 2950  df-sn 3409  df-n0 8240
This theorem is referenced by:  elnn0z  8315  nn0ind-raph  8414  10nn0  8444  declei  8462  numlti  8463  nummul1c  8475  decaddc2  8482  decrmanc  8483  decrmac  8484  decaddm10  8485  decaddi  8486  decaddci  8487  decaddci2  8488  decmul1  8490  decmulnc  8493  6p5e11  8499  7p4e11  8502  8p3e11  8507  9p2e11  8513  10p10e20  8521  0elfz  9079  4fvwrd4  9099  fvinim0ffz  9198  exple1  9476  sq10  9584  bc0k  9624  bcn1  9626  bccl  9635  fz01or  10190  nn0o  10219  ndvdssub  10242  pw2dvdslemn  10253  nn0seqcvgd  10263  ialgcvg  10270  1kp2ke3k  10278  ex-fac  10281
  Copyright terms: Public domain W3C validator