Theorem 2nn 12092

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 12082	. 2 ⊢ 2 = (1 + 1)
2		1nn 12030	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12031	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2833	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2104  (class class class)co 7307  1c1 10918   + caddc 10920  ℕcn 12019  2c2 12074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-un 7620  ax-1cn 10975

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-ov 7310  df-om 7745  df-2nd 7864  df-frecs 8128  df-wrecs 8159  df-recs 8233  df-rdg 8272  df-nn 12020  df-2 12082

This theorem is referenced by:  3nn  12098  2nn0  12296  2z  12398  uz3m2nn  12677  ige2m1fz1  13391  sqeq0  13886  sqeq0d  13909  expmulnbnd  13996  faclbnd5  14058  bcn2  14079  f1oun2prg  14675  wrdl2exs2  14704  pfx2  14705  wwlktovf  14716  reusq0  15219  climcndslem1  15606  climcndslem2  15607  climcnds  15608  harmonic  15616  geo2sum  15630  geo2lim  15632  ege2le3  15844  ef01bndlem  15938  egt2lt3  15960  nthruc  16006  mod2eq0even  16100  bits0o  16182  bitsp1  16183  bitsfzolem  16186  bitsfzo  16187  bitsmod  16188  bitsfi  16189  bitscmp  16190  bitsinv1lem  16193  bitsinv1  16194  2ebits  16199  bitsinvp1  16201  sadcaddlem  16209  sadadd3  16213  sadaddlem  16218  sadasslem  16222  bitsres  16225  bitsuz  16226  bitsshft  16227  smumullem  16244  smumul  16245  sqgcd  16315  3lcm2e6woprm  16365  prm2orodd  16441  4nprm  16445  prmdvdssq  16468  isevengcd2  16479  3lcm2e6  16481  pythagtriplem4  16565  iserodd  16581  oddprmdvds  16649  prmreclem3  16664  prmreclem5  16666  prmreclem6  16667  4sqlem12  16702  vdwlem3  16729  vdwlem9  16735  vdwlem10  16736  prmo2  16786  dec2dvds  16809  dec5nprm  16812  dec2nprm  16813  2expltfac  16839  5prm  16855  6nprm  16856  7prm  16857  8nprm  16858  10nprm  16860  11prm  16861  17prm  16863  23prm  16865  37prm  16867  43prm  16868  83prm  16869  139prm  16870  163prm  16871  317prm  16872  631prm  16873  1259lem1  16877  1259lem2  16878  1259lem3  16879  1259lem4  16880  1259lem5  16881  1259prm  16882  2503lem1  16883  2503lem2  16884  2503lem3  16885  2503prm  16886  4001lem1  16887  4001lem2  16888  4001lem3  16889  4001lem4  16890  4001prm  16891  plusgndx  17033  plusgid  17034  plusgndxnn  17035  grpstr  17039  grpbaseOLD  17042  grpplusgOLD  17044  rngstr  17053  lmodstr  17080  topgrpstr  17116  dsndx  17140  dsid  17141  dsndxnn  17142  slotsdifdsndx  17149  slotsdifunifndx  17156  odrngstr  17158  imasvalstr  17207  pmtrprfvalrn  19141  psgnunilem2  19148  psgnprfval  19174  psgnprfval1  19175  mgpdsOLD  19779  oppraddOLD  19917  sraaddgOLD  20489  sradsOLD  20501  cnfldstr  20644  cnfldfunALTOLD  20656  zlmplusgOLD  20768  znaddOLD  20792  opsrplusgOLD  21300  m2detleiblem1  21818  m2detleiblem5  21819  m2detleiblem6  21820  m2detleiblem3  21823  m2detleiblem4  21824  m2detleib  21825  tmslemOLD  23683  tngplusgOLD  23846  ovollb2lem  24697  ovolunlem1a  24705  ovolunlem1  24706  ovoliunlem1  24711  ovoliunlem3  24713  dyadf  24800  dyadovol  24802  dyadss  24803  dyaddisjlem  24804  dyadmaxlem  24806  opnmbllem  24810  mbfi1fseqlem1  24925  mbfi1fseqlem3  24927  mbfi1fseqlem4  24928  mbfi1fseqlem5  24929  mbfi1fseqlem6  24930  dveflem  25188  aaliou3lem9  25555  quartlem1  26052  quartlem2  26053  zetacvg  26209  lgamgulmlem4  26226  basellem1  26275  basellem2  26276  basellem3  26277  basellem4  26278  basellem5  26279  basellem6  26280  basellem7  26281  basellem8  26282  basellem9  26283  1sgm2ppw  26393  ppiublem1  26395  chtublem  26404  mersenne  26420  perfect1  26421  perfectlem1  26422  perfectlem2  26423  perfect  26424  pcbcctr  26469  bclbnd  26473  bposlem1  26477  bposlem2  26478  bposlem3  26479  bposlem4  26480  bposlem5  26481  bposlem6  26482  bposlem8  26484  lgsdir2lem2  26519  lgsqr  26544  lgsqrmodndvds  26546  gausslemma2dlem1a  26558  gausslemma2d  26567  lgseisenlem1  26568  lgseisenlem2  26569  lgseisenlem3  26570  lgseisenlem4  26571  lgsquadlem1  26573  lgsquadlem2  26574  lgsquad2lem2  26578  2lgslem1c  26586  2lgs  26600  2sqlem3  26613  2sqlem8  26619  chebbnd1lem1  26662  chebbnd1lem3  26664  logdivsum  26726  log2sumbnd  26737  pntlemd  26787  pntlema  26789  pntlemb  26790  pntlemf  26798  pntlemo  26800  ostth2lem1  26811  slotsinbpsd  26847  slotslnbpsd  26848  trkgstr  26850  ttgplusgOLD  27288  ttgdsOLD  27293  axlowdimlem6  27360  eengstr  27393  usgrexmplef  27671  cusgrsizeindb0  27861  usgr2pthlem  28176  uspgrn2crct  28218  usgr2wspthons3  28374  clwwlkn2  28453  wwlksext2clwwlk  28466  eupth2lem3lem4  28640  frgrhash2wsp  28741  2clwwlk2clwwlk  28759  dlwwlknondlwlknonf1olem1  28773  clwlknon2num  28777  numclwlk2lem2f1o  28788  ex-xp  28845  ex-cnv  28846  ex-rn  28849  ex-mod  28858  resvplusgOLD  31580  lmat22e11  31813  lmat22e12  31814  lmat22e21  31815  lmat22e22  31816  lmat22det  31817  oddpwdc  32366  eulerpartlemt  32383  eulerpartlemgh  32390  fib0  32411  fib1  32412  fib3  32415  chtvalz  32654  hgt750lem  32676  hgt750lemb  32681  hgt750leme  32683  problem5  33672  bcprod  33749  opnmbllem0  35857  mblfinlem1  35858  dvasin  35905  areacirclem1  35909  heiborlem3  36015  heiborlem5  36017  heiborlem6  36018  heiborlem7  36019  heiborlem8  36020  heibor  36023  hlhilsplusOLD  39999  12gcd5e1  40053  420gcd8e4  40056  12lcm5e60  40058  60lcm7e420  40060  420lcm8e840  40061  lcm2un  40064  lcmineqlem19  40097  lcmineqlem20  40098  lcmineqlem22  40100  lcmineqlem23  40101  lcmineqlem  40102  3lexlogpow2ineq1  40108  3lexlogpow2ineq2  40109  aks4d1p1p6  40123  aks4d1p1p5  40125  dffltz  40508  flt4lem2  40521  flt4lem5  40524  flt4lem5a  40526  flt4lem5b  40527  flt4lem5c  40528  flt4lem5d  40529  flt4lem5e  40530  flt4lem7  40533  nna4b4nsq  40534  jm2.17a  40820  jm2.17b  40821  jm2.17c  40822  acongrep  40840  acongeq  40843  jm2.27a  40865  jm2.27c  40867  rmydioph  40874  rmxdioph  40876  expdiophlem2  40882  expdioph  40883  frlmpwfi  40961  amgm2d  41847  mnringaddgdOLD  41874  hashnzfz2  41977  lhe4.4ex1a  41985  limsup10exlem  43362  wallispilem5  43659  wallispi2lem1  43661  wallispi2  43663  stirlinglem3  43666  stirlinglem8  43671  stirlinglem10  43673  stirlinglem15  43678  dirkertrigeqlem3  43690  fouriersw  43821  hoicvrrex  44144  ovnsubaddlem1  44158  ovnsubaddlem2  44159  ovnsubadd2lem  44233  ovolval5lem1  44240  ovolval5lem2  44241  elmod2  44880  fmtnoodd  45043  fmtnof1  45045  fmtnosqrt  45049  fmtnorec4  45059  257prm  45071  odz2prm2pw  45073  fmtnoprmfac1lem  45074  fmtnoprmfac1  45075  fmtnoprmfac2lem1  45076  fmtnoprmfac2  45077  fmtno4prm  45085  2pwp1prm  45099  139prmALT  45106  127prm  45109  sfprmdvdsmersenne  45113  lighneallem1  45115  lighneallem3  45117  proththdlem  45123  proththd  45124  iseven5  45174  oddprmALTV  45197  perfectALTVlem1  45231  perfectALTVlem2  45232  perfectALTV  45233  fppr2odd  45241  2exp340mod341  45243  341fppr2  45244  fpprel2  45251  nnsum3primes4  45298  nnsum3primesgbe  45302  evengpoap3  45309  nnsum4primesevenALTV  45311  bgoldbtbndlem1  45315  tgblthelfgott  45325  pw2m1lepw2m1  45919  nnpw2even  45933  logbpw2m1  45971  blenpw2  45982  nnpw2pmod  45987  blen2  45989  nnpw2p  45990  nnpw2pb  45991  blennnt2  45993  nnolog2flm1  45994  dig2nn1st  46009  0dig2pr01  46014  dig2nn0  46015  0dig2nn0e  46016  0dig2nn0o  46017  dig2bits  46018  dignn0flhalflem1  46019  dignn0ehalf  46021  dignn0flhalf  46022  nn0sumshdiglemA  46023  nn0sumshdiglemB  46024  nn0sumshdiglem1  46025  nn0sumshdiglem2  46026  nn0mullong  46029  itcovalt2lem2  46080  amgmw2d  46566