Theorem 2nn 12318

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 12308	. 2 ⊢ 2 = (1 + 1)
2		1nn 12256	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12257	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2821	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2098  (class class class)co 7419  1c1 11141   + caddc 11143  ℕcn 12245  2c2 12300

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429  ax-un 7741  ax-1cn 11198

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-om 7872  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-nn 12246  df-2 12308

This theorem is referenced by:  3nn  12324  2nn0  12522  2z  12627  uz3m2nn  12908  ige2m1fz1  13625  sqeq0  14120  sqeq0d  14145  expmulnbnd  14233  faclbnd5  14293  bcn2  14314  f1oun2prg  14904  wrdl2exs2  14933  pfx2  14934  wwlktovf  14943  reusq0  15445  climcndslem1  15831  climcndslem2  15832  climcnds  15833  harmonic  15841  geo2sum  15855  geo2lim  15857  ege2le3  16070  ef01bndlem  16164  egt2lt3  16186  nthruc  16232  mod2eq0even  16326  bits0o  16408  bitsp1  16409  bitsfzolem  16412  bitsfzo  16413  bitsmod  16414  bitsfi  16415  bitscmp  16416  bitsinv1lem  16419  bitsinv1  16420  2ebits  16425  bitsinvp1  16427  sadcaddlem  16435  sadadd3  16439  sadaddlem  16444  sadasslem  16448  bitsres  16451  bitsuz  16452  bitsshft  16453  smumullem  16470  smumul  16471  sqgcd  16539  3lcm2e6woprm  16589  prm2orodd  16665  4nprm  16669  prmdvdssq  16692  isevengcd2  16705  3lcm2e6  16707  pythagtriplem4  16791  iserodd  16807  oddprmdvds  16875  prmreclem3  16890  prmreclem5  16892  prmreclem6  16893  4sqlem12  16928  vdwlem3  16955  vdwlem9  16961  vdwlem10  16962  prmo2  17012  dec2dvds  17035  dec5nprm  17038  dec2nprm  17039  2expltfac  17065  5prm  17081  6nprm  17082  7prm  17083  8nprm  17084  10nprm  17086  11prm  17087  17prm  17089  23prm  17091  37prm  17093  43prm  17094  83prm  17095  139prm  17096  163prm  17097  317prm  17098  631prm  17099  1259lem1  17103  1259lem2  17104  1259lem3  17105  1259lem4  17106  1259lem5  17107  1259prm  17108  2503lem1  17109  2503lem2  17110  2503lem3  17111  2503prm  17112  4001lem1  17113  4001lem2  17114  4001lem3  17115  4001lem4  17116  4001prm  17117  plusgndx  17262  plusgid  17263  plusgndxnn  17264  grpstr  17268  grpbaseOLD  17271  grpplusgOLD  17273  rngstr  17282  lmodstr  17309  topgrpstr  17345  dsndx  17369  dsid  17370  dsndxnn  17371  slotsdifdsndx  17378  slotsdifunifndx  17385  odrngstr  17387  imasvalstr  17436  pmtrprfvalrn  19455  psgnunilem2  19462  psgnprfval  19488  psgnprfval1  19489  mgpdsOLD  20100  oppraddOLD  20295  sraaddgOLD  21078  sradsOLD  21090  cnfldstr  21298  cnfldstrOLD  21313  cnfldfunALTOLDOLD  21325  zlmplusgOLD  21464  znaddOLD  21490  opsrplusgOLD  22014  m2detleiblem1  22570  m2detleiblem5  22571  m2detleiblem6  22572  m2detleiblem3  22575  m2detleiblem4  22576  m2detleib  22577  tmslemOLD  24435  tngplusgOLD  24598  ovollb2lem  25461  ovolunlem1a  25469  ovolunlem1  25470  ovoliunlem1  25475  ovoliunlem3  25477  dyadf  25564  dyadovol  25566  dyadss  25567  dyaddisjlem  25568  dyadmaxlem  25570  opnmbllem  25574  mbfi1fseqlem1  25689  mbfi1fseqlem3  25691  mbfi1fseqlem4  25692  mbfi1fseqlem5  25693  mbfi1fseqlem6  25694  dveflem  25955  aaliou3lem9  26330  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  27178  ppiublem1  27180  chtublem  27189  mersenne  27205  perfect1  27206  perfectlem1  27207  perfectlem2  27208  perfect  27209  pcbcctr  27254  bclbnd  27258  bposlem1  27262  bposlem2  27263  bposlem3  27264  bposlem4  27265  bposlem5  27266  bposlem6  27267  bposlem8  27269  lgsdir2lem2  27304  lgsqr  27329  lgsqrmodndvds  27331  gausslemma2dlem1a  27343  gausslemma2d  27352  lgseisenlem1  27353  lgseisenlem2  27354  lgseisenlem3  27355  lgseisenlem4  27356  lgsquadlem1  27358  lgsquadlem2  27359  lgsquad2lem2  27363  2lgslem1c  27371  2lgs  27385  2sqlem3  27398  2sqlem8  27404  chebbnd1lem1  27447  chebbnd1lem3  27449  logdivsum  27511  log2sumbnd  27522  pntlemd  27572  pntlema  27574  pntlemb  27575  pntlemf  27583  pntlemo  27585  ostth2lem1  27596  slotsinbpsd  28317  slotslnbpsd  28318  trkgstr  28320  ttgplusgOLD  28758  ttgdsOLD  28763  axlowdimlem6  28830  eengstr  28863  usgrexmplef  29144  cusgrsizeindb0  29335  usgr2pthlem  29649  uspgrn2crct  29691  usgr2wspthons3  29847  clwwlkn2  29926  wwlksext2clwwlk  29939  eupth2lem3lem4  30113  frgrhash2wsp  30214  2clwwlk2clwwlk  30232  dlwwlknondlwlknonf1olem1  30246  clwlknon2num  30250  numclwlk2lem2f1o  30261  ex-xp  30318  ex-cnv  30319  ex-rn  30322  ex-mod  30331  resvplusgOLD  33146  lmat22e11  33550  lmat22e12  33551  lmat22e21  33552  lmat22e22  33553  lmat22det  33554  oddpwdc  34105  eulerpartlemt  34122  eulerpartlemgh  34129  fib0  34150  fib1  34151  fib3  34154  chtvalz  34392  hgt750lem  34414  hgt750lemb  34419  hgt750leme  34421  problem5  35404  bcprod  35463  opnmbllem0  37260  mblfinlem1  37261  dvasin  37308  areacirclem1  37312  heiborlem3  37417  heiborlem5  37419  heiborlem6  37420  heiborlem7  37421  heiborlem8  37422  heibor  37425  hlhilsplusOLD  41546  12gcd5e1  41606  420gcd8e4  41609  12lcm5e60  41611  60lcm7e420  41613  420lcm8e840  41614  lcm2un  41617  lcmineqlem19  41650  lcmineqlem20  41651  lcmineqlem22  41653  lcmineqlem23  41654  lcmineqlem  41655  3lexlogpow2ineq1  41661  3lexlogpow2ineq2  41662  aks4d1p1p6  41676  aks4d1p1p5  41678  dffltz  42193  flt4lem2  42206  flt4lem5  42209  flt4lem5a  42211  flt4lem5b  42212  flt4lem5c  42213  flt4lem5d  42214  flt4lem5e  42215  flt4lem7  42218  nna4b4nsq  42219  jm2.17a  42523  jm2.17b  42524  jm2.17c  42525  acongrep  42543  acongeq  42546  jm2.27a  42568  jm2.27c  42570  rmydioph  42577  rmxdioph  42579  expdiophlem2  42585  expdioph  42586  frlmpwfi  42664  amgm2d  43770  mnringaddgdOLD  43797  hashnzfz2  43900  lhe4.4ex1a  43908  limsup10exlem  45298  wallispilem5  45595  wallispi2lem1  45597  wallispi2  45599  stirlinglem3  45602  stirlinglem8  45607  stirlinglem10  45609  stirlinglem15  45614  dirkertrigeqlem3  45626  fouriersw  45757  hoicvrrex  46082  ovnsubaddlem1  46096  ovnsubaddlem2  46097  ovnsubadd2lem  46171  ovolval5lem1  46178  ovolval5lem2  46179  elmod2  46847  fmtnoodd  47010  fmtnof1  47012  fmtnosqrt  47016  fmtnorec4  47026  257prm  47038  odz2prm2pw  47040  fmtnoprmfac1lem  47041  fmtnoprmfac1  47042  fmtnoprmfac2lem1  47043  fmtnoprmfac2  47044  fmtno4prm  47052  2pwp1prm  47066  139prmALT  47073  127prm  47076  sfprmdvdsmersenne  47080  lighneallem1  47082  lighneallem3  47084  proththdlem  47090  proththd  47091  iseven5  47141  oddprmALTV  47164  perfectALTVlem1  47198  perfectALTVlem2  47199  perfectALTV  47200  fppr2odd  47208  2exp340mod341  47210  341fppr2  47211  fpprel2  47218  nnsum3primes4  47265  nnsum3primesgbe  47269  evengpoap3  47276  nnsum4primesevenALTV  47278  bgoldbtbndlem1  47282  tgblthelfgott  47292  pw2m1lepw2m1  47774  nnpw2even  47788  logbpw2m1  47826  blenpw2  47837  nnpw2pmod  47842  blen2  47844  nnpw2p  47845  nnpw2pb  47846  blennnt2  47848  nnolog2flm1  47849  dig2nn1st  47864  0dig2pr01  47869  dig2nn0  47870  0dig2nn0e  47871  0dig2nn0o  47872  dig2bits  47873  dignn0flhalflem1  47874  dignn0ehalf  47876  dignn0flhalf  47877  nn0sumshdiglemA  47878  nn0sumshdiglemB  47879  nn0sumshdiglem1  47880  nn0sumshdiglem2  47881  nn0mullong  47884  itcovalt2lem2  47935  amgmw2d  48423