Theorem 2nn 12311

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 12301	. 2 ⊢ 2 = (1 + 1)
2		1nn 12249	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12250	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2830	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2108  (class class class)co 7403  1c1 11128   + caddc 11130  ℕcn 12238  2c2 12293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7727  ax-1cn 11185

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-ov 7406  df-om 7860  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-nn 12239  df-2 12301

This theorem is referenced by:  3nn  12317  2ne0  12342  2nn0  12516  2z  12622  uz3m2nn  12905  ige2m1fz1  13631  sqeq0  14136  sqeq0d  14161  expmulnbnd  14251  faclbnd5  14314  bcn2  14335  f1oun2prg  14934  wrdl2exs2  14963  pfx2  14964  wwlktovf  14973  reusq0  15479  climcndslem1  15863  climcndslem2  15864  climcnds  15865  harmonic  15873  geo2sum  15887  geo2lim  15889  ege2le3  16104  ef01bndlem  16200  egt2lt3  16222  nthruc  16268  mod2eq0even  16363  bits0o  16447  bitsp1  16448  bitsfzolem  16451  bitsfzo  16452  bitsmod  16453  bitsfi  16454  bitscmp  16455  bitsinv1lem  16458  bitsinv1  16459  2ebits  16464  bitsinvp1  16466  sadcaddlem  16474  sadadd3  16478  sadaddlem  16483  sadasslem  16487  bitsres  16490  bitsuz  16491  bitsshft  16492  smumullem  16509  smumul  16510  sqgcd  16579  3lcm2e6woprm  16632  prm2orodd  16708  4nprm  16712  prmdvdssq  16735  isevengcd2  16747  3lcm2e6  16749  pythagtriplem4  16837  iserodd  16853  oddprmdvds  16921  prmreclem3  16936  prmreclem5  16938  prmreclem6  16939  4sqlem12  16974  vdwlem3  17001  vdwlem9  17007  vdwlem10  17008  prmo2  17058  dec2dvds  17081  dec5nprm  17084  dec2nprm  17085  2expltfac  17110  5prm  17126  6nprm  17127  7prm  17128  8nprm  17129  10nprm  17131  11prm  17132  17prm  17134  23prm  17136  37prm  17138  43prm  17139  83prm  17140  139prm  17141  163prm  17142  317prm  17143  631prm  17144  1259lem1  17148  1259lem2  17149  1259lem3  17150  1259lem4  17151  1259lem5  17152  1259prm  17153  2503lem1  17154  2503lem2  17155  2503lem3  17156  2503prm  17157  4001lem1  17158  4001lem2  17159  4001lem3  17160  4001lem4  17161  4001prm  17162  plusgndx  17295  plusgid  17296  plusgndxnn  17297  rngstr  17310  lmodstr  17337  topgrpstr  17373  dsndx  17397  dsid  17398  dsndxnn  17399  slotsdifdsndx  17406  slotsdifunifndx  17413  odrngstr  17415  imasvalstr  17463  pmtrprfvalrn  19467  psgnunilem2  19474  psgnprfval  19500  psgnprfval1  19501  cnfldstr  21315  cnfldstrOLD  21330  m2detleiblem1  22560  m2detleiblem5  22561  m2detleiblem6  22562  m2detleiblem3  22565  m2detleiblem4  22566  m2detleib  22567  ovollb2lem  25439  ovolunlem1a  25447  ovolunlem1  25448  ovoliunlem1  25453  ovoliunlem3  25455  dyadf  25542  dyadovol  25544  dyadss  25545  dyaddisjlem  25546  dyadmaxlem  25548  opnmbllem  25552  mbfi1fseqlem1  25666  mbfi1fseqlem3  25668  mbfi1fseqlem4  25669  mbfi1fseqlem5  25670  mbfi1fseqlem6  25671  dveflem  25933  aaliou3lem9  26308  quartlem1  26817  quartlem2  26818  zetacvg  26975  lgamgulmlem4  26992  basellem1  27041  basellem2  27042  basellem3  27043  basellem4  27044  basellem5  27045  basellem6  27046  basellem7  27047  basellem8  27048  basellem9  27049  1sgm2ppw  27161  ppiublem1  27163  chtublem  27172  mersenne  27188  perfect1  27189  perfectlem1  27190  perfectlem2  27191  perfect  27192  pcbcctr  27237  bclbnd  27241  bposlem1  27245  bposlem2  27246  bposlem3  27247  bposlem4  27248  bposlem5  27249  bposlem6  27250  bposlem8  27252  lgsdir2lem2  27287  lgsqr  27312  lgsqrmodndvds  27314  gausslemma2dlem1a  27326  gausslemma2d  27335  lgseisenlem1  27336  lgseisenlem2  27337  lgseisenlem3  27338  lgseisenlem4  27339  lgsquadlem1  27341  lgsquadlem2  27342  lgsquad2lem2  27346  2lgslem1c  27354  2lgs  27368  2sqlem3  27381  2sqlem8  27387  chebbnd1lem1  27430  chebbnd1lem3  27432  logdivsum  27494  log2sumbnd  27505  pntlemd  27555  pntlema  27557  pntlemb  27558  pntlemf  27566  pntlemo  27568  ostth2lem1  27579  slotsinbpsd  28366  slotslnbpsd  28367  trkgstr  28369  axlowdimlem6  28872  eengstr  28905  usgrexmplef  29184  cusgrsizeindb0  29375  usgr2pthlem  29691  uspgrn2crct  29736  usgr2wspthons3  29892  clwwlkn2  29971  wwlksext2clwwlk  29984  eupth2lem3lem4  30158  frgrhash2wsp  30259  2clwwlk2clwwlk  30277  dlwwlknondlwlknonf1olem1  30291  clwlknon2num  30295  numclwlk2lem2f1o  30306  ex-xp  30363  ex-cnv  30364  ex-rn  30367  ex-mod  30376  2exple2exp  32770  fldext2rspun  33669  cos9thpiminplylem1  33762  lmat22e11  33795  lmat22e12  33796  lmat22e21  33797  lmat22e22  33798  lmat22det  33799  oddpwdc  34332  eulerpartlemt  34349  eulerpartlemgh  34356  fib0  34377  fib1  34378  fib3  34381  chtvalz  34607  hgt750lem  34629  hgt750lemb  34634  hgt750leme  34636  problem5  35637  bcprod  35701  opnmbllem0  37626  mblfinlem1  37627  dvasin  37674  areacirclem1  37678  heiborlem3  37783  heiborlem5  37785  heiborlem6  37786  heiborlem7  37787  heiborlem8  37788  heibor  37791  12gcd5e1  41962  420gcd8e4  41965  12lcm5e60  41967  60lcm7e420  41969  420lcm8e840  41970  lcm2un  41973  lcmineqlem19  42006  lcmineqlem20  42007  lcmineqlem22  42009  lcmineqlem23  42010  lcmineqlem  42011  3lexlogpow2ineq1  42017  3lexlogpow2ineq2  42018  aks4d1p1p6  42032  aks4d1p1p5  42034  readvrec2  42351  dffltz  42604  flt4lem2  42617  flt4lem5  42620  flt4lem5a  42622  flt4lem5b  42623  flt4lem5c  42624  flt4lem5d  42625  flt4lem5e  42626  flt4lem7  42629  nna4b4nsq  42630  jm2.17a  42931  jm2.17b  42932  jm2.17c  42933  acongrep  42951  acongeq  42954  jm2.27a  42976  jm2.27c  42978  rmydioph  42985  rmxdioph  42987  expdiophlem2  42993  expdioph  42994  frlmpwfi  43069  amgm2d  44169  hashnzfz2  44293  lhe4.4ex1a  44301  limsup10exlem  45749  wallispilem5  46046  wallispi2lem1  46048  wallispi2  46050  stirlinglem3  46053  stirlinglem8  46058  stirlinglem10  46060  stirlinglem15  46065  dirkertrigeqlem3  46077  fouriersw  46208  hoicvrrex  46533  ovnsubaddlem1  46547  ovnsubaddlem2  46548  ovnsubadd2lem  46622  ovolval5lem1  46629  ovolval5lem2  46630  ceilhalfelfzo1  47307  elmod2  47332  fmtnoodd  47495  fmtnof1  47497  fmtnosqrt  47501  fmtnorec4  47511  257prm  47523  odz2prm2pw  47525  fmtnoprmfac1lem  47526  fmtnoprmfac1  47527  fmtnoprmfac2lem1  47528  fmtnoprmfac2  47529  fmtno4prm  47537  2pwp1prm  47551  139prmALT  47558  127prm  47561  sfprmdvdsmersenne  47565  lighneallem1  47567  lighneallem3  47569  proththdlem  47575  proththd  47576  iseven5  47626  oddprmALTV  47649  perfectALTVlem1  47683  perfectALTVlem2  47684  perfectALTV  47685  fppr2odd  47693  2exp340mod341  47695  341fppr2  47696  fpprel2  47703  nnsum3primes4  47750  nnsum3primesgbe  47754  evengpoap3  47761  nnsum4primesevenALTV  47763  bgoldbtbndlem1  47767  tgblthelfgott  47777  gpgusgralem  48008  gpg3nbgrvtx0  48026  gpg3kgrtriexlem2  48034  gpg3kgrtriexlem5  48037  gpg5grlic  48041  pw2m1lepw2m1  48444  nnpw2even  48457  logbpw2m1  48495  blenpw2  48506  nnpw2pmod  48511  blen2  48513  nnpw2p  48514  nnpw2pb  48515  blennnt2  48517  nnolog2flm1  48518  dig2nn1st  48533  0dig2pr01  48538  dig2nn0  48539  0dig2nn0e  48540  0dig2nn0o  48541  dig2bits  48542  dignn0flhalflem1  48543  dignn0ehalf  48545  dignn0flhalf  48546  nn0sumshdiglemA  48547  nn0sumshdiglemB  48548  nn0sumshdiglem1  48549  nn0sumshdiglem2  48550  nn0mullong  48553  itcovalt2lem2  48604  amgmw2d  49616