Theorem 2nn 12029

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 12019	. 2 ⊢ 2 = (1 + 1)
2		1nn 11967	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 11968	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2836	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2109  (class class class)co 7268  1c1 10856   + caddc 10858  ℕcn 11956  2c2 12011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7579  ax-1cn 10913

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-tr 5196  df-id 5488  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-pred 6199  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-ov 7271  df-om 7701  df-2nd 7818  df-frecs 8081  df-wrecs 8112  df-recs 8186  df-rdg 8225  df-nn 11957  df-2 12019

This theorem is referenced by:  3nn  12035  2nn0  12233  2z  12335  uz3m2nn  12613  ige2m1fz1  13327  sqeq0  13821  sqeq0d  13844  expmulnbnd  13931  faclbnd5  13993  bcn2  14014  f1oun2prg  14611  wrdl2exs2  14640  pfx2  14641  wwlktovf  14652  reusq0  15155  climcndslem1  15542  climcndslem2  15543  climcnds  15544  harmonic  15552  geo2sum  15566  geo2lim  15568  ege2le3  15780  ef01bndlem  15874  egt2lt3  15896  nthruc  15942  mod2eq0even  16036  bits0o  16118  bitsp1  16119  bitsfzolem  16122  bitsfzo  16123  bitsmod  16124  bitsfi  16125  bitscmp  16126  bitsinv1lem  16129  bitsinv1  16130  2ebits  16135  bitsinvp1  16137  sadcaddlem  16145  sadadd3  16149  sadaddlem  16154  sadasslem  16158  bitsres  16161  bitsuz  16162  bitsshft  16163  smumullem  16180  smumul  16181  sqgcd  16251  3lcm2e6woprm  16301  prm2orodd  16377  4nprm  16381  prmdvdssq  16404  isevengcd2  16415  3lcm2e6  16417  pythagtriplem4  16501  iserodd  16517  oddprmdvds  16585  prmreclem3  16600  prmreclem5  16602  prmreclem6  16603  4sqlem12  16638  vdwlem3  16665  vdwlem9  16671  vdwlem10  16672  prmo2  16722  dec2dvds  16745  dec5nprm  16748  dec2nprm  16749  2expltfac  16775  5prm  16791  6nprm  16792  7prm  16793  8nprm  16794  10nprm  16796  11prm  16797  17prm  16799  23prm  16801  37prm  16803  43prm  16804  83prm  16805  139prm  16806  163prm  16807  317prm  16808  631prm  16809  1259lem1  16813  1259lem2  16814  1259lem3  16815  1259lem4  16816  1259lem5  16817  1259prm  16818  2503lem1  16819  2503lem2  16820  2503lem3  16821  2503prm  16822  4001lem1  16823  4001lem2  16824  4001lem3  16825  4001lem4  16826  4001prm  16827  plusgndx  16969  plusgid  16970  plusgndxnn  16971  grpstr  16975  grpbaseOLD  16978  grpplusgOLD  16980  rngstr  16989  lmodstr  17016  topgrpstr  17052  dsndx  17076  dsid  17077  dsndxnn  17078  slotsdifdsndx  17085  slotsdifunifndx  17092  odrngstr  17094  imasvalstr  17143  pmtrprfvalrn  19077  psgnunilem2  19084  psgnprfval  19110  psgnprfval1  19111  mgpdsOLD  19715  oppraddOLD  19853  sraaddgOLD  20425  sradsOLD  20437  cnfldstr  20580  cnfldfunOLD  20591  zlmplusgOLD  20704  znaddOLD  20728  opsrplusgOLD  21236  m2detleiblem1  21754  m2detleiblem5  21755  m2detleiblem6  21756  m2detleiblem3  21759  m2detleiblem4  21760  m2detleib  21761  tmslemOLD  23619  tngplusgOLD  23782  ovollb2lem  24633  ovolunlem1a  24641  ovolunlem1  24642  ovoliunlem1  24647  ovoliunlem3  24649  dyadf  24736  dyadovol  24738  dyadss  24739  dyaddisjlem  24740  dyadmaxlem  24742  opnmbllem  24746  mbfi1fseqlem1  24861  mbfi1fseqlem3  24863  mbfi1fseqlem4  24864  mbfi1fseqlem5  24865  mbfi1fseqlem6  24866  dveflem  25124  aaliou3lem9  25491  quartlem1  25988  quartlem2  25989  zetacvg  26145  lgamgulmlem4  26162  basellem1  26211  basellem2  26212  basellem3  26213  basellem4  26214  basellem5  26215  basellem6  26216  basellem7  26217  basellem8  26218  basellem9  26219  1sgm2ppw  26329  ppiublem1  26331  chtublem  26340  mersenne  26356  perfect1  26357  perfectlem1  26358  perfectlem2  26359  perfect  26360  pcbcctr  26405  bclbnd  26409  bposlem1  26413  bposlem2  26414  bposlem3  26415  bposlem4  26416  bposlem5  26417  bposlem6  26418  bposlem8  26420  lgsdir2lem2  26455  lgsqr  26480  lgsqrmodndvds  26482  gausslemma2dlem1a  26494  gausslemma2d  26503  lgseisenlem1  26504  lgseisenlem2  26505  lgseisenlem3  26506  lgseisenlem4  26507  lgsquadlem1  26509  lgsquadlem2  26510  lgsquad2lem2  26514  2lgslem1c  26522  2lgs  26536  2sqlem3  26549  2sqlem8  26555  chebbnd1lem1  26598  chebbnd1lem3  26600  logdivsum  26662  log2sumbnd  26673  pntlemd  26723  pntlema  26725  pntlemb  26726  pntlemf  26734  pntlemo  26736  ostth2lem1  26747  slotsinbpsd  26783  slotslnbpsd  26784  trkgstr  26786  ttgplusgOLD  27224  ttgdsOLD  27229  axlowdimlem6  27296  eengstr  27329  usgrexmplef  27607  cusgrsizeindb0  27797  usgr2pthlem  28110  uspgrn2crct  28152  usgr2wspthons3  28308  clwwlkn2  28387  wwlksext2clwwlk  28400  eupth2lem3lem4  28574  frgrhash2wsp  28675  2clwwlk2clwwlk  28693  dlwwlknondlwlknonf1olem1  28707  clwlknon2num  28711  numclwlk2lem2f1o  28722  ex-xp  28779  ex-cnv  28780  ex-rn  28783  ex-mod  28792  resvplusgOLD  31514  lmat22e11  31747  lmat22e12  31748  lmat22e21  31749  lmat22e22  31750  lmat22det  31751  oddpwdc  32300  eulerpartlemt  32317  eulerpartlemgh  32324  fib0  32345  fib1  32346  fib3  32349  chtvalz  32588  hgt750lem  32610  hgt750lemb  32615  hgt750leme  32617  problem5  33606  bcprod  33683  opnmbllem0  35792  mblfinlem1  35793  dvasin  35840  areacirclem1  35844  heiborlem3  35950  heiborlem5  35952  heiborlem6  35953  heiborlem7  35954  heiborlem8  35955  heibor  35958  hlhilsplusOLD  39936  12gcd5e1  39991  420gcd8e4  39994  12lcm5e60  39996  60lcm7e420  39998  420lcm8e840  39999  lcm2un  40002  lcmineqlem19  40035  lcmineqlem20  40036  lcmineqlem22  40038  lcmineqlem23  40039  lcmineqlem  40040  3lexlogpow2ineq1  40046  3lexlogpow2ineq2  40047  aks4d1p1p6  40061  aks4d1p1p5  40063  dffltz  40451  flt4lem2  40464  flt4lem5  40467  flt4lem5a  40469  flt4lem5b  40470  flt4lem5c  40471  flt4lem5d  40472  flt4lem5e  40473  flt4lem7  40476  nna4b4nsq  40477  jm2.17a  40762  jm2.17b  40763  jm2.17c  40764  acongrep  40782  acongeq  40785  jm2.27a  40807  jm2.27c  40809  rmydioph  40816  rmxdioph  40818  expdiophlem2  40824  expdioph  40825  frlmpwfi  40903  amgm2d  41762  mnringaddgdOLD  41789  hashnzfz2  41892  lhe4.4ex1a  41900  limsup10exlem  43267  wallispilem5  43564  wallispi2lem1  43566  wallispi2  43568  stirlinglem3  43571  stirlinglem8  43576  stirlinglem10  43578  stirlinglem15  43583  dirkertrigeqlem3  43595  fouriersw  43726  hoicvrrex  44048  ovnsubaddlem1  44062  ovnsubaddlem2  44063  ovnsubadd2lem  44137  ovolval5lem1  44144  ovolval5lem2  44145  elmod2  44774  fmtnoodd  44937  fmtnof1  44939  fmtnosqrt  44943  fmtnorec4  44953  257prm  44965  odz2prm2pw  44967  fmtnoprmfac1lem  44968  fmtnoprmfac1  44969  fmtnoprmfac2lem1  44970  fmtnoprmfac2  44971  fmtno4prm  44979  2pwp1prm  44993  139prmALT  45000  127prm  45003  sfprmdvdsmersenne  45007  lighneallem1  45009  lighneallem3  45011  proththdlem  45017  proththd  45018  iseven5  45068  oddprmALTV  45091  perfectALTVlem1  45125  perfectALTVlem2  45126  perfectALTV  45127  fppr2odd  45135  2exp340mod341  45137  341fppr2  45138  fpprel2  45145  nnsum3primes4  45192  nnsum3primesgbe  45196  evengpoap3  45203  nnsum4primesevenALTV  45205  bgoldbtbndlem1  45209  tgblthelfgott  45219  pw2m1lepw2m1  45813  nnpw2even  45827  logbpw2m1  45865  blenpw2  45876  nnpw2pmod  45881  blen2  45883  nnpw2p  45884  nnpw2pb  45885  blennnt2  45887  nnolog2flm1  45888  dig2nn1st  45903  0dig2pr01  45908  dig2nn0  45909  0dig2nn0e  45910  0dig2nn0o  45911  dig2bits  45912  dignn0flhalflem1  45913  dignn0ehalf  45915  dignn0flhalf  45916  nn0sumshdiglemA  45917  nn0sumshdiglemB  45918  nn0sumshdiglem1  45919  nn0sumshdiglem2  45920  nn0mullong  45923  itcovalt2lem2  45974  amgmw2d  46460