Theorem 2nn 12266

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 12256	. 2 ⊢ 2 = (1 + 1)
2		1nn 12204	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12205	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2825	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2109  (class class class)co 7390  1c1 11076   + caddc 11078  ℕcn 12193  2c2 12248

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-nn 12194  df-2 12256

This theorem is referenced by:  3nn  12272  2ne0  12297  2nn0  12466  2z  12572  uz3m2nn  12860  ige2m1fz1  13584  sqeq0  14092  sqeq0d  14117  expmulnbnd  14207  faclbnd5  14270  bcn2  14291  f1oun2prg  14890  wrdl2exs2  14919  pfx2  14920  wwlktovf  14929  reusq0  15438  climcndslem1  15822  climcndslem2  15823  climcnds  15824  harmonic  15832  geo2sum  15846  geo2lim  15848  ege2le3  16063  ef01bndlem  16159  egt2lt3  16181  nthruc  16227  mod2eq0even  16323  bits0o  16407  bitsp1  16408  bitsfzolem  16411  bitsfzo  16412  bitsmod  16413  bitsfi  16414  bitscmp  16415  bitsinv1lem  16418  bitsinv1  16419  2ebits  16424  bitsinvp1  16426  sadcaddlem  16434  sadadd3  16438  sadaddlem  16443  sadasslem  16447  bitsres  16450  bitsuz  16451  bitsshft  16452  smumullem  16469  smumul  16470  sqgcd  16539  3lcm2e6woprm  16592  prm2orodd  16668  4nprm  16672  prmdvdssq  16695  isevengcd2  16707  3lcm2e6  16709  pythagtriplem4  16797  iserodd  16813  oddprmdvds  16881  prmreclem3  16896  prmreclem5  16898  prmreclem6  16899  4sqlem12  16934  vdwlem3  16961  vdwlem9  16967  vdwlem10  16968  prmo2  17018  dec2dvds  17041  dec5nprm  17044  dec2nprm  17045  2expltfac  17070  5prm  17086  6nprm  17087  7prm  17088  8nprm  17089  10nprm  17091  11prm  17092  17prm  17094  23prm  17096  37prm  17098  43prm  17099  83prm  17100  139prm  17101  163prm  17102  317prm  17103  631prm  17104  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  1259prm  17113  2503lem1  17114  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  4001prm  17122  plusgndx  17253  plusgid  17254  plusgndxnn  17255  rngstr  17268  lmodstr  17295  topgrpstr  17331  dsndx  17355  dsid  17356  dsndxnn  17357  slotsdifdsndx  17364  slotsdifunifndx  17371  odrngstr  17373  imasvalstr  17421  pmtrprfvalrn  19425  psgnunilem2  19432  psgnprfval  19458  psgnprfval1  19459  cnfldstr  21273  cnfldstrOLD  21288  m2detleiblem1  22518  m2detleiblem5  22519  m2detleiblem6  22520  m2detleiblem3  22523  m2detleiblem4  22524  m2detleib  22525  ovollb2lem  25396  ovolunlem1a  25404  ovolunlem1  25405  ovoliunlem1  25410  ovoliunlem3  25412  dyadf  25499  dyadovol  25501  dyadss  25502  dyaddisjlem  25503  dyadmaxlem  25505  opnmbllem  25509  mbfi1fseqlem1  25623  mbfi1fseqlem3  25625  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  mbfi1fseqlem6  25628  dveflem  25890  aaliou3lem9  26265  quartlem1  26774  quartlem2  26775  zetacvg  26932  lgamgulmlem4  26949  basellem1  26998  basellem2  26999  basellem3  27000  basellem4  27001  basellem5  27002  basellem6  27003  basellem7  27004  basellem8  27005  basellem9  27006  1sgm2ppw  27118  ppiublem1  27120  chtublem  27129  mersenne  27145  perfect1  27146  perfectlem1  27147  perfectlem2  27148  perfect  27149  pcbcctr  27194  bclbnd  27198  bposlem1  27202  bposlem2  27203  bposlem3  27204  bposlem4  27205  bposlem5  27206  bposlem6  27207  bposlem8  27209  lgsdir2lem2  27244  lgsqr  27269  lgsqrmodndvds  27271  gausslemma2dlem1a  27283  gausslemma2d  27292  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem3  27295  lgseisenlem4  27296  lgsquadlem1  27298  lgsquadlem2  27299  lgsquad2lem2  27303  2lgslem1c  27311  2lgs  27325  2sqlem3  27338  2sqlem8  27344  chebbnd1lem1  27387  chebbnd1lem3  27389  logdivsum  27451  log2sumbnd  27462  pntlemd  27512  pntlema  27514  pntlemb  27515  pntlemf  27523  pntlemo  27525  ostth2lem1  27536  slotsinbpsd  28375  slotslnbpsd  28376  trkgstr  28378  axlowdimlem6  28881  eengstr  28914  usgrexmplef  29193  cusgrsizeindb0  29384  usgr2pthlem  29700  uspgrn2crct  29745  usgr2wspthons3  29901  clwwlkn2  29980  wwlksext2clwwlk  29993  eupth2lem3lem4  30167  frgrhash2wsp  30268  2clwwlk2clwwlk  30286  dlwwlknondlwlknonf1olem1  30300  clwlknon2num  30304  numclwlk2lem2f1o  30315  ex-xp  30372  ex-cnv  30373  ex-rn  30376  ex-mod  30385  2exple2exp  32777  fldext2rspun  33684  cos9thpiminplylem1  33779  lmat22e11  33815  lmat22e12  33816  lmat22e21  33817  lmat22e22  33818  lmat22det  33819  oddpwdc  34352  eulerpartlemt  34369  eulerpartlemgh  34376  fib0  34397  fib1  34398  fib3  34401  chtvalz  34627  hgt750lem  34649  hgt750lemb  34654  hgt750leme  34656  problem5  35663  bcprod  35732  opnmbllem0  37657  mblfinlem1  37658  dvasin  37705  areacirclem1  37709  heiborlem3  37814  heiborlem5  37816  heiborlem6  37817  heiborlem7  37818  heiborlem8  37819  heibor  37822  12gcd5e1  41998  420gcd8e4  42001  12lcm5e60  42003  60lcm7e420  42005  420lcm8e840  42006  lcm2un  42009  lcmineqlem19  42042  lcmineqlem20  42043  lcmineqlem22  42045  lcmineqlem23  42046  lcmineqlem  42047  3lexlogpow2ineq1  42053  3lexlogpow2ineq2  42054  aks4d1p1p6  42068  aks4d1p1p5  42070  readvrec2  42356  dffltz  42629  flt4lem2  42642  flt4lem5  42645  flt4lem5a  42647  flt4lem5b  42648  flt4lem5c  42649  flt4lem5d  42650  flt4lem5e  42651  flt4lem7  42654  nna4b4nsq  42655  jm2.17a  42956  jm2.17b  42957  jm2.17c  42958  acongrep  42976  acongeq  42979  jm2.27a  43001  jm2.27c  43003  rmydioph  43010  rmxdioph  43012  expdiophlem2  43018  expdioph  43019  frlmpwfi  43094  amgm2d  44194  hashnzfz2  44317  lhe4.4ex1a  44325  limsup10exlem  45777  wallispilem5  46074  wallispi2lem1  46076  wallispi2  46078  stirlinglem3  46081  stirlinglem8  46086  stirlinglem10  46088  stirlinglem15  46093  dirkertrigeqlem3  46105  fouriersw  46236  hoicvrrex  46561  ovnsubaddlem1  46575  ovnsubaddlem2  46576  ovnsubadd2lem  46650  ovolval5lem1  46657  ovolval5lem2  46658  ceilhalfelfzo1  47335  elmod2  47360  fmtnoodd  47538  fmtnof1  47540  fmtnosqrt  47544  fmtnorec4  47554  257prm  47566  odz2prm2pw  47568  fmtnoprmfac1lem  47569  fmtnoprmfac1  47570  fmtnoprmfac2lem1  47571  fmtnoprmfac2  47572  fmtno4prm  47580  2pwp1prm  47594  139prmALT  47601  127prm  47604  sfprmdvdsmersenne  47608  lighneallem1  47610  lighneallem3  47612  proththdlem  47618  proththd  47619  iseven5  47669  oddprmALTV  47692  perfectALTVlem1  47726  perfectALTVlem2  47727  perfectALTV  47728  fppr2odd  47736  2exp340mod341  47738  341fppr2  47739  fpprel2  47746  nnsum3primes4  47793  nnsum3primesgbe  47797  evengpoap3  47804  nnsum4primesevenALTV  47806  bgoldbtbndlem1  47810  tgblthelfgott  47820  gpgusgralem  48051  gpg3nbgrvtx0  48071  gpg3kgrtriexlem2  48079  gpg3kgrtriexlem5  48082  pw2m1lepw2m1  48513  nnpw2even  48522  logbpw2m1  48560  blenpw2  48571  nnpw2pmod  48576  blen2  48578  nnpw2p  48579  nnpw2pb  48580  blennnt2  48582  nnolog2flm1  48583  dig2nn1st  48598  0dig2pr01  48603  dig2nn0  48604  0dig2nn0e  48605  0dig2nn0o  48606  dig2bits  48607  dignn0flhalflem1  48608  dignn0ehalf  48610  dignn0flhalf  48611  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613  nn0sumshdiglem1  48614  nn0sumshdiglem2  48615  nn0mullong  48618  itcovalt2lem2  48669  amgmw2d  49797