Theorem 2nn 11456

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 11358	. 2 ⊢ 2 = (1 + 1)
2		1nn 11310	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 11311	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2877	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2155  (class class class)co 6868  1c1 10216   + caddc 10218  ℕcn 11299  2c2 11350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173  ax-1cn 10273

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-ral 3097  df-rex 3098  df-reu 3099  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-pss 3779  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-tp 4369  df-op 4371  df-uni 4624  df-iun 4707  df-br 4838  df-opab 4900  df-mpt 4917  df-tr 4940  df-id 5213  df-eprel 5218  df-po 5226  df-so 5227  df-fr 5264  df-we 5266  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-pred 5887  df-ord 5933  df-on 5934  df-lim 5935  df-suc 5936  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-ov 6871  df-om 7290  df-wrecs 7636  df-recs 7698  df-rdg 7736  df-nn 11300  df-2 11358

This theorem is referenced by:  3nn  11457  2nn0  11570  2z  11669  uz3m2nn  11943  ige2m1fz1  12646  sqeq0  13144  expmulnbnd  13213  sqeq0d  13224  faclbnd5  13299  bcn2  13320  f1oun2prg  13880  wrdl2exs2  13909  wwlktovf  13918  climcndslem1  14797  climcndslem2  14798  climcnds  14799  harmonic  14807  geo2sum  14820  geo2lim  14822  ege2le3  15034  ef01bndlem  15128  egt2lt3  15148  nthruc  15195  mod2eq0even  15284  bits0o  15365  bitsp1  15366  bitsfzolem  15369  bitsfzo  15370  bitsmod  15371  bitsfi  15372  bitscmp  15373  bitsinv1lem  15376  bitsinv1  15377  2ebits  15382  bitsinvp1  15384  sadcaddlem  15392  sadadd3  15396  sadaddlem  15401  sadasslem  15405  bitsres  15408  bitsuz  15409  bitsshft  15410  smumullem  15427  smumul  15428  sqgcd  15491  3lcm2e6woprm  15541  prm2orodd  15616  3prm  15618  4nprm  15619  isevengcd2  15649  3lcm2e6  15651  pythagtriplem4  15735  iserodd  15751  oddprmdvds  15818  prmreclem3  15833  prmreclem5  15835  prmreclem6  15836  4sqlem12  15871  vdwlem3  15898  vdwlem9  15904  vdwlem10  15905  prmo2  15955  dec2dvds  15978  dec5nprm  15981  dec2nprm  15982  2expltfac  16005  5prm  16021  6nprm  16022  7prm  16023  8nprm  16024  10nprm  16026  11prm  16027  17prm  16029  23prm  16031  37prm  16033  43prm  16034  83prm  16035  139prm  16036  163prm  16037  317prm  16038  631prm  16039  1259lem1  16043  1259lem2  16044  1259lem3  16045  1259lem4  16046  1259lem5  16047  1259prm  16048  2503lem1  16049  2503lem2  16050  2503lem3  16051  2503prm  16052  4001lem1  16053  4001lem2  16054  4001lem3  16055  4001lem4  16056  4001prm  16057  plusgndx  16181  plusgid  16182  grpstr  16195  grpbase  16196  grpplusg  16197  ressplusg  16198  rngstr  16205  lmodstr  16222  topgrpstr  16247  dsndx  16261  dsid  16262  odrngstr  16265  ressds  16272  imasvalstr  16311  pmtrprfvalrn  18103  psgnunilem2  18110  psgnprfval  18136  psgnprfval1  18137  mgpds  18695  oppradd  18826  sraaddg  19382  srads  19389  opsrplusg  19682  cnfldstr  19950  cnfldfun  19960  zlmplusg  20069  znadd  20090  m2detleiblem1  20635  m2detleiblem5  20636  m2detleiblem6  20637  m2detleiblem3  20640  m2detleiblem4  20641  m2detleib  20642  tmslem  22494  tngplusg  22653  ovollb2lem  23463  ovolunlem1a  23471  ovolunlem1  23472  ovoliunlem1  23477  ovoliunlem3  23479  dyadf  23566  dyadovol  23568  dyadss  23569  dyaddisjlem  23570  dyadmaxlem  23572  opnmbllem  23576  mbfi1fseqlem1  23690  mbfi1fseqlem3  23692  mbfi1fseqlem4  23693  mbfi1fseqlem5  23694  mbfi1fseqlem6  23695  dveflem  23950  aaliou3lem9  24313  dcubic1lem  24778  dcubic2  24779  mcubic  24782  quartlem1  24792  quartlem2  24793  zetacvg  24949  lgamgulmlem4  24966  basellem1  25015  basellem2  25016  basellem3  25017  basellem4  25018  basellem5  25019  basellem6  25020  basellem7  25021  basellem8  25022  basellem9  25023  1sgm2ppw  25133  ppiublem1  25135  chtublem  25144  mersenne  25160  perfect1  25161  perfectlem1  25162  perfectlem2  25163  perfect  25164  pcbcctr  25209  bclbnd  25213  bposlem1  25217  bposlem2  25218  bposlem3  25219  bposlem4  25220  bposlem5  25221  bposlem6  25222  bposlem8  25224  lgsdir2lem2  25259  lgsqr  25284  lgsqrmodndvds  25286  gausslemma2dlem1a  25298  gausslemma2d  25307  lgseisenlem1  25308  lgseisenlem2  25309  lgseisenlem3  25310  lgseisenlem4  25311  lgsquadlem1  25313  lgsquadlem2  25314  lgsquad2lem2  25318  2lgslem1c  25326  2lgs  25340  2sqlem3  25353  2sqlem8  25359  chebbnd1lem1  25366  chebbnd1lem3  25368  logdivsum  25430  log2sumbnd  25441  pntlemd  25491  pntlema  25493  pntlemb  25494  pntlemf  25502  pntlemo  25504  ostth2lem1  25515  trkgstr  25551  ttgplusg  25966  ttgds  25969  axlowdimlem6  26035  eengstr  26068  usgrexmplef  26361  cusgrsizeindb0  26567  usgr2pthlem  26881  uspgrn2crct  26923  usgr2wspthons3  27100  clwwlkn2  27187  wwlksext2clwwlk  27201  wwlksext2clwwlkOLD  27202  eupth2lem3lem4  27398  frgrhash2wsp  27501  2clwwlk2clwwlk  27521  dlwwlknonclwlknonf1olem1  27538  clwlknon2num  27542  numclwlk2lem2f1o  27553  numclwwlk2lem1OLD  27557  numclwlk2lem2fOLD  27558  numclwlk2lem2f1oOLD  27560  ex-xp  27618  ex-cnv  27619  ex-rn  27622  ex-mod  27631  resvplusg  30152  lmat22e11  30203  lmat22e12  30204  lmat22e21  30205  lmat22e22  30206  lmat22det  30207  oddpwdc  30735  eulerpartlemt  30752  eulerpartlemgh  30759  fib0  30780  fib1  30781  fib3  30784  chtvalz  31026  hgt750lem  31048  hgt750lemb  31053  hgt750leme  31055  problem5  31879  bcprod  31940  opnmbllem0  33752  mblfinlem1  33753  dvasin  33802  areacirclem1  33806  heiborlem3  33917  heiborlem5  33919  heiborlem6  33920  heiborlem7  33921  heiborlem8  33922  heibor  33925  hlhilsplus  37715  jm2.17a  38022  jm2.17b  38023  jm2.17c  38024  acongrep  38042  acongeq  38045  jm2.27a  38067  jm2.27c  38069  rmydioph  38076  rmxdioph  38078  expdiophlem2  38084  expdioph  38085  frlmpwfi  38163  amgm2d  38995  hashnzfz2  39014  lhe4.4ex1a  39022  limsup10exlem  40478  wallispilem5  40759  wallispi2lem1  40761  wallispi2  40763  stirlinglem3  40766  stirlinglem8  40771  stirlinglem10  40773  stirlinglem15  40778  dirkertrigeqlem3  40790  fouriersw  40921  hoicvrrex  41246  ovnsubaddlem1  41260  ovnsubaddlem2  41261  ovnsubadd2lem  41335  ovolval5lem1  41342  ovolval5lem2  41343  elmod2  41909  pfx2  41981  fmtnoodd  42014  fmtnof1  42016  fmtnosqrt  42020  fmtnorec4  42030  257prm  42042  odz2prm2pw  42044  fmtnoprmfac1lem  42045  fmtnoprmfac1  42046  fmtnoprmfac2lem1  42047  fmtnoprmfac2  42048  fmtno4prm  42056  2pwp1prm  42072  139prmALT  42080  127prm  42084  sfprmdvdsmersenne  42089  lighneallem1  42091  lighneallem3  42093  proththdlem  42099  proththd  42100  iseven5  42145  oddprmALTV  42167  perfectALTVlem1  42199  perfectALTVlem2  42200  perfectALTV  42201  nnsum3primes4  42245  nnsum3primesgbe  42249  evengpoap3  42256  nnsum4primesevenALTV  42258  bgoldbtbndlem1  42262  tgblthelfgott  42272  pw2m1lepw2m1  42872  nnpw2even  42885  logbpw2m1  42923  blenpw2  42934  nnpw2pmod  42939  blen2  42941  nnpw2p  42942  nnpw2pb  42943  blennnt2  42945  nnolog2flm1  42946  dig2nn1st  42961  0dig2pr01  42966  dig2nn0  42967  0dig2nn0e  42968  0dig2nn0o  42969  dig2bits  42970  dignn0flhalflem1  42971  dignn0ehalf  42973  dignn0flhalf  42974  nn0sumshdiglemA  42975  nn0sumshdiglemB  42976  nn0sumshdiglem1  42977  nn0sumshdiglem2  42978  nn0mullong  42981  amgmw2d  43115