Theorem 2nn 11448

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 11438	. 2 ⊢ 2 = (1 + 1)
2		1nn 11387	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 11388	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2855	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2107  (class class class)co 6922  1c1 10273   + caddc 10275  ℕcn 11374  2c2 11430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-1cn 10330

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-ov 6925  df-om 7344  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-nn 11375  df-2 11438

This theorem is referenced by:  3nn  11454  2nn0  11661  2z  11761  uz3m2nn  12037  ige2m1fz1  12747  sqeq0  13245  expmulnbnd  13315  sqeq0d  13326  faclbnd5  13403  bcn2  13424  f1oun2prg  14068  wrdl2exs2  14097  pfx2  14098  wwlktovf  14108  climcndslem1  14985  climcndslem2  14986  climcnds  14987  harmonic  14995  geo2sum  15008  geo2lim  15010  ege2le3  15222  ef01bndlem  15316  egt2lt3  15338  nthruc  15385  mod2eq0even  15474  bits0o  15558  bitsp1  15559  bitsfzolem  15562  bitsfzo  15563  bitsmod  15564  bitsfi  15565  bitscmp  15566  bitsinv1lem  15569  bitsinv1  15570  2ebits  15575  bitsinvp1  15577  sadcaddlem  15585  sadadd3  15589  sadaddlem  15594  sadasslem  15598  bitsres  15601  bitsuz  15602  bitsshft  15603  smumullem  15620  smumul  15621  sqgcd  15684  3lcm2e6woprm  15734  prm2orodd  15809  4nprm  15812  isevengcd2  15842  3lcm2e6  15844  pythagtriplem4  15928  iserodd  15944  oddprmdvds  16011  prmreclem3  16026  prmreclem5  16028  prmreclem6  16029  4sqlem12  16064  vdwlem3  16091  vdwlem9  16097  vdwlem10  16098  prmo2  16148  dec2dvds  16171  dec5nprm  16174  dec2nprm  16175  2expltfac  16198  5prm  16214  6nprm  16215  7prm  16216  8nprm  16217  10nprm  16219  11prm  16220  17prm  16222  23prm  16224  37prm  16226  43prm  16227  83prm  16228  139prm  16229  163prm  16230  317prm  16231  631prm  16232  1259lem1  16236  1259lem2  16237  1259lem3  16238  1259lem4  16239  1259lem5  16240  1259prm  16241  2503lem1  16242  2503lem2  16243  2503lem3  16244  2503prm  16245  4001lem1  16246  4001lem2  16247  4001lem3  16248  4001lem4  16249  4001prm  16250  plusgndx  16368  plusgid  16369  grpstr  16382  grpbase  16383  grpplusg  16384  ressplusg  16385  rngstr  16392  lmodstr  16409  topgrpstr  16434  dsndx  16448  dsid  16449  odrngstr  16452  ressds  16459  imasvalstr  16498  pmtrprfvalrn  18291  psgnunilem2  18299  psgnprfval  18325  psgnprfval1  18326  mgpds  18886  oppradd  19017  sraaddg  19576  srads  19583  opsrplusg  19876  cnfldstr  20144  cnfldfun  20154  zlmplusg  20263  znadd  20284  m2detleiblem1  20835  m2detleiblem5  20836  m2detleiblem6  20837  m2detleiblem3  20840  m2detleiblem4  20841  m2detleib  20842  tmslem  22695  tngplusg  22854  ovollb2lem  23692  ovolunlem1a  23700  ovolunlem1  23701  ovoliunlem1  23706  ovoliunlem3  23708  dyadf  23795  dyadovol  23797  dyadss  23798  dyaddisjlem  23799  dyadmaxlem  23801  opnmbllem  23805  mbfi1fseqlem1  23919  mbfi1fseqlem3  23921  mbfi1fseqlem4  23922  mbfi1fseqlem5  23923  mbfi1fseqlem6  23924  dveflem  24179  aaliou3lem9  24542  dcubic1lem  25021  dcubic2  25022  mcubic  25025  quartlem1  25035  quartlem2  25036  zetacvg  25193  lgamgulmlem4  25210  basellem1  25259  basellem2  25260  basellem3  25261  basellem4  25262  basellem5  25263  basellem6  25264  basellem7  25265  basellem8  25266  basellem9  25267  1sgm2ppw  25377  ppiublem1  25379  chtublem  25388  mersenne  25404  perfect1  25405  perfectlem1  25406  perfectlem2  25407  perfect  25408  pcbcctr  25453  bclbnd  25457  bposlem1  25461  bposlem2  25462  bposlem3  25463  bposlem4  25464  bposlem5  25465  bposlem6  25466  bposlem8  25468  lgsdir2lem2  25503  lgsqr  25528  lgsqrmodndvds  25530  gausslemma2dlem1a  25542  gausslemma2d  25551  lgseisenlem1  25552  lgseisenlem2  25553  lgseisenlem3  25554  lgseisenlem4  25555  lgsquadlem1  25557  lgsquadlem2  25558  lgsquad2lem2  25562  2lgslem1c  25570  2lgs  25584  2sqlem3  25597  2sqlem8  25603  chebbnd1lem1  25610  chebbnd1lem3  25612  logdivsum  25674  log2sumbnd  25685  pntlemd  25735  pntlema  25737  pntlemb  25738  pntlemf  25746  pntlemo  25748  ostth2lem1  25759  trkgstr  25795  ttgplusg  26227  ttgds  26230  axlowdimlem6  26296  eengstr  26329  usgrexmplef  26606  cusgrsizeindb0  26797  usgr2pthlem  27115  uspgrn2crct  27157  usgr2wspthons3  27344  clwwlkn2  27434  wwlksext2clwwlk  27454  eupth2lem3lem4  27635  frgrhash2wsp  27740  2clwwlk2clwwlk  27761  2clwwlk2clwwlkOLD  27762  dlwwlknondlwlknonf1olem1  27789  dlwwlknonclwlknonf1olem1OLD  27790  clwlknon2num  27796  numclwlk2lem2f1o  27807  numclwlk2lem2f1oOLD  27810  ex-xp  27868  ex-cnv  27869  ex-rn  27872  ex-mod  27881  resvplusg  30395  lmat22e11  30482  lmat22e12  30483  lmat22e21  30484  lmat22e22  30485  lmat22det  30486  oddpwdc  31014  eulerpartlemt  31031  eulerpartlemgh  31038  fib0  31060  fib1  31061  fib3  31064  chtvalz  31309  hgt750lem  31331  hgt750lemb  31336  hgt750leme  31338  problem5  32160  bcprod  32218  opnmbllem0  34071  mblfinlem1  34072  dvasin  34121  areacirclem1  34125  heiborlem3  34236  heiborlem5  34238  heiborlem6  34239  heiborlem7  34240  heiborlem8  34241  heibor  34244  hlhilsplus  38094  dffltz  38213  jm2.17a  38486  jm2.17b  38487  jm2.17c  38488  acongrep  38506  acongeq  38509  jm2.27a  38531  jm2.27c  38533  rmydioph  38540  rmxdioph  38542  expdiophlem2  38548  expdioph  38549  frlmpwfi  38627  amgm2d  39457  hashnzfz2  39476  lhe4.4ex1a  39484  limsup10exlem  40912  wallispilem5  41213  wallispi2lem1  41215  wallispi2  41217  stirlinglem3  41220  stirlinglem8  41225  stirlinglem10  41227  stirlinglem15  41232  dirkertrigeqlem3  41244  fouriersw  41375  hoicvrrex  41697  ovnsubaddlem1  41711  ovnsubaddlem2  41712  ovnsubadd2lem  41786  ovolval5lem1  41793  ovolval5lem2  41794  elmod2  42372  fmtnoodd  42466  fmtnof1  42468  fmtnosqrt  42472  fmtnorec4  42482  257prm  42494  odz2prm2pw  42496  fmtnoprmfac1lem  42497  fmtnoprmfac1  42498  fmtnoprmfac2lem1  42499  fmtnoprmfac2  42500  fmtno4prm  42508  2pwp1prm  42524  139prmALT  42532  127prm  42536  sfprmdvdsmersenne  42541  lighneallem1  42543  lighneallem3  42545  proththdlem  42551  proththd  42552  iseven5  42601  oddprmALTV  42623  perfectALTVlem1  42655  perfectALTVlem2  42656  perfectALTV  42657  nnsum3primes4  42701  nnsum3primesgbe  42705  evengpoap3  42712  nnsum4primesevenALTV  42714  bgoldbtbndlem1  42718  tgblthelfgott  42728  pw2m1lepw2m1  43325  nnpw2even  43338  logbpw2m1  43376  blenpw2  43387  nnpw2pmod  43392  blen2  43394  nnpw2p  43395  nnpw2pb  43396  blennnt2  43398  nnolog2flm1  43399  dig2nn1st  43414  0dig2pr01  43419  dig2nn0  43420  0dig2nn0e  43421  0dig2nn0o  43422  dig2bits  43423  dignn0flhalflem1  43424  dignn0ehalf  43426  dignn0flhalf  43427  nn0sumshdiglemA  43428  nn0sumshdiglemB  43429  nn0sumshdiglem1  43430  nn0sumshdiglem2  43431  nn0mullong  43434  amgmw2d  43656