Theorem 2nn 9283

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 9180	. 2 |- 2 = ( 1 + 1 )
2		1nn 9132	. . 3 |- 1 e. NN
3		peano2nn 9133	. . 3 |- ( 1 e. NN -> ( 1 + 1 ) e. NN )
4	2, 3	ax-mp 5	. 2 |- ( 1 + 1 ) e. NN
5	1, 4	eqeltri 2302	1 |- 2 e. NN

Syntax hints:   e. wcel 2200  (class class class)co 6007   1c1 8011   + caddc 8013   NNcn 9121   2c2 9172

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4202  ax-cnex 8101  ax-resscn 8102  ax-1re 8104  ax-addrcl 8107

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010  df-inn 9122  df-2 9180

This theorem is referenced by:  3nn  9284  2nn0  9397  2z  9485  uz3m2nn  9780  ige2m1fz1  10317  qbtwnre  10488  flhalf  10534  sqeq0  10836  sqeq0d  10906  facavg  10980  bcn2  10998  resqrexlemnm  11545  abs00ap  11589  geo2sum  12041  geo2lim  12043  ege2le3  12198  ef01bndlem  12283  mod2eq0even  12405  mod2eq1n2dvds  12406  bitsdc  12474  bits0o  12477  bitsp1  12478  bitsp1o  12480  bitsfzolem  12481  bitsfzo  12482  bitsmod  12483  bitsfi  12484  bitscmp  12485  bitsinv1lem  12488  bitsinv1  12489  sqgcd  12566  3lcm2e6woprm  12624  prm2orodd  12664  3prm  12666  4nprm  12667  isprm5lem  12679  divgcdodd  12681  isevengcd2  12696  3lcm2e6  12698  pw2dvdslemn  12703  pw2dvds  12704  pw2dvdseulemle  12705  oddpwdclemxy  12707  oddpwdclemodd  12710  oddpwdclemdc  12711  oddpwdc  12712  sqpweven  12713  2sqpwodd  12714  pythagtriplem4  12807  oddprmdvds  12893  4sqlem5  12921  4sqlem6  12922  4sqlem10  12926  4sqlem12  12941  dec2dvds  12950  dec5nprm  12953  dec2nprm  12954  2expltfac  12978  evenennn  12980  exmidunben  13013  plusgndx  13158  plusgid  13159  plusgndxnn  13160  plusgslid  13161  grpstrg  13175  grpbaseg  13176  grpplusgg  13177  rngstrg  13184  lmodstrd  13213  topgrpstrd  13245  dsndx  13264  dsid  13265  dsslid  13266  dsndxnn  13267  slotsdifdsndx  13274  slotsdifunifndx  13281  imasvalstrd  13319  cnfldstr  14538  dveflem  15416  1sgm2ppw  15685  mersenne  15687  perfect1  15688  perfectlem1  15689  perfectlem2  15690  perfect  15691  lgsval  15699  lgsfvalg  15700  lgsfcl2  15701  lgsval2lem  15705  lgsdir2lem2  15724  lgsdir2  15728  gausslemma2dlem1a  15753  gausslemma2dlem1cl  15754  gausslemma2dlem1f1o  15755  gausslemma2dlem4  15759  gausslemma2d  15764  lgseisenlem1  15765  lgseisenlem2  15766  lgseisenlem3  15767  lgseisenlem4  15768  lgsquadlemofi  15771  lgsquadlem1  15772  lgsquadlem2  15773  lgsquad2lem2  15777  m1lgs  15780  2lgslem1c  15785  2lgslem3a1  15792  2lgslem3d1  15795  2lgslem4  15798  2lgs  15799  2sqlem3  15812  2sqlem8  15818  clwwlkn2  16163  ex-fl  16172  ex-ceil  16173  redcwlpolemeq1  16510  nconstwlpolem0  16519