Theorem 1nn0 9256

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

Syntax hints:   ∈ wcel 2164  1c1 7873  ℕ₀cn0 9240

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-1re 7966

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-int 3871  df-inn 8983  df-n0 9241

This theorem is referenced by:  peano2nn0  9280  deccl  9462  10nn0  9465  numsucc  9487  numadd  9494  numaddc  9495  11multnc  9515  6p5lem  9517  6p6e12  9521  7p5e12  9524  8p4e12  9529  9p2e11  9534  9p3e12  9535  10p10e20  9542  4t4e16  9546  5t2e10  9547  5t4e20  9549  6t3e18  9552  6t4e24  9553  7t3e21  9557  7t4e28  9558  8t3e24  9563  9t3e27  9570  9t9e81  9576  nn01to3  9682  fz0to3un2pr  10189  elfzom1elp1fzo  10269  fzo0sn0fzo1  10288  fldiv4lem1div2  10376  1tonninf  10512  expn1ap0  10620  nn0expcl  10624  sqval  10668  sq10  10783  nn0opthlem1d  10791  fac2  10802  bccl  10838  hashsng  10869  1elfz0hash  10877  snopiswrd  10924  wrdred1hash  10957  bcxmas  11632  arisum  11641  geoisum1  11662  geoisum1c  11663  cvgratnnlemsumlt  11671  mertenslem2  11679  fprodnn0cl  11755  ege2le3  11814  ef4p  11837  efgt1p2  11838  efgt1p  11839  sin01gt0  11905  dvds1  11995  3dvds2dec  12007  isprm5  12280  pcelnn  12459  pockthg  12495  ennnfonelemhom  12572  dsndx  12828  dsid  12829  dsslid  12830  dsndxnn  12831  basendxltdsndx  12832  slotsdifdsndx  12838  unifndx  12839  unifid  12840  unifndxnn  12841  basendxltunifndx  12842  slotsdifunifndx  12845  homid  12846  homslid  12847  ccoid  12848  ccoslid  12849  cnfldstr  14049  dveflem  14872  plyid  14892  1kp2ke3k  15216  ex-exp  15219  ex-fac  15220  012of  15486  isomninnlem  15520  trilpolemisumle  15528  iswomninnlem  15539  iswomni0  15541  ismkvnnlem  15542