Theorem 2nn 11062

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 10956	. 2 ⊢ 2 = (1 + 1)
2		1nn 10908	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 10909	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2684	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 1977  (class class class)co 6549  1c1 9816   + caddc 9818  ℕcn 10897  2c2 10947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-1cn 9873

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-nn 10898  df-2 10956

This theorem is referenced by:  3nn  11063  2nn0  11186  2z  11286  uz3m2nn  11607  ige2m1fz1  12298  sqeq0  12789  expmulnbnd  12858  sqeq0d  12869  faclbnd5  12947  bcn2  12968  f1oun2prg  13512  wrdl2exs2  13538  wwlktovf  13547  climcndslem1  14420  climcndslem2  14421  climcnds  14422  harmonic  14430  geo2sum  14443  geo2lim  14445  ege2le3  14659  ef01bndlem  14753  egt2lt3  14773  nthruc  14819  mod2eq0even  14908  bits0o  14990  bitsp1  14991  bitsfzolem  14994  bitsfzo  14995  bitsmod  14996  bitsfi  14997  bitscmp  14998  bitsinv1lem  15001  bitsinv1  15002  2ebits  15007  bitsinvp1  15009  sadcaddlem  15017  sadadd3  15021  sadaddlem  15026  sadasslem  15030  bitsres  15033  bitsuz  15034  bitsshft  15035  smumullem  15052  smumul  15053  sqgcd  15116  3lcm2e6woprm  15166  prm2orodd  15242  3prm  15244  4nprm  15245  isevengcd2  15276  3lcm2e6  15278  pythagtriplem4  15362  iserodd  15378  oddprmdvds  15445  prmreclem3  15460  prmreclem5  15462  prmreclem6  15463  4sqlem12  15498  vdwlem3  15525  vdwlem9  15531  vdwlem10  15532  prmo2  15582  dec2dvds  15605  dec5nprm  15608  dec2nprm  15609  2expltfac  15637  5prm  15653  6nprm  15654  7prm  15655  8nprm  15656  10nprm  15658  10nprmOLD  15659  11prm  15660  17prm  15662  23prm  15664  37prm  15666  43prm  15667  83prm  15668  139prm  15669  163prm  15670  317prm  15671  631prm  15672  1259lem1  15676  1259lem2  15677  1259lem3  15678  1259lem4  15679  1259lem5  15680  1259prm  15681  2503lem1  15682  2503lem2  15683  2503lem3  15684  2503prm  15685  4001lem1  15686  4001lem2  15687  4001lem3  15688  4001lem4  15689  4001prm  15690  plusgndx  15803  plusgid  15804  grpstr  15815  grpbase  15816  grpplusg  15817  ressplusg  15818  rngstr  15823  lmodstr  15840  topgrpstr  15865  dsndx  15885  dsid  15886  odrngstr  15889  ressds  15896  imasvalstr  15935  pmtrprfvalrn  17731  psgnunilem2  17738  psgnprfval  17764  psgnprfval1  17765  mgpds  18322  oppradd  18453  sraaddg  19000  srads  19007  opsrplusg  19301  cnfldstr  19569  zlmplusg  19686  znadd  19708  m2detleiblem1  20249  m2detleiblem5  20250  m2detleiblem6  20251  m2detleiblem3  20254  m2detleiblem4  20255  m2detleib  20256  tmslem  22097  tngplusg  22256  ovollb2lem  23063  ovolunlem1a  23071  ovolunlem1  23072  ovoliunlem1  23077  ovoliunlem3  23079  dyadf  23165  dyadovol  23167  dyadss  23168  dyaddisjlem  23169  dyadmaxlem  23171  opnmbllem  23175  mbfi1fseqlem1  23288  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  mbfi1fseqlem6  23293  dveflem  23546  aaliou3lem9  23909  dcubic1lem  24370  dcubic2  24371  mcubic  24374  quartlem1  24384  quartlem2  24385  zetacvg  24541  lgamgulmlem4  24558  basellem1  24607  basellem2  24608  basellem3  24609  basellem4  24610  basellem5  24611  basellem6  24612  basellem7  24613  basellem8  24614  basellem9  24615  1sgm2ppw  24725  ppiublem1  24727  chtublem  24736  mersenne  24752  perfect1  24753  perfectlem1  24754  perfectlem2  24755  perfect  24756  pcbcctr  24801  bclbnd  24805  bposlem1  24809  bposlem2  24810  bposlem3  24811  bposlem4  24812  bposlem5  24813  bposlem6  24814  bposlem8  24816  lgsdir2lem2  24851  lgsqr  24876  lgsqrmodndvds  24878  gausslemma2dlem1a  24890  gausslemma2d  24899  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem3  24902  lgseisenlem4  24903  lgsquadlem1  24905  lgsquadlem2  24906  lgsquad2lem2  24910  2lgslem1c  24918  2lgs  24932  2sqlem3  24945  2sqlem8  24951  chebbnd1lem1  24958  chebbnd1lem3  24960  logdivsum  25022  log2sumbnd  25033  pntlemd  25083  pntlema  25085  pntlemb  25086  pntlemf  25094  pntlemo  25096  ostth2lem1  25107  trkgstr  25143  ttgplusg  25558  ttgds  25561  axlowdimlem6  25627  eengstr  25660  usgraexmplef  25929  cusgrasizeindb0  25999  usgrcyclnl2  26169  eupath2lem3  26506  ex-xp  26685  ex-cnv  26686  ex-rn  26689  ex-mod  26698  resvplusg  29164  lmat22e11  29212  lmat22e12  29213  lmat22e21  29214  lmat22e22  29215  lmat22det  29216  oddpwdc  29743  eulerpartlemt  29760  eulerpartlemgh  29767  fib0  29788  fib1  29789  fib3  29792  problem5  30817  bcprod  30877  opnmbllem0  32615  mblfinlem1  32616  dvasin  32666  areacirclem1  32670  heiborlem3  32782  heiborlem5  32784  heiborlem6  32785  heiborlem7  32786  heiborlem8  32787  heibor  32790  hlhilsplus  36250  jm2.17a  36545  jm2.17b  36546  jm2.17c  36547  acongrep  36565  acongeq  36568  jm2.27a  36590  jm2.27c  36592  rmydioph  36599  rmxdioph  36601  expdiophlem2  36607  expdioph  36608  frlmpwfi  36686  amgm2d  37523  hashnzfz2  37542  lhe4.4ex1a  37550  wallispilem5  38962  wallispi2lem1  38964  wallispi2  38966  stirlinglem3  38969  stirlinglem8  38974  stirlinglem10  38976  stirlinglem15  38981  dirkertrigeqlem3  38993  fouriersw  39124  hoicvrrex  39446  ovnsubaddlem1  39460  ovnsubaddlem2  39461  ovnsubadd2lem  39535  ovolval5lem1  39542  ovolval5lem2  39543  elmod2  39950  fmtnoodd  39983  fmtnof1  39985  fmtnosqrt  39989  fmtnorec4  39999  257prm  40011  odz2prm2pw  40013  fmtnoprmfac1lem  40014  fmtnoprmfac1  40015  fmtnoprmfac2lem1  40016  fmtnoprmfac2  40017  fmtno4prm  40025  2pwp1prm  40041  139prmALT  40049  127prm  40053  sfprmdvdsmersenne  40058  lighneallem1  40060  lighneallem3  40062  proththdlem  40068  proththd  40069  iseven5  40114  oddprmALTV  40136  perfectALTVlem1  40164  perfectALTVlem2  40165  perfectALTV  40166  nnsum3primes4  40204  nnsum3primesgbe  40208  evengpoap3  40215  nnsum4primesevenALTV  40217  bgoldbtbndlem1  40221  tgblthelfgott  40229  tgblthelfgottOLD  40236  pfx2  40275  cusgrsizeindb0  40665  usgr2pthlem  40969  uspgrn2crct  41011  usgr2wspthons3  41167  clwwlksn2  41217  wwlksext2clwwlk  41231  eupth2lem3lem4  41399  frgrhash2wsp  41497  av-numclwwlkovf2  41515  av-numclwwlk2lem1  41532  av-numclwlk2lem2f  41533  av-numclwlk2lem2f1o  41535  pw2m1lepw2m1  42104  nnpw2even  42117  logbpw2m1  42159  blenpw2  42170  nnpw2pmod  42175  blen2  42177  nnpw2p  42178  nnpw2pb  42179  blennnt2  42181  nnolog2flm1  42182  dig2nn1st  42197  0dig2pr01  42202  dig2nn0  42203  0dig2nn0e  42204  0dig2nn0o  42205  dig2bits  42206  dignn0flhalflem1  42207  dignn0ehalf  42209  dignn0flhalf  42210  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212  nn0sumshdiglem1  42213  nn0sumshdiglem2  42214  nn0mullong  42217  amgmw2d  42359