Theorem 2nn 12336

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 12326	. 2 ⊢ 2 = (1 + 1)
2		1nn 12274	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12275	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2834	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2105  (class class class)co 7430  1c1 11153   + caddc 11155  ℕcn 12263  2c2 12318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753  ax-1cn 11210

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-nn 12264  df-2 12326

This theorem is referenced by:  3nn  12342  2nn0  12540  2z  12646  uz3m2nn  12930  ige2m1fz1  13652  sqeq0  14156  sqeq0d  14181  expmulnbnd  14270  faclbnd5  14333  bcn2  14354  f1oun2prg  14952  wrdl2exs2  14981  pfx2  14982  wwlktovf  14991  reusq0  15497  climcndslem1  15881  climcndslem2  15882  climcnds  15883  harmonic  15891  geo2sum  15905  geo2lim  15907  ege2le3  16122  ef01bndlem  16216  egt2lt3  16238  nthruc  16284  mod2eq0even  16379  bits0o  16463  bitsp1  16464  bitsfzolem  16467  bitsfzo  16468  bitsmod  16469  bitsfi  16470  bitscmp  16471  bitsinv1lem  16474  bitsinv1  16475  2ebits  16480  bitsinvp1  16482  sadcaddlem  16490  sadadd3  16494  sadaddlem  16499  sadasslem  16503  bitsres  16506  bitsuz  16507  bitsshft  16508  smumullem  16525  smumul  16526  sqgcd  16595  3lcm2e6woprm  16648  prm2orodd  16724  4nprm  16728  prmdvdssq  16751  isevengcd2  16763  3lcm2e6  16765  pythagtriplem4  16852  iserodd  16868  oddprmdvds  16936  prmreclem3  16951  prmreclem5  16953  prmreclem6  16954  4sqlem12  16989  vdwlem3  17016  vdwlem9  17022  vdwlem10  17023  prmo2  17073  dec2dvds  17096  dec5nprm  17099  dec2nprm  17100  2expltfac  17126  5prm  17142  6nprm  17143  7prm  17144  8nprm  17145  10nprm  17147  11prm  17148  17prm  17150  23prm  17152  37prm  17154  43prm  17155  83prm  17156  139prm  17157  163prm  17158  317prm  17159  631prm  17160  1259lem1  17164  1259lem2  17165  1259lem3  17166  1259lem4  17167  1259lem5  17168  1259prm  17169  2503lem1  17170  2503lem2  17171  2503lem3  17172  2503prm  17173  4001lem1  17174  4001lem2  17175  4001lem3  17176  4001lem4  17177  4001prm  17178  plusgndx  17323  plusgid  17324  plusgndxnn  17325  grpstr  17329  grpbaseOLD  17332  grpplusgOLD  17334  rngstr  17343  lmodstr  17370  topgrpstr  17406  dsndx  17430  dsid  17431  dsndxnn  17432  slotsdifdsndx  17439  slotsdifunifndx  17446  odrngstr  17448  imasvalstr  17497  pmtrprfvalrn  19520  psgnunilem2  19527  psgnprfval  19553  psgnprfval1  19554  mgpdsOLD  20165  oppraddOLD  20360  sraaddgOLD  21197  sradsOLD  21209  cnfldstr  21383  cnfldstrOLD  21398  cnfldfunALTOLDOLD  21410  zlmplusgOLD  21549  znaddOLD  21575  opsrplusgOLD  22089  m2detleiblem1  22645  m2detleiblem5  22646  m2detleiblem6  22647  m2detleiblem3  22650  m2detleiblem4  22651  m2detleib  22652  tmslemOLD  24510  tngplusgOLD  24673  ovollb2lem  25536  ovolunlem1a  25544  ovolunlem1  25545  ovoliunlem1  25550  ovoliunlem3  25552  dyadf  25639  dyadovol  25641  dyadss  25642  dyaddisjlem  25643  dyadmaxlem  25645  opnmbllem  25649  mbfi1fseqlem1  25764  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mbfi1fseqlem6  25769  dveflem  26031  aaliou3lem9  26406  quartlem1  26914  quartlem2  26915  zetacvg  27072  lgamgulmlem4  27089  basellem1  27138  basellem2  27139  basellem3  27140  basellem4  27141  basellem5  27142  basellem6  27143  basellem7  27144  basellem8  27145  basellem9  27146  1sgm2ppw  27258  ppiublem1  27260  chtublem  27269  mersenne  27285  perfect1  27286  perfectlem1  27287  perfectlem2  27288  perfect  27289  pcbcctr  27334  bclbnd  27338  bposlem1  27342  bposlem2  27343  bposlem3  27344  bposlem4  27345  bposlem5  27346  bposlem6  27347  bposlem8  27349  lgsdir2lem2  27384  lgsqr  27409  lgsqrmodndvds  27411  gausslemma2dlem1a  27423  gausslemma2d  27432  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem3  27435  lgseisenlem4  27436  lgsquadlem1  27438  lgsquadlem2  27439  lgsquad2lem2  27443  2lgslem1c  27451  2lgs  27465  2sqlem3  27478  2sqlem8  27484  chebbnd1lem1  27527  chebbnd1lem3  27529  logdivsum  27591  log2sumbnd  27602  pntlemd  27652  pntlema  27654  pntlemb  27655  pntlemf  27663  pntlemo  27665  ostth2lem1  27676  slotsinbpsd  28463  slotslnbpsd  28464  trkgstr  28466  ttgplusgOLD  28904  ttgdsOLD  28909  axlowdimlem6  28976  eengstr  29009  usgrexmplef  29290  cusgrsizeindb0  29481  usgr2pthlem  29795  uspgrn2crct  29837  usgr2wspthons3  29993  clwwlkn2  30072  wwlksext2clwwlk  30085  eupth2lem3lem4  30259  frgrhash2wsp  30360  2clwwlk2clwwlk  30378  dlwwlknondlwlknonf1olem1  30392  clwlknon2num  30396  numclwlk2lem2f1o  30407  ex-xp  30464  ex-cnv  30465  ex-rn  30468  ex-mod  30477  resvplusgOLD  33341  lmat22e11  33778  lmat22e12  33779  lmat22e21  33780  lmat22e22  33781  lmat22det  33782  oddpwdc  34335  eulerpartlemt  34352  eulerpartlemgh  34359  fib0  34380  fib1  34381  fib3  34384  chtvalz  34622  hgt750lem  34644  hgt750lemb  34649  hgt750leme  34651  problem5  35653  bcprod  35717  opnmbllem0  37642  mblfinlem1  37643  dvasin  37690  areacirclem1  37694  heiborlem3  37799  heiborlem5  37801  heiborlem6  37802  heiborlem7  37803  heiborlem8  37804  heibor  37807  hlhilsplusOLD  41925  12gcd5e1  41984  420gcd8e4  41987  12lcm5e60  41989  60lcm7e420  41991  420lcm8e840  41992  lcm2un  41995  lcmineqlem19  42028  lcmineqlem20  42029  lcmineqlem22  42031  lcmineqlem23  42032  lcmineqlem  42033  3lexlogpow2ineq1  42039  3lexlogpow2ineq2  42040  aks4d1p1p6  42054  aks4d1p1p5  42056  readvrec2  42369  dffltz  42620  flt4lem2  42633  flt4lem5  42636  flt4lem5a  42638  flt4lem5b  42639  flt4lem5c  42640  flt4lem5d  42641  flt4lem5e  42642  flt4lem7  42645  nna4b4nsq  42646  jm2.17a  42948  jm2.17b  42949  jm2.17c  42950  acongrep  42968  acongeq  42971  jm2.27a  42993  jm2.27c  42995  rmydioph  43002  rmxdioph  43004  expdiophlem2  43010  expdioph  43011  frlmpwfi  43086  amgm2d  44187  mnringaddgdOLD  44213  hashnzfz2  44316  lhe4.4ex1a  44324  limsup10exlem  45727  wallispilem5  46024  wallispi2lem1  46026  wallispi2  46028  stirlinglem3  46031  stirlinglem8  46036  stirlinglem10  46038  stirlinglem15  46043  dirkertrigeqlem3  46055  fouriersw  46186  hoicvrrex  46511  ovnsubaddlem1  46525  ovnsubaddlem2  46526  ovnsubadd2lem  46600  ovolval5lem1  46607  ovolval5lem2  46608  elmod2  47294  fmtnoodd  47457  fmtnof1  47459  fmtnosqrt  47463  fmtnorec4  47473  257prm  47485  odz2prm2pw  47487  fmtnoprmfac1lem  47488  fmtnoprmfac1  47489  fmtnoprmfac2lem1  47490  fmtnoprmfac2  47491  fmtno4prm  47499  2pwp1prm  47513  139prmALT  47520  127prm  47523  sfprmdvdsmersenne  47527  lighneallem1  47529  lighneallem3  47531  proththdlem  47537  proththd  47538  iseven5  47588  oddprmALTV  47611  perfectALTVlem1  47645  perfectALTVlem2  47646  perfectALTV  47647  fppr2odd  47655  2exp340mod341  47657  341fppr2  47658  fpprel2  47665  nnsum3primes4  47712  nnsum3primesgbe  47716  evengpoap3  47723  nnsum4primesevenALTV  47725  bgoldbtbndlem1  47729  tgblthelfgott  47739  gpgusgralem  47945  ceilhalfelfzo1  47950  gpg3nbgrvtx0  47966  gpg5grlic  47974  pw2m1lepw2m1  48365  nnpw2even  48378  logbpw2m1  48416  blenpw2  48427  nnpw2pmod  48432  blen2  48434  nnpw2p  48435  nnpw2pb  48436  blennnt2  48438  nnolog2flm1  48439  dig2nn1st  48454  0dig2pr01  48459  dig2nn0  48460  0dig2nn0e  48461  0dig2nn0o  48462  dig2bits  48463  dignn0flhalflem1  48464  dignn0ehalf  48466  dignn0flhalf  48467  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  nn0sumshdiglem1  48470  nn0sumshdiglem2  48471  nn0mullong  48474  itcovalt2lem2  48525  amgmw2d  49034