Theorem 2nn 12338

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 12327	. 2 ⊢ 2 = (1 + 1)
2		1nn 12268	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12269	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2856	1 ⊢ 2 ∈ ℕ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7413  1c1 11125   + caddc 11127  ℕcn 12257  2c2 12319

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7736  ax-1cn 11182

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7416  df-om 7863  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-nn 12258  df-2 12327

This theorem is used by:  3nn  12344  0le2  12367  2pos  12369  2ne0  12371  2nn0  12545  2z  12650  uz3m2nn  12943  ige2m1fz1  13671  sqeq0  14184  sqeq0d  14209  expmulnbnd  14299  faclbnd5  14362  bcn2  14383  f1oun2prg  14988  wrdl2exs2  15017  pfx2  15018  wwlktovf  15029  reusq0  15552  climcndslem1  15938  climcndslem2  15939  climcnds  15940  harmonic  15948  geo2sum  15962  geo2lim  15964  ege2le3  16176  ef01bndlem  16272  egt2lt3  16294  nthruc  16340  mod2eq0even  16436  bits0o  16520  bitsp1  16521  bitsfzolem  16524  bitsfzo  16525  bitsmod  16526  bitsfi  16527  bitscmp  16528  bitsinv1lem  16531  bitsinv1  16532  2ebits  16537  bitsinvp1  16539  sadcaddlem  16547  sadadd3  16551  sadaddlem  16556  sadasslem  16560  bitsres  16563  bitsuz  16564  bitsshft  16565  smumullem  16582  smumul  16583  sqgcd  16652  3lcm2e6woprm  16705  prm2orodd  16781  4nprm  16785  prmdvdssq  16809  isevengcd2  16821  3lcm2e6  16823  pythagtriplem4  16911  iserodd  16927  oddprmdvds  16995  prmreclem3  17010  prmreclem5  17012  prmreclem6  17013  4sqlem12  17048  vdwlem3  17075  vdwlem9  17081  vdwlem10  17082  prmo2  17132  dec2dvds  17155  dec5nprm  17158  dec2nprm  17159  2expltfac  17184  5prm  17200  6nprm  17201  7prm  17202  8nprm  17203  10nprmOLD  17206  11prm  17207  17prm  17209  23prm  17211  37prm  17213  43prm  17214  83prm  17215  139prm  17216  163prm  17217  317prm  17218  631prm  17219  1259lem1  17223  1259lem2  17224  1259lem3  17225  1259lem4  17226  1259lem5  17227  1259prm  17228  2503lem1  17229  2503lem2  17230  2503lem3  17231  2503prm  17232  4001lem1  17233  4001lem2  17234  4001lem3  17235  4001lem4  17236  4001prm  17237  plusgndx  17368  plusgid  17369  plusgndxnn  17370  rngstr  17383  lmodstr  17410  topgrpstr  17446  dsndx  17470  dsid  17471  dsndxnn  17472  slotsdifdsndx  17479  slotsdifunifndx  17486  odrngstr  17488  imasvalstr  17536  pmtrprfvalrn  19615  psgnunilem2  19622  psgnprfval  19648  psgnprfval1  19649  cnfldstr  21587  m2detleiblem1  22846  m2detleiblem5  22847  m2detleiblem6  22848  m2detleiblem3  22851  m2detleiblem4  22852  m2detleib  22853  ovollb2lem  25716  ovolunlem1a  25724  ovolunlem1  25725  ovoliunlem1  25730  ovoliunlem3  25732  dyadf  25819  dyadovol  25821  dyadss  25822  dyaddisjlem  25823  dyadmaxlem  25825  opnmbllem  25829  mbfi1fseqlem1  25943  mbfi1fseqlem3  25945  mbfi1fseqlem4  25946  mbfi1fseqlem5  25947  mbfi1fseqlem6  25948  dveflem  26206  aaliou3lem9  26586  quartlem1  27094  quartlem2  27095  zetacvg  27251  lgamgulmlem4  27268  basellem1  27317  basellem2  27318  basellem3  27319  basellem4  27320  basellem5  27321  basellem6  27322  basellem7  27323  basellem8  27324  basellem9  27325  1sgm2ppw  27436  ppiublem1  27438  chtublem  27447  mersenne  27463  perfect1  27464  perfectlem1  27465  perfectlem2  27466  perfect  27467  pcbcctr  27512  bclbnd  27516  bposlem1  27520  bposlem2  27521  bposlem3  27522  bposlem4  27523  bposlem5  27524  bposlem6  27525  bposlem8  27527  lgsdir2lem2  27562  lgsqr  27587  lgsqrmodndvds  27589  gausslemma2dlem1a  27601  gausslemma2d  27610  lgseisenlem1  27611  lgseisenlem2  27612  lgseisenlem3  27613  lgseisenlem4  27614  lgsquadlem1  27616  lgsquadlem2  27617  lgsquad2lem2  27621  2lgslem1c  27629  2lgs  27643  2sqlem3  27656  2sqlem8  27662  chebbnd1lem1  27705  chebbnd1lem3  27707  logdivsum  27769  log2sumbnd  27780  pntlemd  27830  pntlema  27832  pntlemb  27833  pntlemf  27841  pntlemo  27843  ostth2lem1  27854  slotsinbpsd  28782  slotslnbpsd  28783  trkgstr  28785  angmgmlem  29274  angmgmbas  29277  axlowdimlem6  29404  eengstr  29437  usgrexmplef  29719  cusgrsizeindb0  29909  usgr2pthlem  30228  uspgrn2crct  30276  usgr2wspthons3  30435  clwwlkn2  30514  wwlksext2clwwlk  30527  eupth2lem3lem4  30711  frgrhash2wsp  30812  2clwwlk2clwwlk  30830  dlwwlknondlwlknonf1olem1  30844  clwlknon2num  30848  numclwlk2lem2f1o  30859  ex-xp  30916  ex-cnv  30917  ex-rn  30920  ex-mod  30929  2exple2exp  33304  fldext2rspun  34192  cos9thpiminplylem1  34292  lmat22e11  34328  lmat22e12  34329  lmat22e21  34330  lmat22e22  34331  lmat22det  34332  oddpwdc  34865  eulerpartlemt  34882  eulerpartlemgh  34889  fib0  34910  fib1  34911  fib3  34914  chtvalz  35137  hgt750lem  35159  hgt750lemb  35164  hgt750leme  35166  problem5  36248  bcprod  36317  opnmbllem0  38405  mblfinlem1  38406  dvasin  38453  areacirclem1  38457  heiborlem3  38563  heiborlem5  38565  heiborlem6  38566  heiborlem7  38567  heiborlem8  38568  heibor  38571  12gcd5e1  42869  420gcd8e4  42872  12lcm5e60  42874  60lcm7e420  42876  420lcm8e840  42877  lcm2un  42880  lcmineqlem19  42913  lcmineqlem20  42914  lcmineqlem22  42916  lcmineqlem23  42917  lcmineqlem  42918  3lexlogpow2ineq1  42924  3lexlogpow2ineq2  42925  aks4d1p1p6  42939  aks4d1p1p5  42941  readvrec2  43236  dffltz  43480  flt4lem2  43493  flt4lem5  43496  flt4lem5a  43498  flt4lem5b  43499  flt4lem5c  43500  flt4lem5d  43501  flt4lem5e  43502  flt4lem7  43505  nna4b4nsq  43506  jm2.17a  43801  jm2.17b  43802  jm2.17c  43803  acongrep  43821  acongeq  43824  jm2.27a  43846  jm2.27c  43848  rmydioph  43855  rmxdioph  43857  expdiophlem2  43863  expdioph  43864  frlmpwfi  43939  amgm2d  45038  hashnzfz2  45145  lhe4.4ex1a  45153  limsup10exlem  46600  wallispilem5  46897  wallispi2lem1  46899  wallispi2  46901  stirlinglem3  46904  stirlinglem8  46909  stirlinglem10  46911  stirlinglem15  46916  dirkertrigeqlem3  46928  fouriersw  47059  hoicvrrex  47384  ovnsubaddlem1  47398  ovnsubaddlem2  47399  ovnsubadd2lem  47473  ovolval5lem1  47480  ovolval5lem2  47481  numtowerdt  47734  ceilhalfelfzo1  48222  elmod2  48249  fmtnoodd  48436  fmtnof1  48438  fmtnosqrt  48442  fmtnorec4  48452  257prm  48464  odz2prm2pw  48466  fmtnoprmfac1lem  48467  fmtnoprmfac1  48468  fmtnoprmfac2lem1  48469  fmtnoprmfac2  48470  fmtno4prm  48478  2pwp1prm  48492  139prmALT  48499  127prm  48502  sfprmdvdsmersenne  48506  lighneallem1  48508  lighneallem3  48510  proththdlem  48516  proththd  48517  iseven5  48580  oddprmALTV  48603  perfectALTVlem1  48637  perfectALTVlem2  48638  perfectALTV  48639  fppr2odd  48647  2exp340mod341  48649  341fppr2  48650  fpprel2  48657  nnsum3primes4  48704  nnsum3primesgbe  48708  evengpoap3  48715  nnsum4primesevenALTV  48717  bgoldbtbndlem1  48721  tgblthelfgott  48731  gpgusgralem  48972  gpg3nbgrvtx0  48992  gpg3kgrtriexlem2  49000  gpg3kgrtriexlem5  49003  pw2m1lepw2m1  49450  nnpw2even  49459  logbpw2m1  49497  blenpw2  49508  nnpw2pmod  49513  blen2  49515  nnpw2p  49516  nnpw2pb  49517  blennnt2  49519  nnolog2flm1  49520  dig2nn1st  49535  0dig2pr01  49540  dig2nn0  49541  0dig2nn0e  49542  0dig2nn0o  49543  dig2bits  49544  dignn0flhalflem1  49545  dignn0ehalf  49547  dignn0flhalf  49548  nn0sumshdiglemA  49549  nn0sumshdiglemB  49550  nn0sumshdiglem1  49551  nn0sumshdiglem2  49552  nn0mullong  49555  itcovalt2lem2  49606  2elfz13  50777  veronesevrowd  50812  veroquadgsumlem  50816  amgmw2d  50822