MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2nn Structured version   Unicode version

Theorem 2nn 10714
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 10615 . 2  |-  2  =  ( 1  +  1 )
2 1nn 10567 . . 3  |-  1  e.  NN
3 peano2nn 10568 . . 3  |-  ( 1  e.  NN  ->  (
1  +  1 )  e.  NN )
42, 3ax-mp 5 . 2  |-  ( 1  +  1 )  e.  NN
51, 4eqeltri 2541 1  |-  2  e.  NN
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1819  (class class class)co 6296   1c1 9510    + caddc 9512   NNcn 10556   2c2 10606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-1cn 9567
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-ov 6299  df-om 6700  df-recs 7060  df-rdg 7094  df-nn 10557  df-2 10615
This theorem is referenced by:  3nn  10715  2nn0  10833  2z  10917  uz3m2nn  11148  ige2m1fz1  11793  sqeq0  12235  expmulnbnd  12301  sqeq0d  12312  faclbnd5  12379  bcn2  12400  f1oun2prg  12877  wwlktovf  12906  climcndslem1  13673  climcndslem2  13674  climcnds  13675  harmonic  13682  geo2sum  13694  geo2lim  13696  ege2le3  13837  ef01bndlem  13931  egt2lt3  13951  nthruc  13996  bits0o  14092  bitsp1  14093  bitsfzolem  14096  bitsfzo  14097  bitsmod  14098  bitsfi  14099  bitscmp  14100  bitsinv1lem  14103  bitsinv1  14104  2ebits  14109  bitsinvp1  14111  sadcaddlem  14119  sadadd3  14123  sadaddlem  14128  sadasslem  14132  bitsres  14135  bitsuz  14136  bitsshft  14137  smumullem  14154  smumul  14155  sqgcd  14208  3prm  14246  pythagtriplem4  14355  iserodd  14371  prmreclem3  14448  prmreclem5  14450  prmreclem6  14451  4sqlem12  14486  vdwlem3  14513  vdwlem9  14519  vdwlem10  14520  dec2dvds  14561  dec5nprm  14564  dec2nprm  14565  2expltfac  14589  4nprm  14602  5prm  14606  6nprm  14607  7prm  14608  8nprm  14609  10nprm  14611  11prm  14612  17prm  14614  23prm  14616  37prm  14618  43prm  14619  83prm  14620  139prm  14621  163prm  14622  317prm  14623  631prm  14624  1259lem1  14625  1259lem2  14626  1259lem3  14627  1259lem4  14628  1259lem5  14629  1259prm  14630  2503lem1  14631  2503lem2  14632  2503lem3  14633  2503prm  14634  4001lem1  14635  4001lem2  14636  4001lem3  14637  4001lem4  14638  4001prm  14639  plusgndx  14746  plusgid  14747  grpstr  14755  grpbase  14756  grpplusg  14757  ressplusg  14758  rngstr  14763  lmodstr  14780  topgrpstr  14805  dsndx  14819  dsid  14820  odrngstr  14823  ressds  14830  imasvalstr  14869  pmtrprfvalrn  16640  psgnunilem2  16647  psgnprfval  16673  psgnprfval1  16674  mgpds  17278  oppradd  17406  sraaddg  17952  srads  17959  opsrplusg  18271  cnfldstr  18549  zlmplusg  18683  znadd  18706  m2detleiblem1  19253  m2detleiblem5  19254  m2detleiblem6  19255  m2detleiblem3  19258  m2detleiblem4  19259  m2detleib  19260  tmslem  21111  tngplusg  21282  ovollb2lem  22025  ovolunlem1a  22033  ovolunlem1  22034  ovoliunlem1  22039  ovoliunlem3  22041  dyadf  22126  dyadovol  22128  dyadss  22129  dyaddisjlem  22130  dyadmaxlem  22132  opnmbllem  22136  mbfi1fseqlem1  22248  mbfi1fseqlem3  22250  mbfi1fseqlem4  22251  mbfi1fseqlem5  22252  mbfi1fseqlem6  22253  dveflem  22506  aaliou3lem9  22872  dcubic1lem  23300  dcubic2  23301  mcubic  23304  quartlem1  23314  quartlem2  23315  basellem1  23480  basellem2  23481  basellem3  23482  basellem4  23483  basellem5  23484  basellem6  23485  basellem7  23486  basellem8  23487  basellem9  23488  1sgm2ppw  23601  ppiublem1  23603  chtublem  23612  mersenne  23628  perfect1  23629  perfectlem1  23630  perfectlem2  23631  perfect  23632  pcbcctr  23677  bclbnd  23681  bposlem1  23685  bposlem2  23686  bposlem3  23687  bposlem4  23688  bposlem5  23689  bposlem6  23690  bposlem8  23692  lgsdir2lem2  23725  lgsqr  23747  lgseisenlem1  23750  lgseisenlem2  23751  lgseisenlem3  23752  lgseisenlem4  23753  lgsquadlem1  23755  lgsquadlem2  23756  lgsquad2lem2  23760  2sqlem3  23767  2sqlem8  23773  chebbnd1lem1  23780  chebbnd1lem3  23782  logdivsum  23844  log2sumbnd  23855  pntlemd  23905  pntlema  23907  pntlemb  23908  pntlemf  23916  pntlemo  23918  ostth2lem1  23929  trkgstr  23966  ttgplusg  24308  ttgds  24311  axlowdimlem6  24377  eengstr  24410  usgraexmpl  24528  cusgrasizeindb0  24597  usgrcyclnl2  24768  eupath2lem3  25106  konigsberg  25114  ex-xp  25284  ex-cnv  25285  ex-rn  25288  resvplusg  27984  oddpwdc  28490  eulerpartlemt  28507  eulerpartlemgh  28514  fib0  28535  fib1  28536  fib3  28539  zetacvg  28754  lgamgulmlem4  28771  problem5  29220  opnmbllem0  30255  mblfinlem1  30256  dvasin  30308  areacirclem1  30312  heiborlem3  30514  heiborlem5  30516  heiborlem6  30517  heiborlem7  30518  heiborlem8  30519  heibor  30522  jm2.17a  31102  jm2.17b  31103  jm2.17c  31104  acongrep  31122  acongeq  31125  jm2.27a  31151  jm2.27c  31153  rmydioph  31160  rmxdioph  31162  expdiophlem2  31168  expdioph  31169  frlmpwfi  31250  hashnzfz2  31430  lhe4.4ex1a  31438  wallispilem5  32054  wallispi2lem1  32056  wallispi2  32058  stirlinglem3  32061  stirlinglem8  32066  stirlinglem10  32068  stirlinglem15  32073  dirkertrigeqlem3  32085  fouriersw  32217  pfx2  32530  usgra2pthspth  32613  usgra2pthlem1  32615  hlhilsplus  37813
  Copyright terms: Public domain W3C validator