Theorem 1nn0 9477

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

Assertion

Ref	Expression
1nn0	|- 1 e. NN0

Proof of Theorem 1nn0

Step	Hyp	Ref	Expression
1		1nn 9213	. 2 |- 1 e. NN
2	1	nnnn0i 9469	1 |- 1 e. NN0

Syntax hints:   e. wcel 2202   1c1 8093   NN0cn0 9461

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-1re 8186

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-int 3934  df-inn 9203  df-n0 9462

This theorem is referenced by:  peano2nn0  9501  deccl  9686  10nn0  9689  numsucc  9711  numadd  9718  numaddc  9719  11multnc  9739  6p5lem  9741  6p6e12  9745  7p5e12  9748  8p4e12  9753  9p2e11  9758  9p3e12  9759  10p10e20  9766  4t4e16  9770  5t2e10  9771  5t4e20  9773  6t3e18  9776  6t4e24  9777  7t3e21  9781  7t4e28  9782  8t3e24  9787  9t3e27  9794  9t9e81  9800  nn01to3  9912  fz0to3un2pr  10420  elfzom1elp1fzo  10510  fzo0sn0fzo1  10529  fldiv4lem1div2  10630  1tonninf  10766  expn1ap0  10874  nn0expcl  10878  sqval  10922  sq10  11037  nn0opthlem1d  11045  fac2  11056  bccl  11092  hashsng  11123  1elfz0hash  11133  snopiswrd  11189  wrdred1hash  11223  pfx1  11350  s3fv1g  11439  bcxmas  12130  arisum  12139  geoisum1  12160  geoisum1c  12161  cvgratnnlemsumlt  12169  mertenslem2  12177  fprodnn0cl  12253  ege2le3  12312  ef4p  12335  efgt1p2  12336  efgt1p  12337  sin01gt0  12403  dvds1  12494  3dvds2dec  12507  5ndvds6  12576  bitsmod  12597  bitsinv1lem  12602  isprm5  12794  pcelnn  12974  pockthg  13010  dec5nprm  13067  dec2nprm  13068  modxp1i  13071  2exp8  13088  2exp11  13089  2exp16  13090  2expltfac  13092  ennnfonelemhom  13116  ocndx  13374  ocid  13375  basendxnocndx  13376  plendxnocndx  13377  dsndx  13378  dsid  13379  dsslid  13380  dsndxnn  13381  basendxltdsndx  13382  slotsdifdsndx  13388  unifndx  13389  unifid  13390  unifndxnn  13391  basendxltunifndx  13392  slotsdifunifndx  13395  homndx  13396  homid  13397  homslid  13398  ccondx  13399  ccoid  13400  ccoslid  13401  imasvalstrd  13433  prdsvalstrd  13434  cnfldstr  14654  dveflem  15537  plyid  15557  1sgmprm  15808  perfectlem1  15813  perfectlem2  15814  2lgslem3a  15912  2lgslem3c  15914  edgfid  15947  edgfndx  15948  edgfndxnn  15949  basendxltedgfndx  15951  clwwlkccatlem  16341  umgr2cwwkdifex  16366  konigsbergiedgwen  16425  konigsberglem1  16429  konigsberglem2  16430  konigsberglem3  16431  konigsberglem4  16432  konigsberglem5  16433  konigsberg  16434  1kp2ke3k  16438  ex-exp  16441  ex-fac  16442  012of  16713  isomninnlem  16762  trilpolemisumle  16770  iswomninnlem  16782  iswomni0  16784  ismkvnnlem  16785