Theorem 2nn 9228

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 9125	. 2 |- 2 = ( 1 + 1 )
2		1nn 9077	. . 3 |- 1 e. NN
3		peano2nn 9078	. . 3 |- ( 1 e. NN -> ( 1 + 1 ) e. NN )
4	2, 3	ax-mp 5	. 2 |- ( 1 + 1 ) e. NN
5	1, 4	eqeltri 2279	1 |- 2 e. NN

Syntax hints:   e. wcel 2177  (class class class)co 5962   1c1 7956   + caddc 7958   NNcn 9066   2c2 9117

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 2188  ax-sep 4173  ax-cnex 8046  ax-resscn 8047  ax-1re 8049  ax-addrcl 8052

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3860  df-int 3895  df-br 4055  df-iota 5246  df-fv 5293  df-ov 5965  df-inn 9067  df-2 9125

This theorem is referenced by:  3nn  9229  2nn0  9342  2z  9430  uz3m2nn  9724  ige2m1fz1  10261  qbtwnre  10431  flhalf  10477  sqeq0  10779  sqeq0d  10849  facavg  10923  bcn2  10941  resqrexlemnm  11414  abs00ap  11458  geo2sum  11910  geo2lim  11912  ege2le3  12067  ef01bndlem  12152  mod2eq0even  12274  mod2eq1n2dvds  12275  bitsdc  12343  bits0o  12346  bitsp1  12347  bitsp1o  12349  bitsfzolem  12350  bitsfzo  12351  bitsmod  12352  bitsfi  12353  bitscmp  12354  bitsinv1lem  12357  bitsinv1  12358  sqgcd  12435  3lcm2e6woprm  12493  prm2orodd  12533  3prm  12535  4nprm  12536  isprm5lem  12548  divgcdodd  12550  isevengcd2  12565  3lcm2e6  12567  pw2dvdslemn  12572  pw2dvds  12573  pw2dvdseulemle  12574  oddpwdclemxy  12576  oddpwdclemodd  12579  oddpwdclemdc  12580  oddpwdc  12581  sqpweven  12582  2sqpwodd  12583  pythagtriplem4  12676  oddprmdvds  12762  4sqlem5  12790  4sqlem6  12791  4sqlem10  12795  4sqlem12  12810  dec2dvds  12819  dec5nprm  12822  dec2nprm  12823  2expltfac  12847  evenennn  12849  exmidunben  12882  plusgndx  13026  plusgid  13027  plusgndxnn  13028  plusgslid  13029  grpstrg  13043  grpbaseg  13044  grpplusgg  13045  rngstrg  13052  lmodstrd  13081  topgrpstrd  13113  dsndx  13132  dsid  13133  dsslid  13134  dsndxnn  13135  slotsdifdsndx  13142  slotsdifunifndx  13149  imasvalstrd  13187  cnfldstr  14405  dveflem  15283  1sgm2ppw  15552  mersenne  15554  perfect1  15555  perfectlem1  15556  perfectlem2  15557  perfect  15558  lgsval  15566  lgsfvalg  15567  lgsfcl2  15568  lgsval2lem  15572  lgsdir2lem2  15591  lgsdir2  15595  gausslemma2dlem1a  15620  gausslemma2dlem1cl  15621  gausslemma2dlem1f1o  15622  gausslemma2dlem4  15626  gausslemma2d  15631  lgseisenlem1  15632  lgseisenlem2  15633  lgseisenlem3  15634  lgseisenlem4  15635  lgsquadlemofi  15638  lgsquadlem1  15639  lgsquadlem2  15640  lgsquad2lem2  15644  m1lgs  15647  2lgslem1c  15652  2lgslem3a1  15659  2lgslem3d1  15662  2lgslem4  15665  2lgs  15666  2sqlem3  15679  2sqlem8  15685  ex-fl  15831  ex-ceil  15832  redcwlpolemeq1  16165  nconstwlpolem0  16174