Theorem 2nn 9200

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 9097	. 2 |- 2 = ( 1 + 1 )
2		1nn 9049	. . 3 |- 1 e. NN
3		peano2nn 9050	. . 3 |- ( 1 e. NN -> ( 1 + 1 ) e. NN )
4	2, 3	ax-mp 5	. 2 |- ( 1 + 1 ) e. NN
5	1, 4	eqeltri 2278	1 |- 2 e. NN

Syntax hints:   e. wcel 2176  (class class class)co 5946   1c1 7928   + caddc 7930   NNcn 9038   2c2 9089

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-sep 4163  ax-cnex 8018  ax-resscn 8019  ax-1re 8021  ax-addrcl 8024

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-int 3886  df-br 4046  df-iota 5233  df-fv 5280  df-ov 5949  df-inn 9039  df-2 9097

This theorem is referenced by:  3nn  9201  2nn0  9314  2z  9402  uz3m2nn  9696  ige2m1fz1  10233  qbtwnre  10401  flhalf  10447  sqeq0  10749  sqeq0d  10819  facavg  10893  bcn2  10911  resqrexlemnm  11362  abs00ap  11406  geo2sum  11858  geo2lim  11860  ege2le3  12015  ef01bndlem  12100  mod2eq0even  12222  mod2eq1n2dvds  12223  bitsdc  12291  bits0o  12294  bitsp1  12295  bitsp1o  12297  bitsfzolem  12298  bitsfzo  12299  bitsmod  12300  bitsfi  12301  bitscmp  12302  bitsinv1lem  12305  bitsinv1  12306  sqgcd  12383  3lcm2e6woprm  12441  prm2orodd  12481  3prm  12483  4nprm  12484  isprm5lem  12496  divgcdodd  12498  isevengcd2  12513  3lcm2e6  12515  pw2dvdslemn  12520  pw2dvds  12521  pw2dvdseulemle  12522  oddpwdclemxy  12524  oddpwdclemodd  12527  oddpwdclemdc  12528  oddpwdc  12529  sqpweven  12530  2sqpwodd  12531  pythagtriplem4  12624  oddprmdvds  12710  4sqlem5  12738  4sqlem6  12739  4sqlem10  12743  4sqlem12  12758  dec2dvds  12767  dec5nprm  12770  dec2nprm  12771  2expltfac  12795  evenennn  12797  exmidunben  12830  plusgndx  12974  plusgid  12975  plusgndxnn  12976  plusgslid  12977  grpstrg  12991  grpbaseg  12992  grpplusgg  12993  rngstrg  13000  lmodstrd  13029  topgrpstrd  13061  dsndx  13080  dsid  13081  dsslid  13082  dsndxnn  13083  slotsdifdsndx  13090  slotsdifunifndx  13097  imasvalstrd  13135  cnfldstr  14353  dveflem  15231  1sgm2ppw  15500  mersenne  15502  perfect1  15503  perfectlem1  15504  perfectlem2  15505  perfect  15506  lgsval  15514  lgsfvalg  15515  lgsfcl2  15516  lgsval2lem  15520  lgsdir2lem2  15539  lgsdir2  15543  gausslemma2dlem1a  15568  gausslemma2dlem1cl  15569  gausslemma2dlem1f1o  15570  gausslemma2dlem4  15574  gausslemma2d  15579  lgseisenlem1  15580  lgseisenlem2  15581  lgseisenlem3  15582  lgseisenlem4  15583  lgsquadlemofi  15586  lgsquadlem1  15587  lgsquadlem2  15588  lgsquad2lem2  15592  m1lgs  15595  2lgslem1c  15600  2lgslem3a1  15607  2lgslem3d1  15610  2lgslem4  15613  2lgs  15614  2sqlem3  15627  2sqlem8  15633  ex-fl  15698  ex-ceil  15699  redcwlpolemeq1  16030  nconstwlpolem0  16039