ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2nn Unicode version

Theorem 2nn 9066
Description: 2 is a positive integer. (Contributed by NM, 20-Aug-2001.)
Assertion
Ref Expression
2nn  |-  2  e.  NN

Proof of Theorem 2nn
StepHypRef Expression
1 df-2 8964 . 2  |-  2  =  ( 1  +  1 )
2 1nn 8916 . . 3  |-  1  e.  NN
3 peano2nn 8917 . . 3  |-  ( 1  e.  NN  ->  (
1  +  1 )  e.  NN )
42, 3ax-mp 5 . 2  |-  ( 1  +  1 )  e.  NN
51, 4eqeltri 2250 1  |-  2  e.  NN
Colors of variables: wff set class
Syntax hints:    e. wcel 2148  (class class class)co 5869   1c1 7800    + caddc 7802   NNcn 8905   2c2 8956
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 4118  ax-cnex 7890  ax-resscn 7891  ax-1re 7893  ax-addrcl 7896
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 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-br 4001  df-iota 5174  df-fv 5220  df-ov 5872  df-inn 8906  df-2 8964
This theorem is referenced by:  3nn  9067  2nn0  9179  2z  9267  uz3m2nn  9559  ige2m1fz1  10092  qbtwnre  10240  flhalf  10285  sqeq0  10566  sqeq0d  10635  facavg  10707  bcn2  10725  resqrexlemnm  11008  abs00ap  11052  geo2sum  11503  geo2lim  11505  ege2le3  11660  ef01bndlem  11745  mod2eq0even  11863  mod2eq1n2dvds  11864  sqgcd  12010  3lcm2e6woprm  12066  prm2orodd  12106  3prm  12108  4nprm  12109  isprm5lem  12121  divgcdodd  12123  isevengcd2  12138  3lcm2e6  12140  pw2dvdslemn  12145  pw2dvds  12146  pw2dvdseulemle  12147  oddpwdclemxy  12149  oddpwdclemodd  12152  oddpwdclemdc  12153  oddpwdc  12154  sqpweven  12155  2sqpwodd  12156  pythagtriplem4  12248  oddprmdvds  12332  4sqlem5  12360  4sqlem6  12361  4sqlem10  12365  evenennn  12374  exmidunben  12407  plusgndx  12546  plusgid  12547  plusgslid  12548  grpstrg  12560  grpbaseg  12561  grpplusgg  12562  rngstrg  12569  lmodstrd  12590  topgrpstrd  12615  dsndx  12622  dsid  12623  dsslid  12624  dsndxnn  12625  slotsdifdsndx  12632  dveflem  13847  lgsval  14065  lgsfvalg  14066  lgsfcl2  14067  lgsval2lem  14071  lgsdir2lem2  14090  lgsdir2  14094  2sqlem3  14113  2sqlem8  14119  ex-fl  14126  ex-ceil  14127  redcwlpolemeq1  14451  nconstwlpolem0  14459
  Copyright terms: Public domain W3C validator