Theorem 2nn 12420

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 12409	. 2 ⊢ 2 = (1 + 1)
2		1nn 12350	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12351	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2856	1 ⊢ 2 ∈ ℕ

This proof depends on syntax axioms:   ∈ wcel 2144  (class class class)co 7421  1c1 11205   + caddc 11207  ℕcn 12339  2c2 12401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7752  ax-1cn 11262

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7424  df-om 7879  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-nn 12340  df-2 12409

This theorem is used by:  3nn  12426  0le2  12449  2pos  12451  2ne0  12453  2nn0  12627  2z  12732  uz3m2nn  13025  ige2m1fz1  13754  sqeq0  14267  sqeq0d  14292  expmulnbnd  14383  faclbnd5  14446  bcn2  14467  f1oun2prg  15074  wrdl2exs2  15103  pfx2  15104  wwlktovf  15115  reusq0  15638  climcndslem1  16024  climcndslem2  16025  climcnds  16026  harmonic  16034  geo2sum  16048  geo2lim  16050  ege2le3  16262  ef01bndlem  16358  egt2lt3  16380  nthruc  16426  mod2eq0even  16522  bits0o  16606  bitsp1  16607  bitsfzolem  16610  bitsfzo  16611  bitsmod  16612  bitsfi  16613  bitscmp  16614  bitsinv1lem  16617  bitsinv1  16618  2ebits  16623  bitsinvp1  16625  sadcaddlem  16633  sadadd3  16637  sadaddlem  16642  sadasslem  16646  bitsres  16649  bitsuz  16650  bitsshft  16651  smumullem  16668  smumul  16669  sqgcd  16742  dvdssqnn  16747  3lcm2e6woprm  16796  prm2orodd  16872  4nprm  16876  prmdvdssq  16900  isevengcd2  16912  3lcm2e6  16914  pythagtriplem4  17003  iserodd  17019  oddprmdvds  17087  prmreclem3  17102  prmreclem5  17104  prmreclem6  17105  4sqlem12  17140  vdwlem3  17167  vdwlem9  17173  vdwlem10  17174  prmo2  17224  dec2dvds  17247  dec5nprm  17250  dec2nprm  17251  2expltfac  17276  5prm  17292  6nprm  17293  7prm  17294  8nprm  17295  10nprmOLD  17298  11prm  17299  17prm  17301  23prm  17303  37prm  17305  43prm  17306  83prm  17307  139prm  17308  163prm  17309  317prm  17310  631prm  17311  1259lem1  17315  1259lem2  17316  1259lem3  17317  1259lem4  17318  1259lem5  17319  1259prm  17320  2503lem1  17321  2503lem2  17322  2503lem3  17323  2503prm  17324  4001lem1  17325  4001lem2  17326  4001lem3  17327  4001lem4  17328  4001prm  17329  plusgndx  17460  plusgid  17461  plusgndxnn  17462  rngstr  17475  lmodstr  17502  topgrpstr  17538  dsndx  17562  dsid  17563  dsndxnn  17564  slotsdifdsndx  17571  slotsdifunifndx  17578  odrngstr  17580  imasvalstr  17628  pmtrprfvalrn  19708  psgnunilem2  19715  psgnprfval  19741  psgnprfval1  19742  cnfldstr  21686  m2detleiblem1  22945  m2detleiblem5  22946  m2detleiblem6  22947  m2detleiblem3  22950  m2detleiblem4  22951  m2detleib  22952  ovollb2lem  25815  ovolunlem1a  25823  ovolunlem1  25824  ovoliunlem1  25829  ovoliunlem3  25831  dyadf  25918  dyadovol  25920  dyadss  25921  dyaddisjlem  25922  dyadmaxlem  25924  opnmbllem  25928  mbfi1fseqlem1  26042  mbfi1fseqlem3  26044  mbfi1fseqlem4  26045  mbfi1fseqlem5  26046  mbfi1fseqlem6  26047  dveflem  26305  aaliou3lem9  26683  quartlem1  27191  quartlem2  27192  zetacvg  27348  lgamgulmlem4  27365  basellem1  27414  basellem2  27415  basellem3  27416  basellem4  27417  basellem5  27418  basellem6  27419  basellem7  27420  basellem8  27421  basellem9  27422  1sgm2ppw  27533  ppiublem1  27535  chtublem  27544  mersenne  27560  perfect1  27561  perfectlem1  27562  perfectlem2  27563  perfect  27564  pcbcctr  27609  bclbnd  27613  bposlem1  27617  bposlem2  27618  bposlem3  27619  bposlem4  27620  bposlem5  27621  bposlem6  27622  bposlem8  27624  lgsdir2lem2  27659  lgsqr  27684  lgsqrmodndvds  27686  gausslemma2dlem1a  27698  gausslemma2d  27707  lgseisenlem1  27708  lgseisenlem2  27709  lgseisenlem3  27710  lgseisenlem4  27711  lgsquadlem1  27713  lgsquadlem2  27714  lgsquad2lem2  27718  2lgslem1c  27726  2lgs  27740  2sqlem3  27753  2sqlem8  27759  chebbnd1lem1  27802  chebbnd1lem3  27804  logdivsum  27866  log2sumbnd  27877  pntlemd  27927  pntlema  27929  pntlemb  27930  pntlemf  27938  pntlemo  27940  ostth2lem1  27951  flt4lem5  27986  flt4lem5a  27988  flt4lem5b  27989  flt4lem5c  27990  flt4lem5d  27991  flt4lem5e  27992  flt4lem7  27995  slotsinbpsd  28909  slotslnbpsd  28910  trkgstr  28912  angmgmlem  29401  angmgmbas  29404  axlowdimlem6  29531  eengstr  29564  usgrexmplef  29846  cusgrsizeindb0  30036  usgr2pthlem  30355  uspgrn2crct  30403  usgr2wspthons3  30562  clwwlkn2  30641  wwlksext2clwwlk  30654  eupth2lem3lem4  30838  frgrhash2wsp  30939  2clwwlk2clwwlk  30957  dlwwlknondlwlknonf1olem1  30971  clwlknon2num  30975  numclwlk2lem2f1o  30986  ex-xp  31043  ex-cnv  31044  ex-rn  31047  ex-mod  31056  2exple2exp  33472  fldext2rspun  34361  cos9thpiminplylem1  34461  lmat22e11  34497  lmat22e12  34498  lmat22e21  34499  lmat22e22  34500  lmat22det  34501  oddpwdc  35033  eulerpartlemt  35050  eulerpartlemgh  35057  fib0  35078  fib1  35079  fib3  35082  chtvalz  35305  hgt750lem  35327  hgt750lemb  35332  hgt750leme  35334  problem5  36521  bcprod  36596  opnmbllem0  38668  mblfinlem1  38669  dvasin  38716  areacirclem1  38720  heiborlem3  38841  heiborlem5  38843  heiborlem6  38844  heiborlem7  38845  heiborlem8  38846  heibor  38849  12gcd5e1  43147  420gcd8e4  43150  12lcm5e60  43152  60lcm7e420  43154  420lcm8e840  43155  lcm2un  43158  lcmineqlem19  43191  lcmineqlem20  43192  lcmineqlem22  43194  lcmineqlem23  43195  lcmineqlem  43196  3lexlogpow2ineq1  43202  3lexlogpow2ineq2  43203  aks4d1p1p6  43217  aks4d1p1p5  43219  readvrec2  43506  dffltz  43764  jm2.17a  44061  jm2.17b  44062  jm2.17c  44063  acongrep  44081  acongeq  44084  jm2.27a  44106  jm2.27c  44108  rmydioph  44115  rmxdioph  44117  expdiophlem2  44123  expdioph  44124  frlmpwfi  44194  amgm2d  45292  hashnzfz2  45399  lhe4.4ex1a  45407  limsup10exlem  46876  wallispilem5  47173  wallispi2lem1  47175  wallispi2  47177  stirlinglem3  47180  stirlinglem8  47185  stirlinglem10  47187  stirlinglem15  47192  dirkertrigeqlem3  47204  fouriersw  47335  hoicvrrex  47660  ovnsubaddlem1  47674  ovnsubaddlem2  47675  ovnsubadd2lem  47749  ovolval5lem1  47756  ovolval5lem2  47757  numtowerdt  48010  ceilhalfelfzo1  48498  elmod2  48525  fmtnoodd  48712  fmtnof1  48714  fmtnosqrt  48718  fmtnorec4  48728  257prm  48740  odz2prm2pw  48742  fmtnoprmfac1lem  48743  fmtnoprmfac1  48744  fmtnoprmfac2lem1  48745  fmtnoprmfac2  48746  fmtno4prm  48754  2pwp1prm  48768  139prmALT  48775  127prm  48778  sfprmdvdsmersenne  48782  lighneallem1  48784  lighneallem3  48786  proththdlem  48792  proththd  48793  iseven5  48856  oddprmALTV  48879  perfectALTVlem1  48913  perfectALTVlem2  48914  perfectALTV  48915  fppr2odd  48923  2exp340mod341  48925  341fppr2  48926  fpprel2  48933  nnsum3primes4  48980  nnsum3primesgbe  48984  evengpoap3  48991  nnsum4primesevenALTV  48993  bgoldbtbndlem1  48997  tgblthelfgott  49007  gpgusgralem  49248  gpg3nbgrvtx0  49268  gpg3kgrtriexlem2  49276  gpg3kgrtriexlem5  49279  pw2m1lepw2m1  49726  nnpw2even  49735  logbpw2m1  49773  blenpw2  49784  nnpw2pmod  49789  blen2  49791  nnpw2p  49792  nnpw2pb  49793  blennnt2  49795  nnolog2flm1  49796  dig2nn1st  49811  0dig2pr01  49816  dig2nn0  49817  0dig2nn0e  49818  0dig2nn0o  49819  dig2bits  49820  dignn0flhalflem1  49821  dignn0ehalf  49823  dignn0flhalf  49824  nn0sumshdiglemA  49825  nn0sumshdiglemB  49826  nn0sumshdiglem1  49827  nn0sumshdiglem2  49828  nn0mullong  49831  itcovalt2lem2  49882  2elfz13  51113  veronesevrowd  51148  veroquadgsumlem  51152  amgmw2d  51158