Theorem 2nn 9079

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 8977	. 2 |- 2 = ( 1 + 1 )
2		1nn 8929	. . 3 |- 1 e. NN
3		peano2nn 8930	. . 3 |- ( 1 e. NN -> ( 1 + 1 ) e. NN )
4	2, 3	ax-mp 5	. 2 |- ( 1 + 1 ) e. NN
5	1, 4	eqeltri 2250	1 |- 2 e. NN

Syntax hints:   e. wcel 2148  (class class class)co 5874   1c1 7811   + caddc 7813   NNcn 8918   2c2 8969

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 8919  df-2 8977

This theorem is referenced by:  3nn  9080  2nn0  9192  2z  9280  uz3m2nn  9572  ige2m1fz1  10108  qbtwnre  10256  flhalf  10301  sqeq0  10582  sqeq0d  10652  facavg  10725  bcn2  10743  resqrexlemnm  11026  abs00ap  11070  geo2sum  11521  geo2lim  11523  ege2le3  11678  ef01bndlem  11763  mod2eq0even  11882  mod2eq1n2dvds  11883  sqgcd  12029  3lcm2e6woprm  12085  prm2orodd  12125  3prm  12127  4nprm  12128  isprm5lem  12140  divgcdodd  12142  isevengcd2  12157  3lcm2e6  12159  pw2dvdslemn  12164  pw2dvds  12165  pw2dvdseulemle  12166  oddpwdclemxy  12168  oddpwdclemodd  12171  oddpwdclemdc  12172  oddpwdc  12173  sqpweven  12174  2sqpwodd  12175  pythagtriplem4  12267  oddprmdvds  12351  4sqlem5  12379  4sqlem6  12380  4sqlem10  12384  evenennn  12393  exmidunben  12426  plusgndx  12567  plusgid  12568  plusgndxnn  12569  plusgslid  12570  grpstrg  12583  grpbaseg  12584  grpplusgg  12585  rngstrg  12592  lmodstrd  12621  topgrpstrd  12650  dsndx  12665  dsid  12666  dsslid  12667  dsndxnn  12668  slotsdifdsndx  12675  slotsdifunifndx  12682  dveflem  14157  lgsval  14375  lgsfvalg  14376  lgsfcl2  14377  lgsval2lem  14381  lgsdir2lem2  14400  lgsdir2  14404  lgseisenlem1  14420  lgseisenlem2  14421  m1lgs  14422  2sqlem3  14434  2sqlem8  14440  ex-fl  14447  ex-ceil  14448  redcwlpolemeq1  14772  nconstwlpolem0  14780