Theorem 2nn 12285

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 12275	. 2 ⊢ 2 = (1 + 1)
2		1nn 12223	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12224	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2830	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2107  (class class class)co 7409  1c1 11111   + caddc 11113  ℕcn 12212  2c2 12267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725  ax-1cn 11168

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-nn 12213  df-2 12275

This theorem is referenced by:  3nn  12291  2nn0  12489  2z  12594  uz3m2nn  12875  ige2m1fz1  13590  sqeq0  14085  sqeq0d  14110  expmulnbnd  14198  faclbnd5  14258  bcn2  14279  f1oun2prg  14868  wrdl2exs2  14897  pfx2  14898  wwlktovf  14907  reusq0  15409  climcndslem1  15795  climcndslem2  15796  climcnds  15797  harmonic  15805  geo2sum  15819  geo2lim  15821  ege2le3  16033  ef01bndlem  16127  egt2lt3  16149  nthruc  16195  mod2eq0even  16289  bits0o  16371  bitsp1  16372  bitsfzolem  16375  bitsfzo  16376  bitsmod  16377  bitsfi  16378  bitscmp  16379  bitsinv1lem  16382  bitsinv1  16383  2ebits  16388  bitsinvp1  16390  sadcaddlem  16398  sadadd3  16402  sadaddlem  16407  sadasslem  16411  bitsres  16414  bitsuz  16415  bitsshft  16416  smumullem  16433  smumul  16434  sqgcd  16502  3lcm2e6woprm  16552  prm2orodd  16628  4nprm  16632  prmdvdssq  16655  isevengcd2  16666  3lcm2e6  16668  pythagtriplem4  16752  iserodd  16768  oddprmdvds  16836  prmreclem3  16851  prmreclem5  16853  prmreclem6  16854  4sqlem12  16889  vdwlem3  16916  vdwlem9  16922  vdwlem10  16923  prmo2  16973  dec2dvds  16996  dec5nprm  16999  dec2nprm  17000  2expltfac  17026  5prm  17042  6nprm  17043  7prm  17044  8nprm  17045  10nprm  17047  11prm  17048  17prm  17050  23prm  17052  37prm  17054  43prm  17055  83prm  17056  139prm  17057  163prm  17058  317prm  17059  631prm  17060  1259lem1  17064  1259lem2  17065  1259lem3  17066  1259lem4  17067  1259lem5  17068  1259prm  17069  2503lem1  17070  2503lem2  17071  2503lem3  17072  2503prm  17073  4001lem1  17074  4001lem2  17075  4001lem3  17076  4001lem4  17077  4001prm  17078  plusgndx  17223  plusgid  17224  plusgndxnn  17225  grpstr  17229  grpbaseOLD  17232  grpplusgOLD  17234  rngstr  17243  lmodstr  17270  topgrpstr  17306  dsndx  17330  dsid  17331  dsndxnn  17332  slotsdifdsndx  17339  slotsdifunifndx  17346  odrngstr  17348  imasvalstr  17397  pmtrprfvalrn  19356  psgnunilem2  19363  psgnprfval  19389  psgnprfval1  19390  mgpdsOLD  20001  oppraddOLD  20160  sraaddgOLD  20795  sradsOLD  20807  cnfldstr  20946  cnfldfunALTOLD  20958  zlmplusgOLD  21071  znaddOLD  21095  opsrplusgOLD  21609  m2detleiblem1  22126  m2detleiblem5  22127  m2detleiblem6  22128  m2detleiblem3  22131  m2detleiblem4  22132  m2detleib  22133  tmslemOLD  23991  tngplusgOLD  24154  ovollb2lem  25005  ovolunlem1a  25013  ovolunlem1  25014  ovoliunlem1  25019  ovoliunlem3  25021  dyadf  25108  dyadovol  25110  dyadss  25111  dyaddisjlem  25112  dyadmaxlem  25114  opnmbllem  25118  mbfi1fseqlem1  25233  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  mbfi1fseqlem6  25238  dveflem  25496  aaliou3lem9  25863  quartlem1  26362  quartlem2  26363  zetacvg  26519  lgamgulmlem4  26536  basellem1  26585  basellem2  26586  basellem3  26587  basellem4  26588  basellem5  26589  basellem6  26590  basellem7  26591  basellem8  26592  basellem9  26593  1sgm2ppw  26703  ppiublem1  26705  chtublem  26714  mersenne  26730  perfect1  26731  perfectlem1  26732  perfectlem2  26733  perfect  26734  pcbcctr  26779  bclbnd  26783  bposlem1  26787  bposlem2  26788  bposlem3  26789  bposlem4  26790  bposlem5  26791  bposlem6  26792  bposlem8  26794  lgsdir2lem2  26829  lgsqr  26854  lgsqrmodndvds  26856  gausslemma2dlem1a  26868  gausslemma2d  26877  lgseisenlem1  26878  lgseisenlem2  26879  lgseisenlem3  26880  lgseisenlem4  26881  lgsquadlem1  26883  lgsquadlem2  26884  lgsquad2lem2  26888  2lgslem1c  26896  2lgs  26910  2sqlem3  26923  2sqlem8  26929  chebbnd1lem1  26972  chebbnd1lem3  26974  logdivsum  27036  log2sumbnd  27047  pntlemd  27097  pntlema  27099  pntlemb  27100  pntlemf  27108  pntlemo  27110  ostth2lem1  27121  slotsinbpsd  27692  slotslnbpsd  27693  trkgstr  27695  ttgplusgOLD  28133  ttgdsOLD  28138  axlowdimlem6  28205  eengstr  28238  usgrexmplef  28516  cusgrsizeindb0  28706  usgr2pthlem  29020  uspgrn2crct  29062  usgr2wspthons3  29218  clwwlkn2  29297  wwlksext2clwwlk  29310  eupth2lem3lem4  29484  frgrhash2wsp  29585  2clwwlk2clwwlk  29603  dlwwlknondlwlknonf1olem1  29617  clwlknon2num  29621  numclwlk2lem2f1o  29632  ex-xp  29689  ex-cnv  29690  ex-rn  29693  ex-mod  29702  resvplusgOLD  32450  lmat22e11  32798  lmat22e12  32799  lmat22e21  32800  lmat22e22  32801  lmat22det  32802  oddpwdc  33353  eulerpartlemt  33370  eulerpartlemgh  33377  fib0  33398  fib1  33399  fib3  33402  chtvalz  33641  hgt750lem  33663  hgt750lemb  33668  hgt750leme  33670  problem5  34654  bcprod  34708  opnmbllem0  36524  mblfinlem1  36525  dvasin  36572  areacirclem1  36576  heiborlem3  36681  heiborlem5  36683  heiborlem6  36684  heiborlem7  36685  heiborlem8  36686  heibor  36689  hlhilsplusOLD  40814  12gcd5e1  40868  420gcd8e4  40871  12lcm5e60  40873  60lcm7e420  40875  420lcm8e840  40876  lcm2un  40879  lcmineqlem19  40912  lcmineqlem20  40913  lcmineqlem22  40915  lcmineqlem23  40916  lcmineqlem  40917  3lexlogpow2ineq1  40923  3lexlogpow2ineq2  40924  aks4d1p1p6  40938  aks4d1p1p5  40940  dffltz  41376  flt4lem2  41389  flt4lem5  41392  flt4lem5a  41394  flt4lem5b  41395  flt4lem5c  41396  flt4lem5d  41397  flt4lem5e  41398  flt4lem7  41401  nna4b4nsq  41402  jm2.17a  41699  jm2.17b  41700  jm2.17c  41701  acongrep  41719  acongeq  41722  jm2.27a  41744  jm2.27c  41746  rmydioph  41753  rmxdioph  41755  expdiophlem2  41761  expdioph  41762  frlmpwfi  41840  amgm2d  42950  mnringaddgdOLD  42977  hashnzfz2  43080  lhe4.4ex1a  43088  limsup10exlem  44488  wallispilem5  44785  wallispi2lem1  44787  wallispi2  44789  stirlinglem3  44792  stirlinglem8  44797  stirlinglem10  44799  stirlinglem15  44804  dirkertrigeqlem3  44816  fouriersw  44947  hoicvrrex  45272  ovnsubaddlem1  45286  ovnsubaddlem2  45287  ovnsubadd2lem  45361  ovolval5lem1  45368  ovolval5lem2  45369  elmod2  46038  fmtnoodd  46201  fmtnof1  46203  fmtnosqrt  46207  fmtnorec4  46217  257prm  46229  odz2prm2pw  46231  fmtnoprmfac1lem  46232  fmtnoprmfac1  46233  fmtnoprmfac2lem1  46234  fmtnoprmfac2  46235  fmtno4prm  46243  2pwp1prm  46257  139prmALT  46264  127prm  46267  sfprmdvdsmersenne  46271  lighneallem1  46273  lighneallem3  46275  proththdlem  46281  proththd  46282  iseven5  46332  oddprmALTV  46355  perfectALTVlem1  46389  perfectALTVlem2  46390  perfectALTV  46391  fppr2odd  46399  2exp340mod341  46401  341fppr2  46402  fpprel2  46409  nnsum3primes4  46456  nnsum3primesgbe  46460  evengpoap3  46467  nnsum4primesevenALTV  46469  bgoldbtbndlem1  46473  tgblthelfgott  46483  pw2m1lepw2m1  47201  nnpw2even  47215  logbpw2m1  47253  blenpw2  47264  nnpw2pmod  47269  blen2  47271  nnpw2p  47272  nnpw2pb  47273  blennnt2  47275  nnolog2flm1  47276  dig2nn1st  47291  0dig2pr01  47296  dig2nn0  47297  0dig2nn0e  47298  0dig2nn0o  47299  dig2bits  47300  dignn0flhalflem1  47301  dignn0ehalf  47303  dignn0flhalf  47304  nn0sumshdiglemA  47305  nn0sumshdiglemB  47306  nn0sumshdiglem1  47307  nn0sumshdiglem2  47308  nn0mullong  47311  itcovalt2lem2  47362  amgmw2d  47851