Theorem 1nn0 8993

Description: 1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
1nn0	⊢ 1 ∈ ℕ0

Proof of Theorem 1nn0

Step	Hyp	Ref	Expression
1		1nn 8731	. 2 ⊢ 1 ∈ ℕ
2	1	nnnn0i 8985	1 ⊢ 1 ∈ ℕ0

Syntax hints:   ∈ wcel 1480  1c1 7621  ℕ₀cn0 8977

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-1re 7714

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-ral 2421  df-v 2688  df-un 3075  df-in 3077  df-ss 3084  df-int 3772  df-inn 8721  df-n0 8978

This theorem is referenced by:  peano2nn0  9017  deccl  9196  10nn0  9199  numsucc  9221  numadd  9228  numaddc  9229  11multnc  9249  6p5lem  9251  6p6e12  9255  7p5e12  9258  8p4e12  9263  9p2e11  9268  9p3e12  9269  10p10e20  9276  4t4e16  9280  5t2e10  9281  5t4e20  9283  6t3e18  9286  6t4e24  9287  7t3e21  9291  7t4e28  9292  8t3e24  9297  9t3e27  9304  9t9e81  9310  nn01to3  9409  elfzom1elp1fzo  9979  fzo0sn0fzo1  9998  1tonninf  10213  expn1ap0  10303  nn0expcl  10307  sqval  10351  sq10  10459  nn0opthlem1d  10466  fac2  10477  bccl  10513  hashsng  10544  1elfz0hash  10552  bcxmas  11258  arisum  11267  geoisum1  11288  geoisum1c  11289  cvgratnnlemsumlt  11297  mertenslem2  11305  ege2le3  11377  ef4p  11400  efgt1p2  11401  efgt1p  11402  sin01gt0  11468  dvds1  11551  3dvds2dec  11563  ennnfonelemhom  11928  dsndx  12117  dsid  12118  dsslid  12119  dveflem  12855  1kp2ke3k  12936  ex-exp  12939  ex-fac  12940  isomninnlem  13225  trilpolemisumle  13231