Theorem 0nn0 8303

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

Syntax hints:   ∨ wo 661   = wceq 1284   ∈ wcel 1433  0cc0 6981  ℕcn 8039  ℕ₀cn0 8288

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 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-1cn 7069  ax-icn 7071  ax-addcl 7072  ax-mulcl 7074  ax-i2m1 7081

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-un 2977  df-sn 3404  df-n0 8289

This theorem is referenced by:  elnn0z  8364  nn0ind-raph  8464  10nn0  8494  declei  8512  numlti  8513  nummul1c  8525  decaddc2  8532  decrmanc  8533  decrmac  8534  decaddm10  8535  decaddi  8536  decaddci  8537  decaddci2  8538  decmul1  8540  decmulnc  8543  6p5e11  8549  7p4e11  8552  8p3e11  8557  9p2e11  8563  10p10e20  8571  0elfz  9132  4fvwrd4  9150  fvinim0ffz  9250  exple1  9532  sq10  9640  bc0k  9683  bcn1  9685  bccl  9694  fz01or  10278  nn0o  10307  ndvdssub  10330  gcdval  10351  gcdcl  10358  dfgcd3  10399  nn0seqcvgd  10423  ialgcvg  10430  eucialg  10441  lcmcl  10454  pw2dvdslemn  10543  1kp2ke3k  10562  ex-fac  10565