Theorem 2nn 12235

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 12225	. 2 ⊢ 2 = (1 + 1)
2		1nn 12173	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12174	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2824	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  1c1 11045   + caddc 11047  ℕcn 12162  2c2 12217

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-1cn 11102

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-nn 12163  df-2 12225

This theorem is referenced by:  3nn  12241  2ne0  12266  2nn0  12435  2z  12541  uz3m2nn  12829  ige2m1fz1  13553  sqeq0  14061  sqeq0d  14086  expmulnbnd  14176  faclbnd5  14239  bcn2  14260  f1oun2prg  14859  wrdl2exs2  14888  pfx2  14889  wwlktovf  14898  reusq0  15407  climcndslem1  15791  climcndslem2  15792  climcnds  15793  harmonic  15801  geo2sum  15815  geo2lim  15817  ege2le3  16032  ef01bndlem  16128  egt2lt3  16150  nthruc  16196  mod2eq0even  16292  bits0o  16376  bitsp1  16377  bitsfzolem  16380  bitsfzo  16381  bitsmod  16382  bitsfi  16383  bitscmp  16384  bitsinv1lem  16387  bitsinv1  16388  2ebits  16393  bitsinvp1  16395  sadcaddlem  16403  sadadd3  16407  sadaddlem  16412  sadasslem  16416  bitsres  16419  bitsuz  16420  bitsshft  16421  smumullem  16438  smumul  16439  sqgcd  16508  3lcm2e6woprm  16561  prm2orodd  16637  4nprm  16641  prmdvdssq  16664  isevengcd2  16676  3lcm2e6  16678  pythagtriplem4  16766  iserodd  16782  oddprmdvds  16850  prmreclem3  16865  prmreclem5  16867  prmreclem6  16868  4sqlem12  16903  vdwlem3  16930  vdwlem9  16936  vdwlem10  16937  prmo2  16987  dec2dvds  17010  dec5nprm  17013  dec2nprm  17014  2expltfac  17039  5prm  17055  6nprm  17056  7prm  17057  8nprm  17058  10nprm  17060  11prm  17061  17prm  17063  23prm  17065  37prm  17067  43prm  17068  83prm  17069  139prm  17070  163prm  17071  317prm  17072  631prm  17073  1259lem1  17077  1259lem2  17078  1259lem3  17079  1259lem4  17080  1259lem5  17081  1259prm  17082  2503lem1  17083  2503lem2  17084  2503lem3  17085  2503prm  17086  4001lem1  17087  4001lem2  17088  4001lem3  17089  4001lem4  17090  4001prm  17091  plusgndx  17222  plusgid  17223  plusgndxnn  17224  rngstr  17237  lmodstr  17264  topgrpstr  17300  dsndx  17324  dsid  17325  dsndxnn  17326  slotsdifdsndx  17333  slotsdifunifndx  17340  odrngstr  17342  imasvalstr  17390  pmtrprfvalrn  19394  psgnunilem2  19401  psgnprfval  19427  psgnprfval1  19428  cnfldstr  21242  cnfldstrOLD  21257  m2detleiblem1  22487  m2detleiblem5  22488  m2detleiblem6  22489  m2detleiblem3  22492  m2detleiblem4  22493  m2detleib  22494  ovollb2lem  25365  ovolunlem1a  25373  ovolunlem1  25374  ovoliunlem1  25379  ovoliunlem3  25381  dyadf  25468  dyadovol  25470  dyadss  25471  dyaddisjlem  25472  dyadmaxlem  25474  opnmbllem  25478  mbfi1fseqlem1  25592  mbfi1fseqlem3  25594  mbfi1fseqlem4  25595  mbfi1fseqlem5  25596  mbfi1fseqlem6  25597  dveflem  25859  aaliou3lem9  26234  quartlem1  26743  quartlem2  26744  zetacvg  26901  lgamgulmlem4  26918  basellem1  26967  basellem2  26968  basellem3  26969  basellem4  26970  basellem5  26971  basellem6  26972  basellem7  26973  basellem8  26974  basellem9  26975  1sgm2ppw  27087  ppiublem1  27089  chtublem  27098  mersenne  27114  perfect1  27115  perfectlem1  27116  perfectlem2  27117  perfect  27118  pcbcctr  27163  bclbnd  27167  bposlem1  27171  bposlem2  27172  bposlem3  27173  bposlem4  27174  bposlem5  27175  bposlem6  27176  bposlem8  27178  lgsdir2lem2  27213  lgsqr  27238  lgsqrmodndvds  27240  gausslemma2dlem1a  27252  gausslemma2d  27261  lgseisenlem1  27262  lgseisenlem2  27263  lgseisenlem3  27264  lgseisenlem4  27265  lgsquadlem1  27267  lgsquadlem2  27268  lgsquad2lem2  27272  2lgslem1c  27280  2lgs  27294  2sqlem3  27307  2sqlem8  27313  chebbnd1lem1  27356  chebbnd1lem3  27358  logdivsum  27420  log2sumbnd  27431  pntlemd  27481  pntlema  27483  pntlemb  27484  pntlemf  27492  pntlemo  27494  ostth2lem1  27505  slotsinbpsd  28344  slotslnbpsd  28345  trkgstr  28347  axlowdimlem6  28850  eengstr  28883  usgrexmplef  29162  cusgrsizeindb0  29353  usgr2pthlem  29666  uspgrn2crct  29711  usgr2wspthons3  29867  clwwlkn2  29946  wwlksext2clwwlk  29959  eupth2lem3lem4  30133  frgrhash2wsp  30234  2clwwlk2clwwlk  30252  dlwwlknondlwlknonf1olem1  30266  clwlknon2num  30270  numclwlk2lem2f1o  30281  ex-xp  30338  ex-cnv  30339  ex-rn  30342  ex-mod  30351  2exple2exp  32743  fldext2rspun  33650  cos9thpiminplylem1  33745  lmat22e11  33781  lmat22e12  33782  lmat22e21  33783  lmat22e22  33784  lmat22det  33785  oddpwdc  34318  eulerpartlemt  34335  eulerpartlemgh  34342  fib0  34363  fib1  34364  fib3  34367  chtvalz  34593  hgt750lem  34615  hgt750lemb  34620  hgt750leme  34622  problem5  35629  bcprod  35698  opnmbllem0  37623  mblfinlem1  37624  dvasin  37671  areacirclem1  37675  heiborlem3  37780  heiborlem5  37782  heiborlem6  37783  heiborlem7  37784  heiborlem8  37785  heibor  37788  12gcd5e1  41964  420gcd8e4  41967  12lcm5e60  41969  60lcm7e420  41971  420lcm8e840  41972  lcm2un  41975  lcmineqlem19  42008  lcmineqlem20  42009  lcmineqlem22  42011  lcmineqlem23  42012  lcmineqlem  42013  3lexlogpow2ineq1  42019  3lexlogpow2ineq2  42020  aks4d1p1p6  42034  aks4d1p1p5  42036  readvrec2  42322  dffltz  42595  flt4lem2  42608  flt4lem5  42611  flt4lem5a  42613  flt4lem5b  42614  flt4lem5c  42615  flt4lem5d  42616  flt4lem5e  42617  flt4lem7  42620  nna4b4nsq  42621  jm2.17a  42922  jm2.17b  42923  jm2.17c  42924  acongrep  42942  acongeq  42945  jm2.27a  42967  jm2.27c  42969  rmydioph  42976  rmxdioph  42978  expdiophlem2  42984  expdioph  42985  frlmpwfi  43060  amgm2d  44160  hashnzfz2  44283  lhe4.4ex1a  44291  limsup10exlem  45743  wallispilem5  46040  wallispi2lem1  46042  wallispi2  46044  stirlinglem3  46047  stirlinglem8  46052  stirlinglem10  46054  stirlinglem15  46059  dirkertrigeqlem3  46071  fouriersw  46202  hoicvrrex  46527  ovnsubaddlem1  46541  ovnsubaddlem2  46542  ovnsubadd2lem  46616  ovolval5lem1  46623  ovolval5lem2  46624  ceilhalfelfzo1  47304  elmod2  47329  fmtnoodd  47507  fmtnof1  47509  fmtnosqrt  47513  fmtnorec4  47523  257prm  47535  odz2prm2pw  47537  fmtnoprmfac1lem  47538  fmtnoprmfac1  47539  fmtnoprmfac2lem1  47540  fmtnoprmfac2  47541  fmtno4prm  47549  2pwp1prm  47563  139prmALT  47570  127prm  47573  sfprmdvdsmersenne  47577  lighneallem1  47579  lighneallem3  47581  proththdlem  47587  proththd  47588  iseven5  47638  oddprmALTV  47661  perfectALTVlem1  47695  perfectALTVlem2  47696  perfectALTV  47697  fppr2odd  47705  2exp340mod341  47707  341fppr2  47708  fpprel2  47715  nnsum3primes4  47762  nnsum3primesgbe  47766  evengpoap3  47773  nnsum4primesevenALTV  47775  bgoldbtbndlem1  47779  tgblthelfgott  47789  gpgusgralem  48020  gpg3nbgrvtx0  48040  gpg3kgrtriexlem2  48048  gpg3kgrtriexlem5  48051  pw2m1lepw2m1  48482  nnpw2even  48491  logbpw2m1  48529  blenpw2  48540  nnpw2pmod  48545  blen2  48547  nnpw2p  48548  nnpw2pb  48549  blennnt2  48551  nnolog2flm1  48552  dig2nn1st  48567  0dig2pr01  48572  dig2nn0  48573  0dig2nn0e  48574  0dig2nn0o  48575  dig2bits  48576  dignn0flhalflem1  48577  dignn0ehalf  48579  dignn0flhalf  48580  nn0sumshdiglemA  48581  nn0sumshdiglemB  48582  nn0sumshdiglem1  48583  nn0sumshdiglem2  48584  nn0mullong  48587  itcovalt2lem2  48638  amgmw2d  49766