Theorem 2nn 12198

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 12188	. 2 ⊢ 2 = (1 + 1)
2		1nn 12136	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12137	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2827	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2111  (class class class)co 7346  1c1 11007   + caddc 11009  ℕcn 12125  2c2 12180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668  ax-1cn 11064

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-nn 12126  df-2 12188

This theorem is referenced by:  3nn  12204  2ne0  12229  2nn0  12398  2z  12504  uz3m2nn  12792  ige2m1fz1  13516  sqeq0  14027  sqeq0d  14052  expmulnbnd  14142  faclbnd5  14205  bcn2  14226  f1oun2prg  14824  wrdl2exs2  14853  pfx2  14854  wwlktovf  14863  reusq0  15372  climcndslem1  15756  climcndslem2  15757  climcnds  15758  harmonic  15766  geo2sum  15780  geo2lim  15782  ege2le3  15997  ef01bndlem  16093  egt2lt3  16115  nthruc  16161  mod2eq0even  16257  bits0o  16341  bitsp1  16342  bitsfzolem  16345  bitsfzo  16346  bitsmod  16347  bitsfi  16348  bitscmp  16349  bitsinv1lem  16352  bitsinv1  16353  2ebits  16358  bitsinvp1  16360  sadcaddlem  16368  sadadd3  16372  sadaddlem  16377  sadasslem  16381  bitsres  16384  bitsuz  16385  bitsshft  16386  smumullem  16403  smumul  16404  sqgcd  16473  3lcm2e6woprm  16526  prm2orodd  16602  4nprm  16606  prmdvdssq  16629  isevengcd2  16641  3lcm2e6  16643  pythagtriplem4  16731  iserodd  16747  oddprmdvds  16815  prmreclem3  16830  prmreclem5  16832  prmreclem6  16833  4sqlem12  16868  vdwlem3  16895  vdwlem9  16901  vdwlem10  16902  prmo2  16952  dec2dvds  16975  dec5nprm  16978  dec2nprm  16979  2expltfac  17004  5prm  17020  6nprm  17021  7prm  17022  8nprm  17023  10nprm  17025  11prm  17026  17prm  17028  23prm  17030  37prm  17032  43prm  17033  83prm  17034  139prm  17035  163prm  17036  317prm  17037  631prm  17038  1259lem1  17042  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  1259prm  17047  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  4001prm  17056  plusgndx  17187  plusgid  17188  plusgndxnn  17189  rngstr  17202  lmodstr  17229  topgrpstr  17265  dsndx  17289  dsid  17290  dsndxnn  17291  slotsdifdsndx  17298  slotsdifunifndx  17305  odrngstr  17307  imasvalstr  17355  pmtrprfvalrn  19401  psgnunilem2  19408  psgnprfval  19434  psgnprfval1  19435  cnfldstr  21294  cnfldstrOLD  21309  m2detleiblem1  22540  m2detleiblem5  22541  m2detleiblem6  22542  m2detleiblem3  22545  m2detleiblem4  22546  m2detleib  22547  ovollb2lem  25417  ovolunlem1a  25425  ovolunlem1  25426  ovoliunlem1  25431  ovoliunlem3  25433  dyadf  25520  dyadovol  25522  dyadss  25523  dyaddisjlem  25524  dyadmaxlem  25526  opnmbllem  25530  mbfi1fseqlem1  25644  mbfi1fseqlem3  25646  mbfi1fseqlem4  25647  mbfi1fseqlem5  25648  mbfi1fseqlem6  25649  dveflem  25911  aaliou3lem9  26286  quartlem1  26795  quartlem2  26796  zetacvg  26953  lgamgulmlem4  26970  basellem1  27019  basellem2  27020  basellem3  27021  basellem4  27022  basellem5  27023  basellem6  27024  basellem7  27025  basellem8  27026  basellem9  27027  1sgm2ppw  27139  ppiublem1  27141  chtublem  27150  mersenne  27166  perfect1  27167  perfectlem1  27168  perfectlem2  27169  perfect  27170  pcbcctr  27215  bclbnd  27219  bposlem1  27223  bposlem2  27224  bposlem3  27225  bposlem4  27226  bposlem5  27227  bposlem6  27228  bposlem8  27230  lgsdir2lem2  27265  lgsqr  27290  lgsqrmodndvds  27292  gausslemma2dlem1a  27304  gausslemma2d  27313  lgseisenlem1  27314  lgseisenlem2  27315  lgseisenlem3  27316  lgseisenlem4  27317  lgsquadlem1  27319  lgsquadlem2  27320  lgsquad2lem2  27324  2lgslem1c  27332  2lgs  27346  2sqlem3  27359  2sqlem8  27365  chebbnd1lem1  27408  chebbnd1lem3  27410  logdivsum  27472  log2sumbnd  27483  pntlemd  27533  pntlema  27535  pntlemb  27536  pntlemf  27544  pntlemo  27546  ostth2lem1  27557  slotsinbpsd  28420  slotslnbpsd  28421  trkgstr  28423  axlowdimlem6  28926  eengstr  28959  usgrexmplef  29238  cusgrsizeindb0  29429  usgr2pthlem  29742  uspgrn2crct  29787  usgr2wspthons3  29943  clwwlkn2  30022  wwlksext2clwwlk  30035  eupth2lem3lem4  30209  frgrhash2wsp  30310  2clwwlk2clwwlk  30328  dlwwlknondlwlknonf1olem1  30342  clwlknon2num  30346  numclwlk2lem2f1o  30357  ex-xp  30414  ex-cnv  30415  ex-rn  30418  ex-mod  30427  2exple2exp  32826  fldext2rspun  33693  cos9thpiminplylem1  33793  lmat22e11  33829  lmat22e12  33830  lmat22e21  33831  lmat22e22  33832  lmat22det  33833  oddpwdc  34365  eulerpartlemt  34382  eulerpartlemgh  34389  fib0  34410  fib1  34411  fib3  34414  chtvalz  34640  hgt750lem  34662  hgt750lemb  34667  hgt750leme  34669  problem5  35711  bcprod  35780  opnmbllem0  37702  mblfinlem1  37703  dvasin  37750  areacirclem1  37754  heiborlem3  37859  heiborlem5  37861  heiborlem6  37862  heiborlem7  37863  heiborlem8  37864  heibor  37867  12gcd5e1  42042  420gcd8e4  42045  12lcm5e60  42047  60lcm7e420  42049  420lcm8e840  42050  lcm2un  42053  lcmineqlem19  42086  lcmineqlem20  42087  lcmineqlem22  42089  lcmineqlem23  42090  lcmineqlem  42091  3lexlogpow2ineq1  42097  3lexlogpow2ineq2  42098  aks4d1p1p6  42112  aks4d1p1p5  42114  readvrec2  42400  dffltz  42673  flt4lem2  42686  flt4lem5  42689  flt4lem5a  42691  flt4lem5b  42692  flt4lem5c  42693  flt4lem5d  42694  flt4lem5e  42695  flt4lem7  42698  nna4b4nsq  42699  jm2.17a  42999  jm2.17b  43000  jm2.17c  43001  acongrep  43019  acongeq  43022  jm2.27a  43044  jm2.27c  43046  rmydioph  43053  rmxdioph  43055  expdiophlem2  43061  expdioph  43062  frlmpwfi  43137  amgm2d  44237  hashnzfz2  44360  lhe4.4ex1a  44368  limsup10exlem  45816  wallispilem5  46113  wallispi2lem1  46115  wallispi2  46117  stirlinglem3  46120  stirlinglem8  46125  stirlinglem10  46127  stirlinglem15  46132  dirkertrigeqlem3  46144  fouriersw  46275  hoicvrrex  46600  ovnsubaddlem1  46614  ovnsubaddlem2  46615  ovnsubadd2lem  46689  ovolval5lem1  46696  ovolval5lem2  46697  ceilhalfelfzo1  47367  elmod2  47392  fmtnoodd  47570  fmtnof1  47572  fmtnosqrt  47576  fmtnorec4  47586  257prm  47598  odz2prm2pw  47600  fmtnoprmfac1lem  47601  fmtnoprmfac1  47602  fmtnoprmfac2lem1  47603  fmtnoprmfac2  47604  fmtno4prm  47612  2pwp1prm  47626  139prmALT  47633  127prm  47636  sfprmdvdsmersenne  47640  lighneallem1  47642  lighneallem3  47644  proththdlem  47650  proththd  47651  iseven5  47701  oddprmALTV  47724  perfectALTVlem1  47758  perfectALTVlem2  47759  perfectALTV  47760  fppr2odd  47768  2exp340mod341  47770  341fppr2  47771  fpprel2  47778  nnsum3primes4  47825  nnsum3primesgbe  47829  evengpoap3  47836  nnsum4primesevenALTV  47838  bgoldbtbndlem1  47842  tgblthelfgott  47852  gpgusgralem  48093  gpg3nbgrvtx0  48113  gpg3kgrtriexlem2  48121  gpg3kgrtriexlem5  48124  pw2m1lepw2m1  48558  nnpw2even  48567  logbpw2m1  48605  blenpw2  48616  nnpw2pmod  48621  blen2  48623  nnpw2p  48624  nnpw2pb  48625  blennnt2  48627  nnolog2flm1  48628  dig2nn1st  48643  0dig2pr01  48648  dig2nn0  48649  0dig2nn0e  48650  0dig2nn0o  48651  dig2bits  48652  dignn0flhalflem1  48653  dignn0ehalf  48655  dignn0flhalf  48656  nn0sumshdiglemA  48657  nn0sumshdiglemB  48658  nn0sumshdiglem1  48659  nn0sumshdiglem2  48660  nn0mullong  48663  itcovalt2lem2  48714  amgmw2d  49842