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

Theorem 2nn 11699
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 11689 . 2 2 = (1 + 1)
2 1nn 11638 . . 3 1 ∈ ℕ
3 peano2nn 11639 . . 3 (1 ∈ ℕ → (1 + 1) ∈ ℕ)
42, 3ax-mp 5 . 2 (1 + 1) ∈ ℕ
51, 4eqeltri 2909 1 2 ∈ ℕ
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  (class class class)co 7145  1c1 10527   + caddc 10529  cn 11627  2c2 11681
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-1cn 10584
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7148  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-nn 11628  df-2 11689
This theorem is referenced by:  3nn  11705  2nn0  11903  2z  12003  uz3m2nn  12280  ige2m1fz1  12986  sqeq0  13476  sqeq0d  13499  expmulnbnd  13586  faclbnd5  13648  bcn2  13669  f1oun2prg  14269  wrdl2exs2  14298  pfx2  14299  wwlktovf  14310  reusq0  14812  climcndslem1  15194  climcndslem2  15195  climcnds  15196  harmonic  15204  geo2sum  15219  geo2lim  15221  ege2le3  15433  ef01bndlem  15527  egt2lt3  15549  nthruc  15595  mod2eq0even  15685  bits0o  15769  bitsp1  15770  bitsfzolem  15773  bitsfzo  15774  bitsmod  15775  bitsfi  15776  bitscmp  15777  bitsinv1lem  15780  bitsinv1  15781  2ebits  15786  bitsinvp1  15788  sadcaddlem  15796  sadadd3  15800  sadaddlem  15805  sadasslem  15809  bitsres  15812  bitsuz  15813  bitsshft  15814  smumullem  15831  smumul  15832  sqgcd  15899  3lcm2e6woprm  15949  prm2orodd  16025  4nprm  16029  isevengcd2  16060  3lcm2e6  16062  pythagtriplem4  16146  iserodd  16162  oddprmdvds  16229  prmreclem3  16244  prmreclem5  16246  prmreclem6  16247  4sqlem12  16282  vdwlem3  16309  vdwlem9  16315  vdwlem10  16316  prmo2  16366  dec2dvds  16389  dec5nprm  16392  dec2nprm  16393  2expltfac  16416  5prm  16432  6nprm  16433  7prm  16434  8nprm  16435  10nprm  16437  11prm  16438  17prm  16440  23prm  16442  37prm  16444  43prm  16445  83prm  16446  139prm  16447  163prm  16448  317prm  16449  631prm  16450  1259lem1  16454  1259lem2  16455  1259lem3  16456  1259lem4  16457  1259lem5  16458  1259prm  16459  2503lem1  16460  2503lem2  16461  2503lem3  16462  2503prm  16463  4001lem1  16464  4001lem2  16465  4001lem3  16466  4001lem4  16467  4001prm  16468  plusgndx  16585  plusgid  16586  grpstr  16599  grpbase  16600  grpplusg  16601  ressplusg  16602  rngstr  16609  lmodstr  16626  topgrpstr  16651  dsndx  16665  dsid  16666  odrngstr  16669  ressds  16676  imasvalstr  16715  pmtrprfvalrn  18547  psgnunilem2  18554  psgnprfval  18580  psgnprfval1  18581  mgpds  19180  oppradd  19311  sraaddg  19882  srads  19889  opsrplusg  20190  cnfldstr  20477  cnfldfun  20487  zlmplusg  20596  znadd  20617  m2detleiblem1  21163  m2detleiblem5  21164  m2detleiblem6  21165  m2detleiblem3  21168  m2detleiblem4  21169  m2detleib  21170  tmslem  23021  tngplusg  23180  ovollb2lem  24018  ovolunlem1a  24026  ovolunlem1  24027  ovoliunlem1  24032  ovoliunlem3  24034  dyadf  24121  dyadovol  24123  dyadss  24124  dyaddisjlem  24125  dyadmaxlem  24127  opnmbllem  24131  mbfi1fseqlem1  24245  mbfi1fseqlem3  24247  mbfi1fseqlem4  24248  mbfi1fseqlem5  24249  mbfi1fseqlem6  24250  dveflem  24505  aaliou3lem9  24868  quartlem1  25362  quartlem2  25363  zetacvg  25520  lgamgulmlem4  25537  basellem1  25586  basellem2  25587  basellem3  25588  basellem4  25589  basellem5  25590  basellem6  25591  basellem7  25592  basellem8  25593  basellem9  25594  1sgm2ppw  25704  ppiublem1  25706  chtublem  25715  mersenne  25731  perfect1  25732  perfectlem1  25733  perfectlem2  25734  perfect  25735  pcbcctr  25780  bclbnd  25784  bposlem1  25788  bposlem2  25789  bposlem3  25790  bposlem4  25791  bposlem5  25792  bposlem6  25793  bposlem8  25795  lgsdir2lem2  25830  lgsqr  25855  lgsqrmodndvds  25857  gausslemma2dlem1a  25869  gausslemma2d  25878  lgseisenlem1  25879  lgseisenlem2  25880  lgseisenlem3  25881  lgseisenlem4  25882  lgsquadlem1  25884  lgsquadlem2  25885  lgsquad2lem2  25889  2lgslem1c  25897  2lgs  25911  2sqlem3  25924  2sqlem8  25930  chebbnd1lem1  25973  chebbnd1lem3  25975  logdivsum  26037  log2sumbnd  26048  pntlemd  26098  pntlema  26100  pntlemb  26101  pntlemf  26109  pntlemo  26111  ostth2lem1  26122  trkgstr  26158  ttgplusg  26592  ttgds  26595  axlowdimlem6  26661  eengstr  26694  usgrexmplef  26969  cusgrsizeindb0  27159  usgr2pthlem  27472  uspgrn2crct  27514  usgr2wspthons3  27671  clwwlkn2  27750  wwlksext2clwwlk  27764  eupth2lem3lem4  27938  frgrhash2wsp  28039  2clwwlk2clwwlk  28057  dlwwlknondlwlknonf1olem1  28071  clwlknon2num  28075  numclwlk2lem2f1o  28086  ex-xp  28143  ex-cnv  28144  ex-rn  28147  ex-mod  28156  resvplusg  30834  lmat22e11  30983  lmat22e12  30984  lmat22e21  30985  lmat22e22  30986  lmat22det  30987  oddpwdc  31512  eulerpartlemt  31529  eulerpartlemgh  31536  fib0  31557  fib1  31558  fib3  31561  chtvalz  31800  hgt750lem  31822  hgt750lemb  31827  hgt750leme  31829  problem5  32810  bcprod  32868  opnmbllem0  34810  mblfinlem1  34811  dvasin  34860  areacirclem1  34864  heiborlem3  34974  heiborlem5  34976  heiborlem6  34977  heiborlem7  34978  heiborlem8  34979  heibor  34982  hlhilsplus  38958  dffltz  39151  jm2.17a  39437  jm2.17b  39438  jm2.17c  39439  acongrep  39457  acongeq  39460  jm2.27a  39482  jm2.27c  39484  rmydioph  39491  rmxdioph  39493  expdiophlem2  39499  expdioph  39500  frlmpwfi  39578  amgm2d  40432  hashnzfz2  40533  lhe4.4ex1a  40541  limsup10exlem  41933  wallispilem5  42235  wallispi2lem1  42237  wallispi2  42239  stirlinglem3  42242  stirlinglem8  42247  stirlinglem10  42249  stirlinglem15  42254  dirkertrigeqlem3  42266  fouriersw  42397  hoicvrrex  42719  ovnsubaddlem1  42733  ovnsubaddlem2  42734  ovnsubadd2lem  42808  ovolval5lem1  42815  ovolval5lem2  42816  elmod2  43411  fmtnoodd  43542  fmtnof1  43544  fmtnosqrt  43548  fmtnorec4  43558  257prm  43570  odz2prm2pw  43572  fmtnoprmfac1lem  43573  fmtnoprmfac1  43574  fmtnoprmfac2lem1  43575  fmtnoprmfac2  43576  fmtno4prm  43584  2pwp1prm  43598  139prmALT  43606  127prm  43610  sfprmdvdsmersenne  43615  lighneallem1  43617  lighneallem3  43619  proththdlem  43625  proththd  43626  iseven5  43676  oddprmALTV  43699  perfectALTVlem1  43733  perfectALTVlem2  43734  perfectALTV  43735  fppr2odd  43743  2exp340mod341  43745  341fppr2  43746  fpprel2  43753  nnsum3primes4  43800  nnsum3primesgbe  43804  evengpoap3  43811  nnsum4primesevenALTV  43813  bgoldbtbndlem1  43817  tgblthelfgott  43827  pw2m1lepw2m1  44473  nnpw2even  44487  logbpw2m1  44525  blenpw2  44536  nnpw2pmod  44541  blen2  44543  nnpw2p  44544  nnpw2pb  44545  blennnt2  44547  nnolog2flm1  44548  dig2nn1st  44563  0dig2pr01  44568  dig2nn0  44569  0dig2nn0e  44570  0dig2nn0o  44571  dig2bits  44572  dignn0flhalflem1  44573  dignn0ehalf  44575  dignn0flhalf  44576  nn0sumshdiglemA  44577  nn0sumshdiglemB  44578  nn0sumshdiglem1  44579  nn0sumshdiglem2  44580  nn0mullong  44583  amgmw2d  44803
  Copyright terms: Public domain W3C validator