Theorem 2nn 12230

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 12220	. 2 ⊢ 2 = (1 + 1)
2		1nn 12168	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12169	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2833	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2114  (class class class)co 7368  1c1 11039   + caddc 11041  ℕcn 12157  2c2 12212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-1cn 11096

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-nn 12158  df-2 12220

This theorem is referenced by:  3nn  12236  2ne0  12261  2nn0  12430  2z  12535  uz3m2nn  12819  ige2m1fz1  13544  sqeq0  14055  sqeq0d  14080  expmulnbnd  14170  faclbnd5  14233  bcn2  14254  f1oun2prg  14852  wrdl2exs2  14881  pfx2  14882  wwlktovf  14891  reusq0  15400  climcndslem1  15784  climcndslem2  15785  climcnds  15786  harmonic  15794  geo2sum  15808  geo2lim  15810  ege2le3  16025  ef01bndlem  16121  egt2lt3  16143  nthruc  16189  mod2eq0even  16285  bits0o  16369  bitsp1  16370  bitsfzolem  16373  bitsfzo  16374  bitsmod  16375  bitsfi  16376  bitscmp  16377  bitsinv1lem  16380  bitsinv1  16381  2ebits  16386  bitsinvp1  16388  sadcaddlem  16396  sadadd3  16400  sadaddlem  16405  sadasslem  16409  bitsres  16412  bitsuz  16413  bitsshft  16414  smumullem  16431  smumul  16432  sqgcd  16501  3lcm2e6woprm  16554  prm2orodd  16630  4nprm  16634  prmdvdssq  16657  isevengcd2  16669  3lcm2e6  16671  pythagtriplem4  16759  iserodd  16775  oddprmdvds  16843  prmreclem3  16858  prmreclem5  16860  prmreclem6  16861  4sqlem12  16896  vdwlem3  16923  vdwlem9  16929  vdwlem10  16930  prmo2  16980  dec2dvds  17003  dec5nprm  17006  dec2nprm  17007  2expltfac  17032  5prm  17048  6nprm  17049  7prm  17050  8nprm  17051  10nprm  17053  11prm  17054  17prm  17056  23prm  17058  37prm  17060  43prm  17061  83prm  17062  139prm  17063  163prm  17064  317prm  17065  631prm  17066  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  1259prm  17075  2503lem1  17076  2503lem2  17077  2503lem3  17078  2503prm  17079  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  4001prm  17084  plusgndx  17215  plusgid  17216  plusgndxnn  17217  rngstr  17230  lmodstr  17257  topgrpstr  17293  dsndx  17317  dsid  17318  dsndxnn  17319  slotsdifdsndx  17326  slotsdifunifndx  17333  odrngstr  17335  imasvalstr  17383  pmtrprfvalrn  19429  psgnunilem2  19436  psgnprfval  19462  psgnprfval1  19463  cnfldstr  21323  cnfldstrOLD  21338  m2detleiblem1  22580  m2detleiblem5  22581  m2detleiblem6  22582  m2detleiblem3  22585  m2detleiblem4  22586  m2detleib  22587  ovollb2lem  25457  ovolunlem1a  25465  ovolunlem1  25466  ovoliunlem1  25471  ovoliunlem3  25473  dyadf  25560  dyadovol  25562  dyadss  25563  dyaddisjlem  25564  dyadmaxlem  25566  opnmbllem  25570  mbfi1fseqlem1  25684  mbfi1fseqlem3  25686  mbfi1fseqlem4  25687  mbfi1fseqlem5  25688  mbfi1fseqlem6  25689  dveflem  25951  aaliou3lem9  26326  quartlem1  26835  quartlem2  26836  zetacvg  26993  lgamgulmlem4  27010  basellem1  27059  basellem2  27060  basellem3  27061  basellem4  27062  basellem5  27063  basellem6  27064  basellem7  27065  basellem8  27066  basellem9  27067  1sgm2ppw  27179  ppiublem1  27181  chtublem  27190  mersenne  27206  perfect1  27207  perfectlem1  27208  perfectlem2  27209  perfect  27210  pcbcctr  27255  bclbnd  27259  bposlem1  27263  bposlem2  27264  bposlem3  27265  bposlem4  27266  bposlem5  27267  bposlem6  27268  bposlem8  27270  lgsdir2lem2  27305  lgsqr  27330  lgsqrmodndvds  27332  gausslemma2dlem1a  27344  gausslemma2d  27353  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem3  27356  lgseisenlem4  27357  lgsquadlem1  27359  lgsquadlem2  27360  lgsquad2lem2  27364  2lgslem1c  27372  2lgs  27386  2sqlem3  27399  2sqlem8  27405  chebbnd1lem1  27448  chebbnd1lem3  27450  logdivsum  27512  log2sumbnd  27523  pntlemd  27573  pntlema  27575  pntlemb  27576  pntlemf  27584  pntlemo  27586  ostth2lem1  27597  slotsinbpsd  28525  slotslnbpsd  28526  trkgstr  28528  axlowdimlem6  29032  eengstr  29065  usgrexmplef  29344  cusgrsizeindb0  29535  usgr2pthlem  29848  uspgrn2crct  29893  usgr2wspthons3  30052  clwwlkn2  30131  wwlksext2clwwlk  30144  eupth2lem3lem4  30318  frgrhash2wsp  30419  2clwwlk2clwwlk  30437  dlwwlknondlwlknonf1olem1  30451  clwlknon2num  30455  numclwlk2lem2f1o  30466  ex-xp  30523  ex-cnv  30524  ex-rn  30527  ex-mod  30536  2exple2exp  32936  fldext2rspun  33859  cos9thpiminplylem1  33959  lmat22e11  33995  lmat22e12  33996  lmat22e21  33997  lmat22e22  33998  lmat22det  33999  oddpwdc  34531  eulerpartlemt  34548  eulerpartlemgh  34555  fib0  34576  fib1  34577  fib3  34580  chtvalz  34806  hgt750lem  34828  hgt750lemb  34833  hgt750leme  34835  problem5  35882  bcprod  35951  opnmbllem0  37904  mblfinlem1  37905  dvasin  37952  areacirclem1  37956  heiborlem3  38061  heiborlem5  38063  heiborlem6  38064  heiborlem7  38065  heiborlem8  38066  heibor  38069  12gcd5e1  42370  420gcd8e4  42373  12lcm5e60  42375  60lcm7e420  42377  420lcm8e840  42378  lcm2un  42381  lcmineqlem19  42414  lcmineqlem20  42415  lcmineqlem22  42417  lcmineqlem23  42418  lcmineqlem  42419  3lexlogpow2ineq1  42425  3lexlogpow2ineq2  42426  aks4d1p1p6  42440  aks4d1p1p5  42442  readvrec2  42728  dffltz  42989  flt4lem2  43002  flt4lem5  43005  flt4lem5a  43007  flt4lem5b  43008  flt4lem5c  43009  flt4lem5d  43010  flt4lem5e  43011  flt4lem7  43014  nna4b4nsq  43015  jm2.17a  43314  jm2.17b  43315  jm2.17c  43316  acongrep  43334  acongeq  43337  jm2.27a  43359  jm2.27c  43361  rmydioph  43368  rmxdioph  43370  expdiophlem2  43376  expdioph  43377  frlmpwfi  43452  amgm2d  44551  hashnzfz2  44674  lhe4.4ex1a  44682  limsup10exlem  46127  wallispilem5  46424  wallispi2lem1  46426  wallispi2  46428  stirlinglem3  46431  stirlinglem8  46436  stirlinglem10  46438  stirlinglem15  46443  dirkertrigeqlem3  46455  fouriersw  46586  hoicvrrex  46911  ovnsubaddlem1  46925  ovnsubaddlem2  46926  ovnsubadd2lem  47000  ovolval5lem1  47007  ovolval5lem2  47008  nthrucw  47241  ceilhalfelfzo1  47687  elmod2  47712  fmtnoodd  47890  fmtnof1  47892  fmtnosqrt  47896  fmtnorec4  47906  257prm  47918  odz2prm2pw  47920  fmtnoprmfac1lem  47921  fmtnoprmfac1  47922  fmtnoprmfac2lem1  47923  fmtnoprmfac2  47924  fmtno4prm  47932  2pwp1prm  47946  139prmALT  47953  127prm  47956  sfprmdvdsmersenne  47960  lighneallem1  47962  lighneallem3  47964  proththdlem  47970  proththd  47971  iseven5  48021  oddprmALTV  48044  perfectALTVlem1  48078  perfectALTVlem2  48079  perfectALTV  48080  fppr2odd  48088  2exp340mod341  48090  341fppr2  48091  fpprel2  48098  nnsum3primes4  48145  nnsum3primesgbe  48149  evengpoap3  48156  nnsum4primesevenALTV  48158  bgoldbtbndlem1  48162  tgblthelfgott  48172  gpgusgralem  48413  gpg3nbgrvtx0  48433  gpg3kgrtriexlem2  48441  gpg3kgrtriexlem5  48444  pw2m1lepw2m1  48877  nnpw2even  48886  logbpw2m1  48924  blenpw2  48935  nnpw2pmod  48940  blen2  48942  nnpw2p  48943  nnpw2pb  48944  blennnt2  48946  nnolog2flm1  48947  dig2nn1st  48962  0dig2pr01  48967  dig2nn0  48968  0dig2nn0e  48969  0dig2nn0o  48970  dig2bits  48971  dignn0flhalflem1  48972  dignn0ehalf  48974  dignn0flhalf  48975  nn0sumshdiglemA  48976  nn0sumshdiglemB  48977  nn0sumshdiglem1  48978  nn0sumshdiglem2  48979  nn0mullong  48982  itcovalt2lem2  49033  amgmw2d  50160