Theorem 2nn 12315

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 12304	. 2 ⊢ 2 = (1 + 1)
2		1nn 12245	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12246	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2859	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2143  (class class class)co 7412  1c1 11102   + caddc 11104  ℕcn 12234  2c2 12296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406  ax-un 7734  ax-1cn 11159

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-nn 12235  df-2 12304

This theorem is referenced by:  3nn  12321  0le2  12344  2pos  12346  2ne0  12348  2nn0  12522  2z  12627  uz3m2nn  12919  ige2m1fz1  13646  sqeq0  14158  sqeq0d  14183  expmulnbnd  14273  faclbnd5  14336  bcn2  14357  f1oun2prg  14956  wrdl2exs2  14985  pfx2  14986  wwlktovf  14995  reusq0  15518  climcndslem1  15905  climcndslem2  15906  climcnds  15907  harmonic  15915  geo2sum  15929  geo2lim  15931  ege2le3  16145  ef01bndlem  16241  egt2lt3  16263  nthruc  16309  mod2eq0even  16405  bits0o  16489  bitsp1  16490  bitsfzolem  16493  bitsfzo  16494  bitsmod  16495  bitsfi  16496  bitscmp  16497  bitsinv1lem  16500  bitsinv1  16501  2ebits  16506  bitsinvp1  16508  sadcaddlem  16516  sadadd3  16520  sadaddlem  16525  sadasslem  16529  bitsres  16532  bitsuz  16533  bitsshft  16534  smumullem  16551  smumul  16552  sqgcd  16621  3lcm2e6woprm  16674  prm2orodd  16750  4nprm  16754  prmdvdssq  16778  isevengcd2  16790  3lcm2e6  16792  pythagtriplem4  16880  iserodd  16896  oddprmdvds  16964  prmreclem3  16979  prmreclem5  16981  prmreclem6  16982  4sqlem12  17017  vdwlem3  17044  vdwlem9  17050  vdwlem10  17051  prmo2  17101  dec2dvds  17124  dec5nprm  17127  dec2nprm  17128  2expltfac  17153  5prm  17169  6nprm  17170  7prm  17171  8nprm  17172  10nprmOLD  17175  11prm  17176  17prm  17178  23prm  17180  37prm  17182  43prm  17183  83prm  17184  139prm  17185  163prm  17186  317prm  17187  631prm  17188  1259lem1  17192  1259lem2  17193  1259lem3  17194  1259lem4  17195  1259lem5  17196  1259prm  17197  2503lem1  17198  2503lem2  17199  2503lem3  17200  2503prm  17201  4001lem1  17202  4001lem2  17203  4001lem3  17204  4001lem4  17205  4001prm  17206  plusgndx  17337  plusgid  17338  plusgndxnn  17339  rngstr  17352  lmodstr  17379  topgrpstr  17415  dsndx  17439  dsid  17440  dsndxnn  17441  slotsdifdsndx  17448  slotsdifunifndx  17455  odrngstr  17457  imasvalstr  17505  pmtrprfvalrn  19559  psgnunilem2  19566  psgnprfval  19592  psgnprfval1  19593  cnfldstr  21505  m2detleiblem1  22762  m2detleiblem5  22763  m2detleiblem6  22764  m2detleiblem3  22767  m2detleiblem4  22768  m2detleib  22769  ovollb2lem  25628  ovolunlem1a  25636  ovolunlem1  25637  ovoliunlem1  25642  ovoliunlem3  25644  dyadf  25731  dyadovol  25733  dyadss  25734  dyaddisjlem  25735  dyadmaxlem  25737  opnmbllem  25741  mbfi1fseqlem1  25855  mbfi1fseqlem3  25857  mbfi1fseqlem4  25858  mbfi1fseqlem5  25859  mbfi1fseqlem6  25860  dveflem  26119  aaliou3lem9  26494  quartlem1  27003  quartlem2  27004  zetacvg  27160  lgamgulmlem4  27177  basellem1  27226  basellem2  27227  basellem3  27228  basellem4  27229  basellem5  27230  basellem6  27231  basellem7  27232  basellem8  27233  basellem9  27234  1sgm2ppw  27345  ppiublem1  27347  chtublem  27356  mersenne  27372  perfect1  27373  perfectlem1  27374  perfectlem2  27375  perfect  27376  pcbcctr  27421  bclbnd  27425  bposlem1  27429  bposlem2  27430  bposlem3  27431  bposlem4  27432  bposlem5  27433  bposlem6  27434  bposlem8  27436  lgsdir2lem2  27471  lgsqr  27496  lgsqrmodndvds  27498  gausslemma2dlem1a  27510  gausslemma2d  27519  lgseisenlem1  27520  lgseisenlem2  27521  lgseisenlem3  27522  lgseisenlem4  27523  lgsquadlem1  27525  lgsquadlem2  27526  lgsquad2lem2  27530  2lgslem1c  27538  2lgs  27552  2sqlem3  27565  2sqlem8  27571  chebbnd1lem1  27614  chebbnd1lem3  27616  logdivsum  27678  log2sumbnd  27689  pntlemd  27739  pntlema  27741  pntlemb  27742  pntlemf  27750  pntlemo  27752  ostth2lem1  27763  slotsinbpsd  28691  slotslnbpsd  28692  trkgstr  28694  axlowdimlem6  29278  eengstr  29311  usgrexmplef  29590  cusgrsizeindb0  29780  usgr2pthlem  30093  uspgrn2crct  30138  usgr2wspthons3  30297  clwwlkn2  30376  wwlksext2clwwlk  30389  eupth2lem3lem4  30563  frgrhash2wsp  30664  2clwwlk2clwwlk  30682  dlwwlknondlwlknonf1olem1  30696  clwlknon2num  30700  numclwlk2lem2f1o  30711  ex-xp  30768  ex-cnv  30769  ex-rn  30772  ex-mod  30781  2exple2exp  33159  fldext2rspun  34053  cos9thpiminplylem1  34153  lmat22e11  34189  lmat22e12  34190  lmat22e21  34191  lmat22e22  34192  lmat22det  34193  oddpwdc  34725  eulerpartlemt  34742  eulerpartlemgh  34749  fib0  34770  fib1  34771  fib3  34774  chtvalz  34997  hgt750lem  35019  hgt750lemb  35024  hgt750leme  35026  problem5  36142  bcprod  36211  opnmbllem0  38288  mblfinlem1  38289  dvasin  38336  areacirclem1  38340  heiborlem3  38445  heiborlem5  38447  heiborlem6  38448  heiborlem7  38449  heiborlem8  38450  heibor  38453  12gcd5e1  42751  420gcd8e4  42754  12lcm5e60  42756  60lcm7e420  42758  420lcm8e840  42759  lcm2un  42762  lcmineqlem19  42795  lcmineqlem20  42796  lcmineqlem22  42798  lcmineqlem23  42799  lcmineqlem  42800  3lexlogpow2ineq1  42806  3lexlogpow2ineq2  42807  aks4d1p1p6  42821  aks4d1p1p5  42823  readvrec2  43103  dffltz  43349  flt4lem2  43362  flt4lem5  43365  flt4lem5a  43367  flt4lem5b  43368  flt4lem5c  43369  flt4lem5d  43370  flt4lem5e  43371  flt4lem7  43374  nna4b4nsq  43375  jm2.17a  43670  jm2.17b  43671  jm2.17c  43672  acongrep  43690  acongeq  43693  jm2.27a  43715  jm2.27c  43717  rmydioph  43724  rmxdioph  43726  expdiophlem2  43732  expdioph  43733  frlmpwfi  43808  amgm2d  44907  hashnzfz2  45014  lhe4.4ex1a  45022  limsup10exlem  46469  wallispilem5  46766  wallispi2lem1  46768  wallispi2  46770  stirlinglem3  46773  stirlinglem8  46778  stirlinglem10  46780  stirlinglem15  46785  dirkertrigeqlem3  46797  fouriersw  46928  hoicvrrex  47253  ovnsubaddlem1  47267  ovnsubaddlem2  47268  ovnsubadd2lem  47342  ovolval5lem1  47349  ovolval5lem2  47350  nthrucw  47590  ceilhalfelfzo1  48054  elmod2  48081  fmtnoodd  48268  fmtnof1  48270  fmtnosqrt  48274  fmtnorec4  48284  257prm  48296  odz2prm2pw  48298  fmtnoprmfac1lem  48299  fmtnoprmfac1  48300  fmtnoprmfac2lem1  48301  fmtnoprmfac2  48302  fmtno4prm  48310  2pwp1prm  48324  139prmALT  48331  127prm  48334  sfprmdvdsmersenne  48338  lighneallem1  48340  lighneallem3  48342  proththdlem  48348  proththd  48349  iseven5  48412  oddprmALTV  48435  perfectALTVlem1  48469  perfectALTVlem2  48470  perfectALTV  48471  fppr2odd  48479  2exp340mod341  48481  341fppr2  48482  fpprel2  48489  nnsum3primes4  48536  nnsum3primesgbe  48540  evengpoap3  48547  nnsum4primesevenALTV  48549  bgoldbtbndlem1  48553  tgblthelfgott  48563  gpgusgralem  48804  gpg3nbgrvtx0  48824  gpg3kgrtriexlem2  48832  gpg3kgrtriexlem5  48835  pw2m1lepw2m1  49283  nnpw2even  49292  logbpw2m1  49330  blenpw2  49341  nnpw2pmod  49346  blen2  49348  nnpw2p  49349  nnpw2pb  49350  blennnt2  49352  nnolog2flm1  49353  dig2nn1st  49368  0dig2pr01  49373  dig2nn0  49374  0dig2nn0e  49375  0dig2nn0o  49376  dig2bits  49377  dignn0flhalflem1  49378  dignn0ehalf  49380  dignn0flhalf  49381  nn0sumshdiglemA  49382  nn0sumshdiglemB  49383  nn0sumshdiglem1  49384  nn0sumshdiglem2  49385  nn0mullong  49388  itcovalt2lem2  49439  amgmw2d  50587