Theorem 2nn 12245

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7360  1c1 11030   + caddc 11032  ℕcn 12165  2c2 12227

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682  ax-1cn 11087

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-nn 12166  df-2 12235

This theorem is referenced by:  3nn  12251  2ne0  12276  2nn0  12445  2z  12550  uz3m2nn  12835  ige2m1fz1  13561  sqeq0  14073  sqeq0d  14098  expmulnbnd  14188  faclbnd5  14251  bcn2  14272  f1oun2prg  14870  wrdl2exs2  14899  pfx2  14900  wwlktovf  14909  reusq0  15418  climcndslem1  15805  climcndslem2  15806  climcnds  15807  harmonic  15815  geo2sum  15829  geo2lim  15831  ege2le3  16046  ef01bndlem  16142  egt2lt3  16164  nthruc  16210  mod2eq0even  16306  bits0o  16390  bitsp1  16391  bitsfzolem  16394  bitsfzo  16395  bitsmod  16396  bitsfi  16397  bitscmp  16398  bitsinv1lem  16401  bitsinv1  16402  2ebits  16407  bitsinvp1  16409  sadcaddlem  16417  sadadd3  16421  sadaddlem  16426  sadasslem  16430  bitsres  16433  bitsuz  16434  bitsshft  16435  smumullem  16452  smumul  16453  sqgcd  16522  3lcm2e6woprm  16575  prm2orodd  16651  4nprm  16655  prmdvdssq  16679  isevengcd2  16691  3lcm2e6  16693  pythagtriplem4  16781  iserodd  16797  oddprmdvds  16865  prmreclem3  16880  prmreclem5  16882  prmreclem6  16883  4sqlem12  16918  vdwlem3  16945  vdwlem9  16951  vdwlem10  16952  prmo2  17002  dec2dvds  17025  dec5nprm  17028  dec2nprm  17029  2expltfac  17054  5prm  17070  6nprm  17071  7prm  17072  8nprm  17073  10nprm  17075  11prm  17076  17prm  17078  23prm  17080  37prm  17082  43prm  17083  83prm  17084  139prm  17085  163prm  17086  317prm  17087  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  1259prm  17097  2503lem1  17098  2503lem2  17099  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  4001prm  17106  plusgndx  17237  plusgid  17238  plusgndxnn  17239  rngstr  17252  lmodstr  17279  topgrpstr  17315  dsndx  17339  dsid  17340  dsndxnn  17341  slotsdifdsndx  17348  slotsdifunifndx  17355  odrngstr  17357  imasvalstr  17405  pmtrprfvalrn  19454  psgnunilem2  19461  psgnprfval  19487  psgnprfval1  19488  cnfldstr  21346  cnfldstrOLD  21361  m2detleiblem1  22599  m2detleiblem5  22600  m2detleiblem6  22601  m2detleiblem3  22604  m2detleiblem4  22605  m2detleib  22606  ovollb2lem  25465  ovolunlem1a  25473  ovolunlem1  25474  ovoliunlem1  25479  ovoliunlem3  25481  dyadf  25568  dyadovol  25570  dyadss  25571  dyaddisjlem  25572  dyadmaxlem  25574  opnmbllem  25578  mbfi1fseqlem1  25692  mbfi1fseqlem3  25694  mbfi1fseqlem4  25695  mbfi1fseqlem5  25696  mbfi1fseqlem6  25697  dveflem  25956  aaliou3lem9  26327  quartlem1  26834  quartlem2  26835  zetacvg  26992  lgamgulmlem4  27009  basellem1  27058  basellem2  27059  basellem3  27060  basellem4  27061  basellem5  27062  basellem6  27063  basellem7  27064  basellem8  27065  basellem9  27066  1sgm2ppw  27177  ppiublem1  27179  chtublem  27188  mersenne  27204  perfect1  27205  perfectlem1  27206  perfectlem2  27207  perfect  27208  pcbcctr  27253  bclbnd  27257  bposlem1  27261  bposlem2  27262  bposlem3  27263  bposlem4  27264  bposlem5  27265  bposlem6  27266  bposlem8  27268  lgsdir2lem2  27303  lgsqr  27328  lgsqrmodndvds  27330  gausslemma2dlem1a  27342  gausslemma2d  27351  lgseisenlem1  27352  lgseisenlem2  27353  lgseisenlem3  27354  lgseisenlem4  27355  lgsquadlem1  27357  lgsquadlem2  27358  lgsquad2lem2  27362  2lgslem1c  27370  2lgs  27384  2sqlem3  27397  2sqlem8  27403  chebbnd1lem1  27446  chebbnd1lem3  27448  logdivsum  27510  log2sumbnd  27521  pntlemd  27571  pntlema  27573  pntlemb  27574  pntlemf  27582  pntlemo  27584  ostth2lem1  27595  slotsinbpsd  28523  slotslnbpsd  28524  trkgstr  28526  axlowdimlem6  29030  eengstr  29063  usgrexmplef  29342  cusgrsizeindb0  29533  usgr2pthlem  29846  uspgrn2crct  29891  usgr2wspthons3  30050  clwwlkn2  30129  wwlksext2clwwlk  30142  eupth2lem3lem4  30316  frgrhash2wsp  30417  2clwwlk2clwwlk  30435  dlwwlknondlwlknonf1olem1  30449  clwlknon2num  30453  numclwlk2lem2f1o  30464  ex-xp  30521  ex-cnv  30522  ex-rn  30525  ex-mod  30534  2exple2exp  32933  fldext2rspun  33842  cos9thpiminplylem1  33942  lmat22e11  33978  lmat22e12  33979  lmat22e21  33980  lmat22e22  33981  lmat22det  33982  oddpwdc  34514  eulerpartlemt  34531  eulerpartlemgh  34538  fib0  34559  fib1  34560  fib3  34563  chtvalz  34789  hgt750lem  34811  hgt750lemb  34816  hgt750leme  34818  problem5  35867  bcprod  35936  opnmbllem0  37991  mblfinlem1  37992  dvasin  38039  areacirclem1  38043  heiborlem3  38148  heiborlem5  38150  heiborlem6  38151  heiborlem7  38152  heiborlem8  38153  heibor  38156  12gcd5e1  42456  420gcd8e4  42459  12lcm5e60  42461  60lcm7e420  42463  420lcm8e840  42464  lcm2un  42467  lcmineqlem19  42500  lcmineqlem20  42501  lcmineqlem22  42503  lcmineqlem23  42504  lcmineqlem  42505  3lexlogpow2ineq1  42511  3lexlogpow2ineq2  42512  aks4d1p1p6  42526  aks4d1p1p5  42528  readvrec2  42807  dffltz  43081  flt4lem2  43094  flt4lem5  43097  flt4lem5a  43099  flt4lem5b  43100  flt4lem5c  43101  flt4lem5d  43102  flt4lem5e  43103  flt4lem7  43106  nna4b4nsq  43107  jm2.17a  43406  jm2.17b  43407  jm2.17c  43408  acongrep  43426  acongeq  43429  jm2.27a  43451  jm2.27c  43453  rmydioph  43460  rmxdioph  43462  expdiophlem2  43468  expdioph  43469  frlmpwfi  43544  amgm2d  44643  hashnzfz2  44766  lhe4.4ex1a  44774  limsup10exlem  46218  wallispilem5  46515  wallispi2lem1  46517  wallispi2  46519  stirlinglem3  46522  stirlinglem8  46527  stirlinglem10  46529  stirlinglem15  46534  dirkertrigeqlem3  46546  fouriersw  46677  hoicvrrex  47002  ovnsubaddlem1  47016  ovnsubaddlem2  47017  ovnsubadd2lem  47091  ovolval5lem1  47098  ovolval5lem2  47099  nthrucw  47332  ceilhalfelfzo1  47794  elmod2  47821  fmtnoodd  48008  fmtnof1  48010  fmtnosqrt  48014  fmtnorec4  48024  257prm  48036  odz2prm2pw  48038  fmtnoprmfac1lem  48039  fmtnoprmfac1  48040  fmtnoprmfac2lem1  48041  fmtnoprmfac2  48042  fmtno4prm  48050  2pwp1prm  48064  139prmALT  48071  127prm  48074  sfprmdvdsmersenne  48078  lighneallem1  48080  lighneallem3  48082  proththdlem  48088  proththd  48089  iseven5  48152  oddprmALTV  48175  perfectALTVlem1  48209  perfectALTVlem2  48210  perfectALTV  48211  fppr2odd  48219  2exp340mod341  48221  341fppr2  48222  fpprel2  48229  nnsum3primes4  48276  nnsum3primesgbe  48280  evengpoap3  48287  nnsum4primesevenALTV  48289  bgoldbtbndlem1  48293  tgblthelfgott  48303  gpgusgralem  48544  gpg3nbgrvtx0  48564  gpg3kgrtriexlem2  48572  gpg3kgrtriexlem5  48575  pw2m1lepw2m1  49008  nnpw2even  49017  logbpw2m1  49055  blenpw2  49066  nnpw2pmod  49071  blen2  49073  nnpw2p  49074  nnpw2pb  49075  blennnt2  49077  nnolog2flm1  49078  dig2nn1st  49093  0dig2pr01  49098  dig2nn0  49099  0dig2nn0e  49100  0dig2nn0o  49101  dig2bits  49102  dignn0flhalflem1  49103  dignn0ehalf  49105  dignn0flhalf  49106  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108  nn0sumshdiglem1  49109  nn0sumshdiglem2  49110  nn0mullong  49113  itcovalt2lem2  49164  amgmw2d  50291