Theorem 1nn0 9346

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 9082	. 2 |- 1 e. NN
2	1	nnnn0i 9338	1 |- 1 e. NN0

Syntax hints:   e. wcel 2178   1c1 7961   NN0cn0 9330

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-1re 8054

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-int 3900  df-inn 9072  df-n0 9331

This theorem is referenced by:  peano2nn0  9370  deccl  9553  10nn0  9556  numsucc  9578  numadd  9585  numaddc  9586  11multnc  9606  6p5lem  9608  6p6e12  9612  7p5e12  9615  8p4e12  9620  9p2e11  9625  9p3e12  9626  10p10e20  9633  4t4e16  9637  5t2e10  9638  5t4e20  9640  6t3e18  9643  6t4e24  9644  7t3e21  9648  7t4e28  9649  8t3e24  9654  9t3e27  9661  9t9e81  9667  nn01to3  9773  fz0to3un2pr  10280  elfzom1elp1fzo  10368  fzo0sn0fzo1  10387  fldiv4lem1div2  10487  1tonninf  10623  expn1ap0  10731  nn0expcl  10735  sqval  10779  sq10  10894  nn0opthlem1d  10902  fac2  10913  bccl  10949  hashsng  10980  1elfz0hash  10988  snopiswrd  11041  wrdred1hash  11074  pfx1  11194  bcxmas  11915  arisum  11924  geoisum1  11945  geoisum1c  11946  cvgratnnlemsumlt  11954  mertenslem2  11962  fprodnn0cl  12038  ege2le3  12097  ef4p  12120  efgt1p2  12121  efgt1p  12122  sin01gt0  12188  dvds1  12279  3dvds2dec  12292  5ndvds6  12361  bitsmod  12382  bitsinv1lem  12387  isprm5  12579  pcelnn  12759  pockthg  12795  dec5nprm  12852  dec2nprm  12853  modxp1i  12856  2exp8  12873  2exp11  12874  2exp16  12875  2expltfac  12877  ennnfonelemhom  12901  ocndx  13158  ocid  13159  basendxnocndx  13160  plendxnocndx  13161  dsndx  13162  dsid  13163  dsslid  13164  dsndxnn  13165  basendxltdsndx  13166  slotsdifdsndx  13172  unifndx  13173  unifid  13174  unifndxnn  13175  basendxltunifndx  13176  slotsdifunifndx  13179  homndx  13180  homid  13181  homslid  13182  ccondx  13183  ccoid  13184  ccoslid  13185  imasvalstrd  13217  prdsvalstrd  13218  cnfldstr  14435  dveflem  15313  plyid  15333  1sgmprm  15581  perfectlem1  15586  perfectlem2  15587  2lgslem3a  15685  2lgslem3c  15687  edgfid  15720  edgfndx  15721  edgfndxnn  15722  basendxltedgfndx  15724  1kp2ke3k  15860  ex-exp  15863  ex-fac  15864  012of  16130  isomninnlem  16171  trilpolemisumle  16179  iswomninnlem  16190  iswomni0  16192  ismkvnnlem  16193