Theorem 2nn 11711

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 11701	. 2 ⊢ 2 = (1 + 1)
2		1nn 11649	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 11650	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2909	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2114  (class class class)co 7156  1c1 10538   + caddc 10540  ℕcn 11638  2c2 11693

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-1cn 10595

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-nn 11639  df-2 11701

This theorem is referenced by:  3nn  11717  2nn0  11915  2z  12015  uz3m2nn  12292  ige2m1fz1  12997  sqeq0  13487  sqeq0d  13510  expmulnbnd  13597  faclbnd5  13659  bcn2  13680  f1oun2prg  14279  wrdl2exs2  14308  pfx2  14309  wwlktovf  14320  reusq0  14822  climcndslem1  15204  climcndslem2  15205  climcnds  15206  harmonic  15214  geo2sum  15229  geo2lim  15231  ege2le3  15443  ef01bndlem  15537  egt2lt3  15559  nthruc  15605  mod2eq0even  15695  bits0o  15779  bitsp1  15780  bitsfzolem  15783  bitsfzo  15784  bitsmod  15785  bitsfi  15786  bitscmp  15787  bitsinv1lem  15790  bitsinv1  15791  2ebits  15796  bitsinvp1  15798  sadcaddlem  15806  sadadd3  15810  sadaddlem  15815  sadasslem  15819  bitsres  15822  bitsuz  15823  bitsshft  15824  smumullem  15841  smumul  15842  sqgcd  15909  3lcm2e6woprm  15959  prm2orodd  16035  4nprm  16039  isevengcd2  16070  3lcm2e6  16072  pythagtriplem4  16156  iserodd  16172  oddprmdvds  16239  prmreclem3  16254  prmreclem5  16256  prmreclem6  16257  4sqlem12  16292  vdwlem3  16319  vdwlem9  16325  vdwlem10  16326  prmo2  16376  dec2dvds  16399  dec5nprm  16402  dec2nprm  16403  2expltfac  16426  5prm  16442  6nprm  16443  7prm  16444  8nprm  16445  10nprm  16447  11prm  16448  17prm  16450  23prm  16452  37prm  16454  43prm  16455  83prm  16456  139prm  16457  163prm  16458  317prm  16459  631prm  16460  1259lem1  16464  1259lem2  16465  1259lem3  16466  1259lem4  16467  1259lem5  16468  1259prm  16469  2503lem1  16470  2503lem2  16471  2503lem3  16472  2503prm  16473  4001lem1  16474  4001lem2  16475  4001lem3  16476  4001lem4  16477  4001prm  16478  plusgndx  16595  plusgid  16596  grpstr  16609  grpbase  16610  grpplusg  16611  ressplusg  16612  rngstr  16619  lmodstr  16636  topgrpstr  16661  dsndx  16675  dsid  16676  odrngstr  16679  ressds  16686  imasvalstr  16725  pmtrprfvalrn  18616  psgnunilem2  18623  psgnprfval  18649  psgnprfval1  18650  mgpds  19249  oppradd  19380  sraaddg  19951  srads  19958  opsrplusg  20260  cnfldstr  20547  cnfldfun  20557  zlmplusg  20666  znadd  20687  m2detleiblem1  21233  m2detleiblem5  21234  m2detleiblem6  21235  m2detleiblem3  21238  m2detleiblem4  21239  m2detleib  21240  tmslem  23092  tngplusg  23251  ovollb2lem  24089  ovolunlem1a  24097  ovolunlem1  24098  ovoliunlem1  24103  ovoliunlem3  24105  dyadf  24192  dyadovol  24194  dyadss  24195  dyaddisjlem  24196  dyadmaxlem  24198  opnmbllem  24202  mbfi1fseqlem1  24316  mbfi1fseqlem3  24318  mbfi1fseqlem4  24319  mbfi1fseqlem5  24320  mbfi1fseqlem6  24321  dveflem  24576  aaliou3lem9  24939  quartlem1  25435  quartlem2  25436  zetacvg  25592  lgamgulmlem4  25609  basellem1  25658  basellem2  25659  basellem3  25660  basellem4  25661  basellem5  25662  basellem6  25663  basellem7  25664  basellem8  25665  basellem9  25666  1sgm2ppw  25776  ppiublem1  25778  chtublem  25787  mersenne  25803  perfect1  25804  perfectlem1  25805  perfectlem2  25806  perfect  25807  pcbcctr  25852  bclbnd  25856  bposlem1  25860  bposlem2  25861  bposlem3  25862  bposlem4  25863  bposlem5  25864  bposlem6  25865  bposlem8  25867  lgsdir2lem2  25902  lgsqr  25927  lgsqrmodndvds  25929  gausslemma2dlem1a  25941  gausslemma2d  25950  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem3  25953  lgseisenlem4  25954  lgsquadlem1  25956  lgsquadlem2  25957  lgsquad2lem2  25961  2lgslem1c  25969  2lgs  25983  2sqlem3  25996  2sqlem8  26002  chebbnd1lem1  26045  chebbnd1lem3  26047  logdivsum  26109  log2sumbnd  26120  pntlemd  26170  pntlema  26172  pntlemb  26173  pntlemf  26181  pntlemo  26183  ostth2lem1  26194  trkgstr  26230  ttgplusg  26664  ttgds  26667  axlowdimlem6  26733  eengstr  26766  usgrexmplef  27041  cusgrsizeindb0  27231  usgr2pthlem  27544  uspgrn2crct  27586  usgr2wspthons3  27743  clwwlkn2  27822  wwlksext2clwwlk  27836  eupth2lem3lem4  28010  frgrhash2wsp  28111  2clwwlk2clwwlk  28129  dlwwlknondlwlknonf1olem1  28143  clwlknon2num  28147  numclwlk2lem2f1o  28158  ex-xp  28215  ex-cnv  28216  ex-rn  28219  ex-mod  28228  resvplusg  30906  lmat22e11  31083  lmat22e12  31084  lmat22e21  31085  lmat22e22  31086  lmat22det  31087  oddpwdc  31612  eulerpartlemt  31629  eulerpartlemgh  31636  fib0  31657  fib1  31658  fib3  31661  chtvalz  31900  hgt750lem  31922  hgt750lemb  31927  hgt750leme  31929  problem5  32912  bcprod  32970  bj-endcomp  34601  opnmbllem0  34943  mblfinlem1  34944  dvasin  34993  areacirclem1  34997  heiborlem3  35106  heiborlem5  35108  heiborlem6  35109  heiborlem7  35110  heiborlem8  35111  heibor  35114  hlhilsplus  39091  12gcd5e1  39124  420gcd8e4  39127  12lcm5e60  39129  60lcm7e420  39131  420lcm8e840  39132  lcm2un  39135  dffltz  39320  jm2.17a  39606  jm2.17b  39607  jm2.17c  39608  acongrep  39626  acongeq  39629  jm2.27a  39651  jm2.27c  39653  rmydioph  39660  rmxdioph  39662  expdiophlem2  39668  expdioph  39669  frlmpwfi  39747  amgm2d  40600  hashnzfz2  40702  lhe4.4ex1a  40710  limsup10exlem  42102  wallispilem5  42403  wallispi2lem1  42405  wallispi2  42407  stirlinglem3  42410  stirlinglem8  42415  stirlinglem10  42417  stirlinglem15  42422  dirkertrigeqlem3  42434  fouriersw  42565  hoicvrrex  42887  ovnsubaddlem1  42901  ovnsubaddlem2  42902  ovnsubadd2lem  42976  ovolval5lem1  42983  ovolval5lem2  42984  elmod2  43579  fmtnoodd  43744  fmtnof1  43746  fmtnosqrt  43750  fmtnorec4  43760  257prm  43772  odz2prm2pw  43774  fmtnoprmfac1lem  43775  fmtnoprmfac1  43776  fmtnoprmfac2lem1  43777  fmtnoprmfac2  43778  fmtno4prm  43786  2pwp1prm  43800  139prmALT  43808  127prm  43812  sfprmdvdsmersenne  43817  lighneallem1  43819  lighneallem3  43821  proththdlem  43827  proththd  43828  iseven5  43878  oddprmALTV  43901  perfectALTVlem1  43935  perfectALTVlem2  43936  perfectALTV  43937  fppr2odd  43945  2exp340mod341  43947  341fppr2  43948  fpprel2  43955  nnsum3primes4  44002  nnsum3primesgbe  44006  evengpoap3  44013  nnsum4primesevenALTV  44015  bgoldbtbndlem1  44019  tgblthelfgott  44029  pw2m1lepw2m1  44624  nnpw2even  44638  logbpw2m1  44676  blenpw2  44687  nnpw2pmod  44692  blen2  44694  nnpw2p  44695  nnpw2pb  44696  blennnt2  44698  nnolog2flm1  44699  dig2nn1st  44714  0dig2pr01  44719  dig2nn0  44720  0dig2nn0e  44721  0dig2nn0o  44722  dig2bits  44723  dignn0flhalflem1  44724  dignn0ehalf  44726  dignn0flhalf  44727  nn0sumshdiglemA  44728  nn0sumshdiglemB  44729  nn0sumshdiglem1  44730  nn0sumshdiglem2  44731  nn0mullong  44734  amgmw2d  44954