Theorem 2nn 9169

Description: 2 is a positive integer. (Contributed by NM, 20-Aug-2001.)

Assertion

Ref	Expression
2nn	|- 2 e. NN

Proof of Theorem 2nn

Step	Hyp	Ref	Expression
1		df-2 9066	. 2 |- 2 = ( 1 + 1 )
2		1nn 9018	. . 3 |- 1 e. NN
3		peano2nn 9019	. . 3 |- ( 1 e. NN -> ( 1 + 1 ) e. NN )
4	2, 3	ax-mp 5	. 2 |- ( 1 + 1 ) e. NN
5	1, 4	eqeltri 2269	1 |- 2 e. NN

Syntax hints:   e. wcel 2167  (class class class)co 5925   1c1 7897   + caddc 7899   NNcn 9007   2c2 9058

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152  ax-cnex 7987  ax-resscn 7988  ax-1re 7990  ax-addrcl 7993

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-int 3876  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928  df-inn 9008  df-2 9066

This theorem is referenced by:  3nn  9170  2nn0  9283  2z  9371  uz3m2nn  9664  ige2m1fz1  10201  qbtwnre  10363  flhalf  10409  sqeq0  10711  sqeq0d  10781  facavg  10855  bcn2  10873  resqrexlemnm  11200  abs00ap  11244  geo2sum  11696  geo2lim  11698  ege2le3  11853  ef01bndlem  11938  mod2eq0even  12060  mod2eq1n2dvds  12061  bitsdc  12129  bits0o  12132  bitsp1  12133  bitsp1o  12135  bitsfzolem  12136  bitsfzo  12137  bitsmod  12138  bitsfi  12139  bitscmp  12140  bitsinv1lem  12143  bitsinv1  12144  sqgcd  12221  3lcm2e6woprm  12279  prm2orodd  12319  3prm  12321  4nprm  12322  isprm5lem  12334  divgcdodd  12336  isevengcd2  12351  3lcm2e6  12353  pw2dvdslemn  12358  pw2dvds  12359  pw2dvdseulemle  12360  oddpwdclemxy  12362  oddpwdclemodd  12365  oddpwdclemdc  12366  oddpwdc  12367  sqpweven  12368  2sqpwodd  12369  pythagtriplem4  12462  oddprmdvds  12548  4sqlem5  12576  4sqlem6  12577  4sqlem10  12581  4sqlem12  12596  dec2dvds  12605  dec5nprm  12608  dec2nprm  12609  2expltfac  12633  evenennn  12635  exmidunben  12668  plusgndx  12812  plusgid  12813  plusgndxnn  12814  plusgslid  12815  grpstrg  12828  grpbaseg  12829  grpplusgg  12830  rngstrg  12837  lmodstrd  12866  topgrpstrd  12898  dsndx  12917  dsid  12918  dsslid  12919  dsndxnn  12920  slotsdifdsndx  12927  slotsdifunifndx  12934  imasvalstrd  12972  cnfldstr  14190  dveflem  15046  1sgm2ppw  15315  mersenne  15317  perfect1  15318  perfectlem1  15319  perfectlem2  15320  perfect  15321  lgsval  15329  lgsfvalg  15330  lgsfcl2  15331  lgsval2lem  15335  lgsdir2lem2  15354  lgsdir2  15358  gausslemma2dlem1a  15383  gausslemma2dlem1cl  15384  gausslemma2dlem1f1o  15385  gausslemma2dlem4  15389  gausslemma2d  15394  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgseisenlem4  15398  lgsquadlemofi  15401  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2lem2  15407  m1lgs  15410  2lgslem1c  15415  2lgslem3a1  15422  2lgslem3d1  15425  2lgslem4  15428  2lgs  15429  2sqlem3  15442  2sqlem8  15448  ex-fl  15455  ex-ceil  15456  redcwlpolemeq1  15785  nconstwlpolem0  15794