Theorem 2nn0 9191

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

Assertion

Ref	Expression
2nn0	|- 2 e. NN0

Proof of Theorem 2nn0

Step	Hyp	Ref	Expression
1		2nn 9078	. 2 |- 2 e. NN
2	1	nnnn0i 9182	1 |- 2 e. NN0

Syntax hints:   e. wcel 2148   2c2 8968   NN0cn0 9174

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4121  ax-cnex 7901  ax-resscn 7902  ax-1re 7904  ax-addrcl 7907

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877  df-inn 8918  df-2 8976  df-n0 9175

This theorem is referenced by:  nn0n0n1ge2  9321  7p6e13  9459  8p3e11  9462  8p5e13  9464  9p3e12  9469  9p4e13  9470  4t3e12  9479  4t4e16  9480  5t3e15  9482  5t5e25  9484  6t3e18  9486  6t5e30  9488  7t3e21  9491  7t4e28  9492  7t5e35  9493  7t6e42  9494  7t7e49  9495  8t3e24  9497  8t4e32  9498  8t5e40  9499  9t3e27  9504  9t4e36  9505  9t8e72  9509  9t9e81  9510  decbin3  9523  2eluzge0  9573  nn01to3  9615  xnn0le2is012  9864  fzo0to42pr  10217  nn0sqcl  10544  sqmul  10579  resqcl  10584  zsqcl  10587  cu2  10615  i3  10618  i4  10619  binom3  10634  nn0opthlem1d  10695  fac3  10707  faclbnd2  10717  abssq  11085  sqabs  11086  ef4p  11697  efgt1p2  11698  efi4p  11720  ef01bndlem  11759  cos01bnd  11761  oexpneg  11876  oddge22np1  11880  isprm5  12136  pythagtriplem4  12262  oddprmdvds  12346  basendxltdsndx  12664  dsndxnplusgndx  12666  dsndxnmulrndx  12667  slotsdnscsi  12668  dsndxntsetndx  12669  slotsdifdsndx  12670  slotsdifunifndx  12677  setsmsdsg  13911  dveflem  14118  tangtx  14190  2logb9irr  14320  2logb9irrap  14326  binom4  14328  lgslem1  14332  1kp2ke3k  14396  ex-exp  14399  ex-fac  14400