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

Theorem 2nn 11170
Description: 2 is a positive integer. (Contributed by NM, 20-Aug-2001.)
Assertion
Ref Expression
2nn 2 ∈ ℕ

Proof of Theorem 2nn
StepHypRef Expression
1 df-2 11064 . 2 2 = (1 + 1)
2 1nn 11016 . . 3 1 ∈ ℕ
3 peano2nn 11017 . . 3 (1 ∈ ℕ → (1 + 1) ∈ ℕ)
42, 3ax-mp 5 . 2 (1 + 1) ∈ ℕ
51, 4eqeltri 2695 1 2 ∈ ℕ
Colors of variables: wff setvar class
Syntax hints:  wcel 1988  (class class class)co 6635  1c1 9922   + caddc 9924  cn 11005  2c2 11055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-1cn 9979
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-ov 6638  df-om 7051  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-nn 11006  df-2 11064
This theorem is referenced by:  3nn  11171  2nn0  11294  2z  11394  uz3m2nn  11716  ige2m1fz1  12413  sqeq0  12910  expmulnbnd  12979  sqeq0d  12990  faclbnd5  13068  bcn2  13089  f1oun2prg  13643  wrdl2exs2  13671  wwlktovf  13680  climcndslem1  14562  climcndslem2  14563  climcnds  14564  harmonic  14572  geo2sum  14585  geo2lim  14587  ege2le3  14801  ef01bndlem  14895  egt2lt3  14915  nthruc  14962  mod2eq0even  15051  bits0o  15133  bitsp1  15134  bitsfzolem  15137  bitsfzo  15138  bitsmod  15139  bitsfi  15140  bitscmp  15141  bitsinv1lem  15144  bitsinv1  15145  2ebits  15150  bitsinvp1  15152  sadcaddlem  15160  sadadd3  15164  sadaddlem  15169  sadasslem  15173  bitsres  15176  bitsuz  15177  bitsshft  15178  smumullem  15195  smumul  15196  sqgcd  15259  3lcm2e6woprm  15309  prm2orodd  15385  3prm  15387  4nprm  15388  isevengcd2  15419  3lcm2e6  15421  pythagtriplem4  15505  iserodd  15521  oddprmdvds  15588  prmreclem3  15603  prmreclem5  15605  prmreclem6  15606  4sqlem12  15641  vdwlem3  15668  vdwlem9  15674  vdwlem10  15675  prmo2  15725  dec2dvds  15748  dec5nprm  15751  dec2nprm  15752  2expltfac  15780  5prm  15796  6nprm  15797  7prm  15798  8nprm  15799  10nprm  15801  10nprmOLD  15802  11prm  15803  17prm  15805  23prm  15807  37prm  15809  43prm  15810  83prm  15811  139prm  15812  163prm  15813  317prm  15814  631prm  15815  1259lem1  15819  1259lem2  15820  1259lem3  15821  1259lem4  15822  1259lem5  15823  1259prm  15824  2503lem1  15825  2503lem2  15826  2503lem3  15827  2503prm  15828  4001lem1  15829  4001lem2  15830  4001lem3  15831  4001lem4  15832  4001prm  15833  plusgndx  15957  plusgid  15958  grpstr  15971  grpbase  15972  grpplusg  15973  ressplusg  15974  rngstr  15981  lmodstr  15998  topgrpstr  16023  dsndx  16043  dsid  16044  odrngstr  16047  ressds  16054  imasvalstr  16093  pmtrprfvalrn  17889  psgnunilem2  17896  psgnprfval  17922  psgnprfval1  17923  mgpds  18480  oppradd  18611  sraaddg  19160  srads  19167  opsrplusg  19461  cnfldstr  19729  cnfldfun  19739  zlmplusg  19848  znadd  19870  m2detleiblem1  20411  m2detleiblem5  20412  m2detleiblem6  20413  m2detleiblem3  20416  m2detleiblem4  20417  m2detleib  20418  tmslem  22268  tngplusg  22427  ovollb2lem  23237  ovolunlem1a  23245  ovolunlem1  23246  ovoliunlem1  23251  ovoliunlem3  23253  dyadf  23340  dyadovol  23342  dyadss  23343  dyaddisjlem  23344  dyadmaxlem  23346  opnmbllem  23350  mbfi1fseqlem1  23463  mbfi1fseqlem3  23465  mbfi1fseqlem4  23466  mbfi1fseqlem5  23467  mbfi1fseqlem6  23468  dveflem  23723  aaliou3lem9  24086  dcubic1lem  24551  dcubic2  24552  mcubic  24555  quartlem1  24565  quartlem2  24566  zetacvg  24722  lgamgulmlem4  24739  basellem1  24788  basellem2  24789  basellem3  24790  basellem4  24791  basellem5  24792  basellem6  24793  basellem7  24794  basellem8  24795  basellem9  24796  1sgm2ppw  24906  ppiublem1  24908  chtublem  24917  mersenne  24933  perfect1  24934  perfectlem1  24935  perfectlem2  24936  perfect  24937  pcbcctr  24982  bclbnd  24986  bposlem1  24990  bposlem2  24991  bposlem3  24992  bposlem4  24993  bposlem5  24994  bposlem6  24995  bposlem8  24997  lgsdir2lem2  25032  lgsqr  25057  lgsqrmodndvds  25059  gausslemma2dlem1a  25071  gausslemma2d  25080  lgseisenlem1  25081  lgseisenlem2  25082  lgseisenlem3  25083  lgseisenlem4  25084  lgsquadlem1  25086  lgsquadlem2  25087  lgsquad2lem2  25091  2lgslem1c  25099  2lgs  25113  2sqlem3  25126  2sqlem8  25132  chebbnd1lem1  25139  chebbnd1lem3  25141  logdivsum  25203  log2sumbnd  25214  pntlemd  25264  pntlema  25266  pntlemb  25267  pntlemf  25275  pntlemo  25277  ostth2lem1  25288  trkgstr  25324  ttgplusg  25739  ttgds  25742  axlowdimlem6  25808  eengstr  25841  usgrexmplef  26132  cusgrsizeindb0  26326  usgr2pthlem  26640  uspgrn2crct  26681  usgr2wspthons3  26838  clwwlksn2  26890  wwlksext2clwwlk  26904  eupth2lem3lem4  27071  frgrhash2wsp  27170  numclwwlkovf2  27189  numclwwlk2lem1  27206  numclwlk2lem2f  27207  numclwlk2lem2f1o  27209  ex-xp  27263  ex-cnv  27264  ex-rn  27267  ex-mod  27276  resvplusg  29807  lmat22e11  29858  lmat22e12  29859  lmat22e21  29860  lmat22e22  29861  lmat22det  29862  oddpwdc  30390  eulerpartlemt  30407  eulerpartlemgh  30414  fib0  30435  fib1  30436  fib3  30439  chtvalz  30681  hgt750lem  30703  hgt750lemb  30708  hgt750leme  30710  problem5  31537  bcprod  31599  opnmbllem0  33416  mblfinlem1  33417  dvasin  33467  areacirclem1  33471  heiborlem3  33583  heiborlem5  33585  heiborlem6  33586  heiborlem7  33587  heiborlem8  33588  heibor  33591  hlhilsplus  37051  jm2.17a  37346  jm2.17b  37347  jm2.17c  37348  acongrep  37366  acongeq  37369  jm2.27a  37391  jm2.27c  37393  rmydioph  37400  rmxdioph  37402  expdiophlem2  37408  expdioph  37409  frlmpwfi  37487  amgm2d  38321  hashnzfz2  38340  lhe4.4ex1a  38348  limsup10exlem  39798  wallispilem5  40049  wallispi2lem1  40051  wallispi2  40053  stirlinglem3  40056  stirlinglem8  40061  stirlinglem10  40063  stirlinglem15  40068  dirkertrigeqlem3  40080  fouriersw  40211  hoicvrrex  40533  ovnsubaddlem1  40547  ovnsubaddlem2  40548  ovnsubadd2lem  40622  ovolval5lem1  40629  ovolval5lem2  40630  elmod2  41104  pfx2  41177  fmtnoodd  41210  fmtnof1  41212  fmtnosqrt  41216  fmtnorec4  41226  257prm  41238  odz2prm2pw  41240  fmtnoprmfac1lem  41241  fmtnoprmfac1  41242  fmtnoprmfac2lem1  41243  fmtnoprmfac2  41244  fmtno4prm  41252  2pwp1prm  41268  139prmALT  41276  127prm  41280  sfprmdvdsmersenne  41285  lighneallem1  41287  lighneallem3  41289  proththdlem  41295  proththd  41296  iseven5  41341  oddprmALTV  41363  perfectALTVlem1  41395  perfectALTVlem2  41396  perfectALTV  41397  nnsum3primes4  41441  nnsum3primesgbe  41445  evengpoap3  41452  nnsum4primesevenALTV  41454  bgoldbtbndlem1  41458  tgblthelfgott  41468  tgblthelfgottOLD  41474  pw2m1lepw2m1  42075  nnpw2even  42088  logbpw2m1  42126  blenpw2  42137  nnpw2pmod  42142  blen2  42144  nnpw2p  42145  nnpw2pb  42146  blennnt2  42148  nnolog2flm1  42149  dig2nn1st  42164  0dig2pr01  42169  dig2nn0  42170  0dig2nn0e  42171  0dig2nn0o  42172  dig2bits  42173  dignn0flhalflem1  42174  dignn0ehalf  42176  dignn0flhalf  42177  nn0sumshdiglemA  42178  nn0sumshdiglemB  42179  nn0sumshdiglem1  42180  nn0sumshdiglem2  42181  nn0mullong  42184  amgmw2d  42315
  Copyright terms: Public domain W3C validator