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

Theorem 2nn 11028
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 10922 . 2 2 = (1 + 1)
2 1nn 10874 . . 3 1 ∈ ℕ
3 peano2nn 10875 . . 3 (1 ∈ ℕ → (1 + 1) ∈ ℕ)
42, 3ax-mp 5 . 2 (1 + 1) ∈ ℕ
51, 4eqeltri 2679 1 2 ∈ ℕ
Colors of variables: wff setvar class
Syntax hints:  wcel 1975  (class class class)co 6523  1c1 9789   + caddc 9791  cn 10863  2c2 10913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-1cn 9846
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-ral 2896  df-rex 2897  df-reu 2898  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-iun 4447  df-br 4574  df-opab 4634  df-mpt 4635  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-pred 5579  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-ov 6526  df-om 6931  df-wrecs 7267  df-recs 7328  df-rdg 7366  df-nn 10864  df-2 10922
This theorem is referenced by:  3nn  11029  2nn0  11152  2z  11238  uz3m2nn  11559  ige2m1fz1  12249  sqeq0  12740  expmulnbnd  12809  sqeq0d  12820  faclbnd5  12898  bcn2  12919  f1oun2prg  13454  wrdl2exs2  13480  wwlktovf  13489  climcndslem1  14362  climcndslem2  14363  climcnds  14364  harmonic  14372  geo2sum  14385  geo2lim  14387  ege2le3  14601  ef01bndlem  14695  egt2lt3  14715  nthruc  14761  mod2eq0even  14850  bits0o  14932  bitsp1  14933  bitsfzolem  14936  bitsfzo  14937  bitsmod  14938  bitsfi  14939  bitscmp  14940  bitsinv1lem  14943  bitsinv1  14944  2ebits  14949  bitsinvp1  14951  sadcaddlem  14959  sadadd3  14963  sadaddlem  14968  sadasslem  14972  bitsres  14975  bitsuz  14976  bitsshft  14977  smumullem  14994  smumul  14995  sqgcd  15058  3lcm2e6woprm  15108  prm2orodd  15184  3prm  15186  4nprm  15187  isevengcd2  15218  3lcm2e6  15220  pythagtriplem4  15304  iserodd  15320  oddprmdvds  15387  prmreclem3  15402  prmreclem5  15404  prmreclem6  15405  4sqlem12  15440  vdwlem3  15467  vdwlem9  15473  vdwlem10  15474  prmo2  15524  dec2dvds  15547  dec5nprm  15550  dec2nprm  15551  2expltfac  15579  5prm  15595  6nprm  15596  7prm  15597  8nprm  15598  10nprm  15600  10nprmOLD  15601  11prm  15602  17prm  15604  23prm  15606  37prm  15608  43prm  15609  83prm  15610  139prm  15611  163prm  15612  317prm  15613  631prm  15614  1259lem1  15618  1259lem2  15619  1259lem3  15620  1259lem4  15621  1259lem5  15622  1259prm  15623  2503lem1  15624  2503lem2  15625  2503lem3  15626  2503prm  15627  4001lem1  15628  4001lem2  15629  4001lem3  15630  4001lem4  15631  4001prm  15632  plusgndx  15745  plusgid  15746  grpstr  15757  grpbase  15758  grpplusg  15759  ressplusg  15760  rngstr  15765  lmodstr  15782  topgrpstr  15807  dsndx  15827  dsid  15828  odrngstr  15831  ressds  15838  imasvalstr  15877  pmtrprfvalrn  17673  psgnunilem2  17680  psgnprfval  17706  psgnprfval1  17707  mgpds  18264  oppradd  18395  sraaddg  18942  srads  18949  opsrplusg  19243  cnfldstr  19511  zlmplusg  19627  znadd  19649  m2detleiblem1  20187  m2detleiblem5  20188  m2detleiblem6  20189  m2detleiblem3  20192  m2detleiblem4  20193  m2detleib  20194  tmslem  22034  tngplusg  22190  ovollb2lem  22976  ovolunlem1a  22984  ovolunlem1  22985  ovoliunlem1  22990  ovoliunlem3  22992  dyadf  23078  dyadovol  23080  dyadss  23081  dyaddisjlem  23082  dyadmaxlem  23084  opnmbllem  23088  mbfi1fseqlem1  23201  mbfi1fseqlem3  23203  mbfi1fseqlem4  23204  mbfi1fseqlem5  23205  mbfi1fseqlem6  23206  dveflem  23459  aaliou3lem9  23822  dcubic1lem  24283  dcubic2  24284  mcubic  24287  quartlem1  24297  quartlem2  24298  zetacvg  24454  lgamgulmlem4  24471  basellem1  24520  basellem2  24521  basellem3  24522  basellem4  24523  basellem5  24524  basellem6  24525  basellem7  24526  basellem8  24527  basellem9  24528  1sgm2ppw  24638  ppiublem1  24640  chtublem  24649  mersenne  24665  perfect1  24666  perfectlem1  24667  perfectlem2  24668  perfect  24669  pcbcctr  24714  bclbnd  24718  bposlem1  24722  bposlem2  24723  bposlem3  24724  bposlem4  24725  bposlem5  24726  bposlem6  24727  bposlem8  24729  lgsdir2lem2  24764  lgsqr  24789  lgsqrmodndvds  24791  gausslemma2dlem1a  24803  gausslemma2d  24812  lgseisenlem1  24813  lgseisenlem2  24814  lgseisenlem3  24815  lgseisenlem4  24816  lgsquadlem1  24818  lgsquadlem2  24819  lgsquad2lem2  24823  2lgslem1c  24831  2lgs  24845  2sqlem3  24858  2sqlem8  24864  chebbnd1lem1  24871  chebbnd1lem3  24873  logdivsum  24935  log2sumbnd  24946  pntlemd  24996  pntlema  24998  pntlemb  24999  pntlemf  25007  pntlemo  25009  ostth2lem1  25020  trkgstr  25056  ttgplusg  25472  ttgds  25475  axlowdimlem6  25541  eengstr  25574  usgraexmplef  25691  cusgrasizeindb0  25761  usgrcyclnl2  25931  eupath2lem3  26268  ex-xp  26447  ex-cnv  26448  ex-rn  26451  ex-mod  26460  resvplusg  28966  lmat22e11  29014  lmat22e12  29015  lmat22e21  29016  lmat22e22  29017  lmat22det  29018  oddpwdc  29545  eulerpartlemt  29562  eulerpartlemgh  29569  fib0  29590  fib1  29591  fib3  29594  problem5  30619  bcprod  30679  opnmbllem0  32414  mblfinlem1  32415  dvasin  32465  areacirclem1  32469  heiborlem3  32581  heiborlem5  32583  heiborlem6  32584  heiborlem7  32585  heiborlem8  32586  heibor  32589  hlhilsplus  36049  jm2.17a  36344  jm2.17b  36345  jm2.17c  36346  acongrep  36364  acongeq  36367  jm2.27a  36389  jm2.27c  36391  rmydioph  36398  rmxdioph  36400  expdiophlem2  36406  expdioph  36407  frlmpwfi  36485  amgm2d  37322  hashnzfz2  37341  lhe4.4ex1a  37349  wallispilem5  38762  wallispi2lem1  38764  wallispi2  38766  stirlinglem3  38769  stirlinglem8  38774  stirlinglem10  38776  stirlinglem15  38781  dirkertrigeqlem3  38793  fouriersw  38924  hoicvrrex  39246  ovnsubaddlem1  39260  ovnsubaddlem2  39261  ovnsubadd2lem  39335  ovolval5lem1  39342  ovolval5lem2  39343  elmod2  39751  fmtnoodd  39784  fmtnof1  39786  fmtnosqrt  39790  fmtnorec4  39800  257prm  39812  odz2prm2pw  39814  fmtnoprmfac1lem  39815  fmtnoprmfac1  39816  fmtnoprmfac2lem1  39817  fmtnoprmfac2  39818  fmtno4prm  39826  2pwp1prm  39842  139prmALT  39850  127prm  39854  sfprmdvdsmersenne  39859  lighneallem1  39861  lighneallem3  39863  proththdlem  39869  proththd  39870  iseven5  39915  oddprmALTV  39937  perfectALTVlem1  39965  perfectALTVlem2  39966  perfectALTV  39967  nnsum3primes4  40005  nnsum3primesgbe  40009  evengpoap3  40016  nnsum4primesevenALTV  40018  bgoldbtbndlem1  40022  tgblthelfgott  40030  tgblthelfgottOLD  40037  pfx2  40076  cusgrsizeindb0  40663  usgr2pthlem  40967  uspgrn2crct  41009  usgr2wspthons3  41165  clwwlksn2  41215  wwlksext2clwwlk  41229  eupth2lem3lem4  41397  frgrhash2wsp  41495  av-numclwwlkovf2  41513  av-numclwwlk2lem1  41530  av-numclwlk2lem2f  41531  av-numclwlk2lem2f1o  41533  pw2m1lepw2m1  42102  nnpw2even  42115  logbpw2m1  42157  blenpw2  42168  nnpw2pmod  42173  blen2  42175  nnpw2p  42176  nnpw2pb  42177  blennnt2  42179  nnolog2flm1  42180  dig2nn1st  42195  0dig2pr01  42200  dig2nn0  42201  0dig2nn0e  42202  0dig2nn0o  42203  dig2bits  42204  dignn0flhalflem1  42205  dignn0ehalf  42207  dignn0flhalf  42208  nn0sumshdiglemA  42209  nn0sumshdiglemB  42210  nn0sumshdiglem1  42211  nn0sumshdiglem2  42212  nn0mullong  42215  amgmw2d  42318
  Copyright terms: Public domain W3C validator