Theorem 2nn 11698

Description: 2 is a positive integer. (Contributed by NM, 20-Aug-2001.)

Assertion

Ref	Expression
2nn	⊢ 2 ∈ ℕ

Proof of Theorem 2nn

Step	Hyp	Ref	Expression
1		df-2 11688	. 2 ⊢ 2 = (1 + 1)
2		1nn 11636	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 11637	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2886	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2111  (class class class)co 7135  1c1 10527   + caddc 10529  ℕcn 11625  2c2 11680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-1cn 10584

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-om 7561  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-nn 11626  df-2 11688

This theorem is referenced by:  3nn  11704  2nn0  11902  2z  12002  uz3m2nn  12279  ige2m1fz1  12991  sqeq0  13482  sqeq0d  13505  expmulnbnd  13592  faclbnd5  13654  bcn2  13675  f1oun2prg  14270  wrdl2exs2  14299  pfx2  14300  wwlktovf  14311  reusq0  14814  climcndslem1  15196  climcndslem2  15197  climcnds  15198  harmonic  15206  geo2sum  15221  geo2lim  15223  ege2le3  15435  ef01bndlem  15529  egt2lt3  15551  nthruc  15597  mod2eq0even  15687  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  16418  5prm  16434  6nprm  16435  7prm  16436  8nprm  16437  10nprm  16439  11prm  16440  17prm  16442  23prm  16444  37prm  16446  43prm  16447  83prm  16448  139prm  16449  163prm  16450  317prm  16451  631prm  16452  1259lem1  16456  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  1259prm  16461  2503lem1  16462  2503lem2  16463  2503lem3  16464  2503prm  16465  4001lem1  16466  4001lem2  16467  4001lem3  16468  4001lem4  16469  4001prm  16470  plusgndx  16587  plusgid  16588  grpstr  16601  grpbase  16602  grpplusg  16603  ressplusg  16604  rngstr  16611  lmodstr  16628  topgrpstr  16653  dsndx  16667  dsid  16668  odrngstr  16671  ressds  16678  imasvalstr  16717  pmtrprfvalrn  18608  psgnunilem2  18615  psgnprfval  18641  psgnprfval1  18642  mgpds  19242  oppradd  19376  sraaddg  19944  srads  19951  cnfldstr  20093  cnfldfun  20103  zlmplusg  20212  znadd  20232  opsrplusg  20719  m2detleiblem1  21229  m2detleiblem5  21230  m2detleiblem6  21231  m2detleiblem3  21234  m2detleiblem4  21235  m2detleib  21236  tmslem  23089  tngplusg  23248  ovollb2lem  24092  ovolunlem1a  24100  ovolunlem1  24101  ovoliunlem1  24106  ovoliunlem3  24108  dyadf  24195  dyadovol  24197  dyadss  24198  dyaddisjlem  24199  dyadmaxlem  24201  opnmbllem  24205  mbfi1fseqlem1  24319  mbfi1fseqlem3  24321  mbfi1fseqlem4  24322  mbfi1fseqlem5  24323  mbfi1fseqlem6  24324  dveflem  24582  aaliou3lem9  24946  quartlem1  25443  quartlem2  25444  zetacvg  25600  lgamgulmlem4  25617  basellem1  25666  basellem2  25667  basellem3  25668  basellem4  25669  basellem5  25670  basellem6  25671  basellem7  25672  basellem8  25673  basellem9  25674  1sgm2ppw  25784  ppiublem1  25786  chtublem  25795  mersenne  25811  perfect1  25812  perfectlem1  25813  perfectlem2  25814  perfect  25815  pcbcctr  25860  bclbnd  25864  bposlem1  25868  bposlem2  25869  bposlem3  25870  bposlem4  25871  bposlem5  25872  bposlem6  25873  bposlem8  25875  lgsdir2lem2  25910  lgsqr  25935  lgsqrmodndvds  25937  gausslemma2dlem1a  25949  gausslemma2d  25958  lgseisenlem1  25959  lgseisenlem2  25960  lgseisenlem3  25961  lgseisenlem4  25962  lgsquadlem1  25964  lgsquadlem2  25965  lgsquad2lem2  25969  2lgslem1c  25977  2lgs  25991  2sqlem3  26004  2sqlem8  26010  chebbnd1lem1  26053  chebbnd1lem3  26055  logdivsum  26117  log2sumbnd  26128  pntlemd  26178  pntlema  26180  pntlemb  26181  pntlemf  26189  pntlemo  26191  ostth2lem1  26202  trkgstr  26238  ttgplusg  26672  ttgds  26675  axlowdimlem6  26741  eengstr  26774  usgrexmplef  27049  cusgrsizeindb0  27239  usgr2pthlem  27552  uspgrn2crct  27594  usgr2wspthons3  27750  clwwlkn2  27829  wwlksext2clwwlk  27842  eupth2lem3lem4  28016  frgrhash2wsp  28117  2clwwlk2clwwlk  28135  dlwwlknondlwlknonf1olem1  28149  clwlknon2num  28153  numclwlk2lem2f1o  28164  ex-xp  28221  ex-cnv  28222  ex-rn  28225  ex-mod  28234  resvplusg  30957  lmat22e11  31171  lmat22e12  31172  lmat22e21  31173  lmat22e22  31174  lmat22det  31175  oddpwdc  31722  eulerpartlemt  31739  eulerpartlemgh  31746  fib0  31767  fib1  31768  fib3  31771  chtvalz  32010  hgt750lem  32032  hgt750lemb  32037  hgt750leme  32039  problem5  33025  bcprod  33083  bj-endcomp  34731  opnmbllem0  35093  mblfinlem1  35094  dvasin  35141  areacirclem1  35145  heiborlem3  35251  heiborlem5  35253  heiborlem6  35254  heiborlem7  35255  heiborlem8  35256  heibor  35259  hlhilsplus  39236  12gcd5e1  39291  420gcd8e4  39294  12lcm5e60  39296  60lcm7e420  39298  420lcm8e840  39299  lcm2un  39302  lcmineqlem19  39335  lcmineqlem20  39336  lcmineqlem22  39338  lcmineqlem23  39339  lcmineqlem  39340  3lexlogpow5ineq2  39342  3lexlogpow5ineq3  39343  dffltz  39615  jm2.17a  39901  jm2.17b  39902  jm2.17c  39903  acongrep  39921  acongeq  39924  jm2.27a  39946  jm2.27c  39948  rmydioph  39955  rmxdioph  39957  expdiophlem2  39963  expdioph  39964  frlmpwfi  40042  amgm2d  40904  mnringaddgd  40928  hashnzfz2  41025  lhe4.4ex1a  41033  limsup10exlem  42414  wallispilem5  42711  wallispi2lem1  42713  wallispi2  42715  stirlinglem3  42718  stirlinglem8  42723  stirlinglem10  42725  stirlinglem15  42730  dirkertrigeqlem3  42742  fouriersw  42873  hoicvrrex  43195  ovnsubaddlem1  43209  ovnsubaddlem2  43210  ovnsubadd2lem  43284  ovolval5lem1  43291  ovolval5lem2  43292  elmod2  43887  fmtnoodd  44050  fmtnof1  44052  fmtnosqrt  44056  fmtnorec4  44066  257prm  44078  odz2prm2pw  44080  fmtnoprmfac1lem  44081  fmtnoprmfac1  44082  fmtnoprmfac2lem1  44083  fmtnoprmfac2  44084  fmtno4prm  44092  2pwp1prm  44106  139prmALT  44113  127prm  44116  sfprmdvdsmersenne  44121  lighneallem1  44123  lighneallem3  44125  proththdlem  44131  proththd  44132  iseven5  44182  oddprmALTV  44205  perfectALTVlem1  44239  perfectALTVlem2  44240  perfectALTV  44241  fppr2odd  44249  2exp340mod341  44251  341fppr2  44252  fpprel2  44259  nnsum3primes4  44306  nnsum3primesgbe  44310  evengpoap3  44317  nnsum4primesevenALTV  44319  bgoldbtbndlem1  44323  tgblthelfgott  44333  pw2m1lepw2m1  44929  nnpw2even  44943  logbpw2m1  44981  blenpw2  44992  nnpw2pmod  44997  blen2  44999  nnpw2p  45000  nnpw2pb  45001  blennnt2  45003  nnolog2flm1  45004  dig2nn1st  45019  0dig2pr01  45024  dig2nn0  45025  0dig2nn0e  45026  0dig2nn0o  45027  dig2bits  45028  dignn0flhalflem1  45029  dignn0ehalf  45031  dignn0flhalf  45032  nn0sumshdiglemA  45033  nn0sumshdiglemB  45034  nn0sumshdiglem1  45035  nn0sumshdiglem2  45036  nn0mullong  45039  itcovalt2lem2  45090  amgmw2d  45332