Theorem 2nn 12252

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

Syntax hints:   ∈ wcel 2119  (class class class)co 7363  1c1 11037   + caddc 11039  ℕcn 12172  2c2 12234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685  ax-1cn 11094

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7366  df-om 7814  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-nn 12173  df-2 12242

This theorem is referenced by:  3nn  12258  2ne0  12283  2nn0  12452  2z  12557  uz3m2nn  12842  ige2m1fz1  13568  sqeq0  14080  sqeq0d  14105  expmulnbnd  14195  faclbnd5  14258  bcn2  14279  f1oun2prg  14877  wrdl2exs2  14906  pfx2  14907  wwlktovf  14916  reusq0  15425  climcndslem1  15812  climcndslem2  15813  climcnds  15814  harmonic  15822  geo2sum  15836  geo2lim  15838  ege2le3  16053  ef01bndlem  16149  egt2lt3  16171  nthruc  16217  mod2eq0even  16313  bits0o  16397  bitsp1  16398  bitsfzolem  16401  bitsfzo  16402  bitsmod  16403  bitsfi  16404  bitscmp  16405  bitsinv1lem  16408  bitsinv1  16409  2ebits  16414  bitsinvp1  16416  sadcaddlem  16424  sadadd3  16428  sadaddlem  16433  sadasslem  16437  bitsres  16440  bitsuz  16441  bitsshft  16442  smumullem  16459  smumul  16460  sqgcd  16529  3lcm2e6woprm  16582  prm2orodd  16658  4nprm  16662  prmdvdssq  16686  isevengcd2  16698  3lcm2e6  16700  pythagtriplem4  16788  iserodd  16804  oddprmdvds  16872  prmreclem3  16887  prmreclem5  16889  prmreclem6  16890  4sqlem12  16925  vdwlem3  16952  vdwlem9  16958  vdwlem10  16959  prmo2  17009  dec2dvds  17032  dec5nprm  17035  dec2nprm  17036  2expltfac  17061  5prm  17077  6nprm  17078  7prm  17079  8nprm  17080  10nprm  17082  11prm  17083  17prm  17085  23prm  17087  37prm  17089  43prm  17090  83prm  17091  139prm  17092  163prm  17093  317prm  17094  631prm  17095  1259lem1  17099  1259lem2  17100  1259lem3  17101  1259lem4  17102  1259lem5  17103  1259prm  17104  2503lem1  17105  2503lem2  17106  2503lem3  17107  2503prm  17108  4001lem1  17109  4001lem2  17110  4001lem3  17111  4001lem4  17112  4001prm  17113  plusgndx  17244  plusgid  17245  plusgndxnn  17246  rngstr  17259  lmodstr  17286  topgrpstr  17322  dsndx  17346  dsid  17347  dsndxnn  17348  slotsdifdsndx  17355  slotsdifunifndx  17362  odrngstr  17364  imasvalstr  17412  pmtrprfvalrn  19461  psgnunilem2  19468  psgnprfval  19494  psgnprfval1  19495  cnfldstr  21356  m2detleiblem1  22614  m2detleiblem5  22615  m2detleiblem6  22616  m2detleiblem3  22619  m2detleiblem4  22620  m2detleib  22621  ovollb2lem  25480  ovolunlem1a  25488  ovolunlem1  25489  ovoliunlem1  25494  ovoliunlem3  25496  dyadf  25583  dyadovol  25585  dyadss  25586  dyaddisjlem  25587  dyadmaxlem  25589  opnmbllem  25593  mbfi1fseqlem1  25707  mbfi1fseqlem3  25709  mbfi1fseqlem4  25710  mbfi1fseqlem5  25711  mbfi1fseqlem6  25712  dveflem  25971  aaliou3lem9  26341  quartlem1  26846  quartlem2  26847  zetacvg  27003  lgamgulmlem4  27020  basellem1  27069  basellem2  27070  basellem3  27071  basellem4  27072  basellem5  27073  basellem6  27074  basellem7  27075  basellem8  27076  basellem9  27077  1sgm2ppw  27188  ppiublem1  27190  chtublem  27199  mersenne  27215  perfect1  27216  perfectlem1  27217  perfectlem2  27218  perfect  27219  pcbcctr  27264  bclbnd  27268  bposlem1  27272  bposlem2  27273  bposlem3  27274  bposlem4  27275  bposlem5  27276  bposlem6  27277  bposlem8  27279  lgsdir2lem2  27314  lgsqr  27339  lgsqrmodndvds  27341  gausslemma2dlem1a  27353  gausslemma2d  27362  lgseisenlem1  27363  lgseisenlem2  27364  lgseisenlem3  27365  lgseisenlem4  27366  lgsquadlem1  27368  lgsquadlem2  27369  lgsquad2lem2  27373  2lgslem1c  27381  2lgs  27395  2sqlem3  27408  2sqlem8  27414  chebbnd1lem1  27457  chebbnd1lem3  27459  logdivsum  27521  log2sumbnd  27532  pntlemd  27582  pntlema  27584  pntlemb  27585  pntlemf  27593  pntlemo  27595  ostth2lem1  27606  slotsinbpsd  28534  slotslnbpsd  28535  trkgstr  28537  axlowdimlem6  29041  eengstr  29074  usgrexmplef  29353  cusgrsizeindb0  29543  usgr2pthlem  29856  uspgrn2crct  29901  usgr2wspthons3  30060  clwwlkn2  30139  wwlksext2clwwlk  30152  eupth2lem3lem4  30326  frgrhash2wsp  30427  2clwwlk2clwwlk  30445  dlwwlknondlwlknonf1olem1  30459  clwlknon2num  30463  numclwlk2lem2f1o  30474  ex-xp  30531  ex-cnv  30532  ex-rn  30535  ex-mod  30544  2exple2exp  32944  fldext2rspun  33873  cos9thpiminplylem1  33973  lmat22e11  34009  lmat22e12  34010  lmat22e21  34011  lmat22e22  34012  lmat22det  34013  oddpwdc  34545  eulerpartlemt  34562  eulerpartlemgh  34569  fib0  34590  fib1  34591  fib3  34594  chtvalz  34820  hgt750lem  34842  hgt750lemb  34847  hgt750leme  34849  problem5  35904  bcprod  35973  opnmbllem0  38030  mblfinlem1  38031  dvasin  38078  areacirclem1  38082  heiborlem3  38187  heiborlem5  38189  heiborlem6  38190  heiborlem7  38191  heiborlem8  38192  heibor  38195  12gcd5e1  42495  420gcd8e4  42498  12lcm5e60  42500  60lcm7e420  42502  420lcm8e840  42503  lcm2un  42506  lcmineqlem19  42539  lcmineqlem20  42540  lcmineqlem22  42542  lcmineqlem23  42543  lcmineqlem  42544  3lexlogpow2ineq1  42550  3lexlogpow2ineq2  42551  aks4d1p1p6  42565  aks4d1p1p5  42567  readvrec2  42845  dffltz  43091  flt4lem2  43104  flt4lem5  43107  flt4lem5a  43109  flt4lem5b  43110  flt4lem5c  43111  flt4lem5d  43112  flt4lem5e  43113  flt4lem7  43116  nna4b4nsq  43117  jm2.17a  43412  jm2.17b  43413  jm2.17c  43414  acongrep  43432  acongeq  43435  jm2.27a  43457  jm2.27c  43459  rmydioph  43466  rmxdioph  43468  expdiophlem2  43474  expdioph  43475  frlmpwfi  43550  amgm2d  44649  hashnzfz2  44772  lhe4.4ex1a  44780  limsup10exlem  46222  wallispilem5  46519  wallispi2lem1  46521  wallispi2  46523  stirlinglem3  46526  stirlinglem8  46531  stirlinglem10  46533  stirlinglem15  46538  dirkertrigeqlem3  46550  fouriersw  46681  hoicvrrex  47006  ovnsubaddlem1  47020  ovnsubaddlem2  47021  ovnsubadd2lem  47095  ovolval5lem1  47102  ovolval5lem2  47103  nthrucw  47338  ceilhalfelfzo1  47804  elmod2  47831  fmtnoodd  48018  fmtnof1  48020  fmtnosqrt  48024  fmtnorec4  48034  257prm  48046  odz2prm2pw  48048  fmtnoprmfac1lem  48049  fmtnoprmfac1  48050  fmtnoprmfac2lem1  48051  fmtnoprmfac2  48052  fmtno4prm  48060  2pwp1prm  48074  139prmALT  48081  127prm  48084  sfprmdvdsmersenne  48088  lighneallem1  48090  lighneallem3  48092  proththdlem  48098  proththd  48099  iseven5  48162  oddprmALTV  48185  perfectALTVlem1  48219  perfectALTVlem2  48220  perfectALTV  48221  fppr2odd  48229  2exp340mod341  48231  341fppr2  48232  fpprel2  48239  nnsum3primes4  48286  nnsum3primesgbe  48290  evengpoap3  48297  nnsum4primesevenALTV  48299  bgoldbtbndlem1  48303  tgblthelfgott  48313  gpgusgralem  48554  gpg3nbgrvtx0  48574  gpg3kgrtriexlem2  48582  gpg3kgrtriexlem5  48585  pw2m1lepw2m1  49018  nnpw2even  49027  logbpw2m1  49065  blenpw2  49076  nnpw2pmod  49081  blen2  49083  nnpw2p  49084  nnpw2pb  49085  blennnt2  49087  nnolog2flm1  49088  dig2nn1st  49103  0dig2pr01  49108  dig2nn0  49109  0dig2nn0e  49110  0dig2nn0o  49111  dig2bits  49112  dignn0flhalflem1  49113  dignn0ehalf  49115  dignn0flhalf  49116  nn0sumshdiglemA  49117  nn0sumshdiglemB  49118  nn0sumshdiglem1  49119  nn0sumshdiglem2  49120  nn0mullong  49123  itcovalt2lem2  49174  amgmw2d  50301