Theorem 1nn0 9106

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 8844	. 2 ⊢ 1 ∈ ℕ
2	1	nnnn0i 9098	1 ⊢ 1 ∈ ℕ0

Syntax hints:   ∈ wcel 2128  1c1 7733  ℕ₀cn0 9090

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 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139  ax-1re 7826

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-int 3808  df-inn 8834  df-n0 9091

This theorem is referenced by:  peano2nn0  9130  deccl  9309  10nn0  9312  numsucc  9334  numadd  9341  numaddc  9342  11multnc  9362  6p5lem  9364  6p6e12  9368  7p5e12  9371  8p4e12  9376  9p2e11  9381  9p3e12  9382  10p10e20  9389  4t4e16  9393  5t2e10  9394  5t4e20  9396  6t3e18  9399  6t4e24  9400  7t3e21  9404  7t4e28  9405  8t3e24  9410  9t3e27  9417  9t9e81  9423  nn01to3  9526  elfzom1elp1fzo  10101  fzo0sn0fzo1  10120  1tonninf  10339  expn1ap0  10429  nn0expcl  10433  sqval  10477  sq10  10586  nn0opthlem1d  10594  fac2  10605  bccl  10641  hashsng  10672  1elfz0hash  10680  bcxmas  11386  arisum  11395  geoisum1  11416  geoisum1c  11417  cvgratnnlemsumlt  11425  mertenslem2  11433  fprodnn0cl  11509  ege2le3  11568  ef4p  11591  efgt1p2  11592  efgt1p  11593  sin01gt0  11658  dvds1  11744  3dvds2dec  11756  ennnfonelemhom  12144  dsndx  12348  dsid  12349  dsslid  12350  dveflem  13087  1kp2ke3k  13300  ex-exp  13303  ex-fac  13304  012of  13567  isomninnlem  13601  trilpolemisumle  13609  iswomninnlem  13620  iswomni0  13622  ismkvnnlem  13623