Theorem 1nn0 9293

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

Syntax hints:   ∈ wcel 2175  1c1 7908  ℕ₀cn0 9277

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-1re 8001

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-v 2773  df-un 3169  df-in 3171  df-ss 3178  df-int 3885  df-inn 9019  df-n0 9278

This theorem is referenced by:  peano2nn0  9317  deccl  9500  10nn0  9503  numsucc  9525  numadd  9532  numaddc  9533  11multnc  9553  6p5lem  9555  6p6e12  9559  7p5e12  9562  8p4e12  9567  9p2e11  9572  9p3e12  9573  10p10e20  9580  4t4e16  9584  5t2e10  9585  5t4e20  9587  6t3e18  9590  6t4e24  9591  7t3e21  9595  7t4e28  9596  8t3e24  9601  9t3e27  9608  9t9e81  9614  nn01to3  9720  fz0to3un2pr  10227  elfzom1elp1fzo  10312  fzo0sn0fzo1  10331  fldiv4lem1div2  10431  1tonninf  10567  expn1ap0  10675  nn0expcl  10679  sqval  10723  sq10  10838  nn0opthlem1d  10846  fac2  10857  bccl  10893  hashsng  10924  1elfz0hash  10932  snopiswrd  10979  wrdred1hash  11012  bcxmas  11719  arisum  11728  geoisum1  11749  geoisum1c  11750  cvgratnnlemsumlt  11758  mertenslem2  11766  fprodnn0cl  11842  ege2le3  11901  ef4p  11924  efgt1p2  11925  efgt1p  11926  sin01gt0  11992  dvds1  12083  3dvds2dec  12096  5ndvds6  12165  bitsmod  12186  bitsinv1lem  12191  isprm5  12383  pcelnn  12563  pockthg  12599  dec5nprm  12656  dec2nprm  12657  modxp1i  12660  2exp8  12677  2exp11  12678  2exp16  12679  2expltfac  12681  ennnfonelemhom  12705  ocndx  12961  ocid  12962  basendxnocndx  12963  plendxnocndx  12964  dsndx  12965  dsid  12966  dsslid  12967  dsndxnn  12968  basendxltdsndx  12969  slotsdifdsndx  12975  unifndx  12976  unifid  12977  unifndxnn  12978  basendxltunifndx  12979  slotsdifunifndx  12982  homndx  12983  homid  12984  homslid  12985  ccondx  12986  ccoid  12987  ccoslid  12988  imasvalstrd  13020  prdsvalstrd  13021  cnfldstr  14238  dveflem  15116  plyid  15136  1sgmprm  15384  perfectlem1  15389  perfectlem2  15390  2lgslem3a  15488  2lgslem3c  15490  1kp2ke3k  15524  ex-exp  15527  ex-fac  15528  012of  15794  isomninnlem  15833  trilpolemisumle  15841  iswomninnlem  15852  iswomni0  15854  ismkvnnlem  15855