Theorem 2nn 12201

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 12191	. 2 ⊢ 2 = (1 + 1)
2		1nn 12139	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12140	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2824	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2109  (class class class)co 7349  1c1 11010   + caddc 11012  ℕcn 12128  2c2 12183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-un 7671  ax-1cn 11067

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-nn 12129  df-2 12191

This theorem is referenced by:  3nn  12207  2ne0  12232  2nn0  12401  2z  12507  uz3m2nn  12795  ige2m1fz1  13519  sqeq0  14027  sqeq0d  14052  expmulnbnd  14142  faclbnd5  14205  bcn2  14226  f1oun2prg  14824  wrdl2exs2  14853  pfx2  14854  wwlktovf  14863  reusq0  15372  climcndslem1  15756  climcndslem2  15757  climcnds  15758  harmonic  15766  geo2sum  15780  geo2lim  15782  ege2le3  15997  ef01bndlem  16093  egt2lt3  16115  nthruc  16161  mod2eq0even  16257  bits0o  16341  bitsp1  16342  bitsfzolem  16345  bitsfzo  16346  bitsmod  16347  bitsfi  16348  bitscmp  16349  bitsinv1lem  16352  bitsinv1  16353  2ebits  16358  bitsinvp1  16360  sadcaddlem  16368  sadadd3  16372  sadaddlem  16377  sadasslem  16381  bitsres  16384  bitsuz  16385  bitsshft  16386  smumullem  16403  smumul  16404  sqgcd  16473  3lcm2e6woprm  16526  prm2orodd  16602  4nprm  16606  prmdvdssq  16629  isevengcd2  16641  3lcm2e6  16643  pythagtriplem4  16731  iserodd  16747  oddprmdvds  16815  prmreclem3  16830  prmreclem5  16832  prmreclem6  16833  4sqlem12  16868  vdwlem3  16895  vdwlem9  16901  vdwlem10  16902  prmo2  16952  dec2dvds  16975  dec5nprm  16978  dec2nprm  16979  2expltfac  17004  5prm  17020  6nprm  17021  7prm  17022  8nprm  17023  10nprm  17025  11prm  17026  17prm  17028  23prm  17030  37prm  17032  43prm  17033  83prm  17034  139prm  17035  163prm  17036  317prm  17037  631prm  17038  1259lem1  17042  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  1259prm  17047  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  4001prm  17056  plusgndx  17187  plusgid  17188  plusgndxnn  17189  rngstr  17202  lmodstr  17229  topgrpstr  17265  dsndx  17289  dsid  17290  dsndxnn  17291  slotsdifdsndx  17298  slotsdifunifndx  17305  odrngstr  17307  imasvalstr  17355  pmtrprfvalrn  19367  psgnunilem2  19374  psgnprfval  19400  psgnprfval1  19401  cnfldstr  21263  cnfldstrOLD  21278  m2detleiblem1  22509  m2detleiblem5  22510  m2detleiblem6  22511  m2detleiblem3  22514  m2detleiblem4  22515  m2detleib  22516  ovollb2lem  25387  ovolunlem1a  25395  ovolunlem1  25396  ovoliunlem1  25401  ovoliunlem3  25403  dyadf  25490  dyadovol  25492  dyadss  25493  dyaddisjlem  25494  dyadmaxlem  25496  opnmbllem  25500  mbfi1fseqlem1  25614  mbfi1fseqlem3  25616  mbfi1fseqlem4  25617  mbfi1fseqlem5  25618  mbfi1fseqlem6  25619  dveflem  25881  aaliou3lem9  26256  quartlem1  26765  quartlem2  26766  zetacvg  26923  lgamgulmlem4  26940  basellem1  26989  basellem2  26990  basellem3  26991  basellem4  26992  basellem5  26993  basellem6  26994  basellem7  26995  basellem8  26996  basellem9  26997  1sgm2ppw  27109  ppiublem1  27111  chtublem  27120  mersenne  27136  perfect1  27137  perfectlem1  27138  perfectlem2  27139  perfect  27140  pcbcctr  27185  bclbnd  27189  bposlem1  27193  bposlem2  27194  bposlem3  27195  bposlem4  27196  bposlem5  27197  bposlem6  27198  bposlem8  27200  lgsdir2lem2  27235  lgsqr  27260  lgsqrmodndvds  27262  gausslemma2dlem1a  27274  gausslemma2d  27283  lgseisenlem1  27284  lgseisenlem2  27285  lgseisenlem3  27286  lgseisenlem4  27287  lgsquadlem1  27289  lgsquadlem2  27290  lgsquad2lem2  27294  2lgslem1c  27302  2lgs  27316  2sqlem3  27329  2sqlem8  27335  chebbnd1lem1  27378  chebbnd1lem3  27380  logdivsum  27442  log2sumbnd  27453  pntlemd  27503  pntlema  27505  pntlemb  27506  pntlemf  27514  pntlemo  27516  ostth2lem1  27527  slotsinbpsd  28386  slotslnbpsd  28387  trkgstr  28389  axlowdimlem6  28892  eengstr  28925  usgrexmplef  29204  cusgrsizeindb0  29395  usgr2pthlem  29708  uspgrn2crct  29753  usgr2wspthons3  29909  clwwlkn2  29988  wwlksext2clwwlk  30001  eupth2lem3lem4  30175  frgrhash2wsp  30276  2clwwlk2clwwlk  30294  dlwwlknondlwlknonf1olem1  30308  clwlknon2num  30312  numclwlk2lem2f1o  30323  ex-xp  30380  ex-cnv  30381  ex-rn  30384  ex-mod  30393  2exple2exp  32790  fldext2rspun  33649  cos9thpiminplylem1  33749  lmat22e11  33785  lmat22e12  33786  lmat22e21  33787  lmat22e22  33788  lmat22det  33789  oddpwdc  34322  eulerpartlemt  34339  eulerpartlemgh  34346  fib0  34367  fib1  34368  fib3  34371  chtvalz  34597  hgt750lem  34619  hgt750lemb  34624  hgt750leme  34626  problem5  35646  bcprod  35715  opnmbllem0  37640  mblfinlem1  37641  dvasin  37688  areacirclem1  37692  heiborlem3  37797  heiborlem5  37799  heiborlem6  37800  heiborlem7  37801  heiborlem8  37802  heibor  37805  12gcd5e1  41980  420gcd8e4  41983  12lcm5e60  41985  60lcm7e420  41987  420lcm8e840  41988  lcm2un  41991  lcmineqlem19  42024  lcmineqlem20  42025  lcmineqlem22  42027  lcmineqlem23  42028  lcmineqlem  42029  3lexlogpow2ineq1  42035  3lexlogpow2ineq2  42036  aks4d1p1p6  42050  aks4d1p1p5  42052  readvrec2  42338  dffltz  42611  flt4lem2  42624  flt4lem5  42627  flt4lem5a  42629  flt4lem5b  42630  flt4lem5c  42631  flt4lem5d  42632  flt4lem5e  42633  flt4lem7  42636  nna4b4nsq  42637  jm2.17a  42937  jm2.17b  42938  jm2.17c  42939  acongrep  42957  acongeq  42960  jm2.27a  42982  jm2.27c  42984  rmydioph  42991  rmxdioph  42993  expdiophlem2  42999  expdioph  43000  frlmpwfi  43075  amgm2d  44175  hashnzfz2  44298  lhe4.4ex1a  44306  limsup10exlem  45757  wallispilem5  46054  wallispi2lem1  46056  wallispi2  46058  stirlinglem3  46061  stirlinglem8  46066  stirlinglem10  46068  stirlinglem15  46073  dirkertrigeqlem3  46085  fouriersw  46216  hoicvrrex  46541  ovnsubaddlem1  46555  ovnsubaddlem2  46556  ovnsubadd2lem  46630  ovolval5lem1  46637  ovolval5lem2  46638  ceilhalfelfzo1  47318  elmod2  47343  fmtnoodd  47521  fmtnof1  47523  fmtnosqrt  47527  fmtnorec4  47537  257prm  47549  odz2prm2pw  47551  fmtnoprmfac1lem  47552  fmtnoprmfac1  47553  fmtnoprmfac2lem1  47554  fmtnoprmfac2  47555  fmtno4prm  47563  2pwp1prm  47577  139prmALT  47584  127prm  47587  sfprmdvdsmersenne  47591  lighneallem1  47593  lighneallem3  47595  proththdlem  47601  proththd  47602  iseven5  47652  oddprmALTV  47675  perfectALTVlem1  47709  perfectALTVlem2  47710  perfectALTV  47711  fppr2odd  47719  2exp340mod341  47721  341fppr2  47722  fpprel2  47729  nnsum3primes4  47776  nnsum3primesgbe  47780  evengpoap3  47787  nnsum4primesevenALTV  47789  bgoldbtbndlem1  47793  tgblthelfgott  47803  gpgusgralem  48044  gpg3nbgrvtx0  48064  gpg3kgrtriexlem2  48072  gpg3kgrtriexlem5  48075  pw2m1lepw2m1  48509  nnpw2even  48518  logbpw2m1  48556  blenpw2  48567  nnpw2pmod  48572  blen2  48574  nnpw2p  48575  nnpw2pb  48576  blennnt2  48578  nnolog2flm1  48579  dig2nn1st  48594  0dig2pr01  48599  dig2nn0  48600  0dig2nn0e  48601  0dig2nn0o  48602  dig2bits  48603  dignn0flhalflem1  48604  dignn0ehalf  48606  dignn0flhalf  48607  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0sumshdiglem1  48610  nn0sumshdiglem2  48611  nn0mullong  48614  itcovalt2lem2  48665  amgmw2d  49793