Theorem 2nn 12339

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 12329	. 2 ⊢ 2 = (1 + 1)
2		1nn 12277	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12278	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2837	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2108  (class class class)co 7431  1c1 11156   + caddc 11158  ℕcn 12266  2c2 12321

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-nn 12267  df-2 12329

This theorem is referenced by:  3nn  12345  2nn0  12543  2z  12649  uz3m2nn  12933  ige2m1fz1  13656  sqeq0  14160  sqeq0d  14185  expmulnbnd  14274  faclbnd5  14337  bcn2  14358  f1oun2prg  14956  wrdl2exs2  14985  pfx2  14986  wwlktovf  14995  reusq0  15501  climcndslem1  15885  climcndslem2  15886  climcnds  15887  harmonic  15895  geo2sum  15909  geo2lim  15911  ege2le3  16126  ef01bndlem  16220  egt2lt3  16242  nthruc  16288  mod2eq0even  16383  bits0o  16467  bitsp1  16468  bitsfzolem  16471  bitsfzo  16472  bitsmod  16473  bitsfi  16474  bitscmp  16475  bitsinv1lem  16478  bitsinv1  16479  2ebits  16484  bitsinvp1  16486  sadcaddlem  16494  sadadd3  16498  sadaddlem  16503  sadasslem  16507  bitsres  16510  bitsuz  16511  bitsshft  16512  smumullem  16529  smumul  16530  sqgcd  16599  3lcm2e6woprm  16652  prm2orodd  16728  4nprm  16732  prmdvdssq  16755  isevengcd2  16767  3lcm2e6  16769  pythagtriplem4  16857  iserodd  16873  oddprmdvds  16941  prmreclem3  16956  prmreclem5  16958  prmreclem6  16959  4sqlem12  16994  vdwlem3  17021  vdwlem9  17027  vdwlem10  17028  prmo2  17078  dec2dvds  17101  dec5nprm  17104  dec2nprm  17105  2expltfac  17130  5prm  17146  6nprm  17147  7prm  17148  8nprm  17149  10nprm  17151  11prm  17152  17prm  17154  23prm  17156  37prm  17158  43prm  17159  83prm  17160  139prm  17161  163prm  17162  317prm  17163  631prm  17164  1259lem1  17168  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  1259prm  17173  2503lem1  17174  2503lem2  17175  2503lem3  17176  2503prm  17177  4001lem1  17178  4001lem2  17179  4001lem3  17180  4001lem4  17181  4001prm  17182  plusgndx  17323  plusgid  17324  plusgndxnn  17325  grpstr  17328  grpbaseOLD  17331  grpplusgOLD  17333  rngstr  17342  lmodstr  17369  topgrpstr  17405  dsndx  17429  dsid  17430  dsndxnn  17431  slotsdifdsndx  17438  slotsdifunifndx  17445  odrngstr  17447  imasvalstr  17496  pmtrprfvalrn  19506  psgnunilem2  19513  psgnprfval  19539  psgnprfval1  19540  oppraddOLD  20344  sraaddgOLD  21180  sradsOLD  21192  cnfldstr  21366  cnfldstrOLD  21381  cnfldfunALTOLDOLD  21393  zlmplusgOLD  21532  znaddOLD  21558  opsrplusgOLD  22072  m2detleiblem1  22630  m2detleiblem5  22631  m2detleiblem6  22632  m2detleiblem3  22635  m2detleiblem4  22636  m2detleib  22637  tmslemOLD  24495  tngplusgOLD  24658  ovollb2lem  25523  ovolunlem1a  25531  ovolunlem1  25532  ovoliunlem1  25537  ovoliunlem3  25539  dyadf  25626  dyadovol  25628  dyadss  25629  dyaddisjlem  25630  dyadmaxlem  25632  opnmbllem  25636  mbfi1fseqlem1  25750  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  mbfi1fseqlem6  25755  dveflem  26017  aaliou3lem9  26392  quartlem1  26900  quartlem2  26901  zetacvg  27058  lgamgulmlem4  27075  basellem1  27124  basellem2  27125  basellem3  27126  basellem4  27127  basellem5  27128  basellem6  27129  basellem7  27130  basellem8  27131  basellem9  27132  1sgm2ppw  27244  ppiublem1  27246  chtublem  27255  mersenne  27271  perfect1  27272  perfectlem1  27273  perfectlem2  27274  perfect  27275  pcbcctr  27320  bclbnd  27324  bposlem1  27328  bposlem2  27329  bposlem3  27330  bposlem4  27331  bposlem5  27332  bposlem6  27333  bposlem8  27335  lgsdir2lem2  27370  lgsqr  27395  lgsqrmodndvds  27397  gausslemma2dlem1a  27409  gausslemma2d  27418  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem3  27421  lgseisenlem4  27422  lgsquadlem1  27424  lgsquadlem2  27425  lgsquad2lem2  27429  2lgslem1c  27437  2lgs  27451  2sqlem3  27464  2sqlem8  27470  chebbnd1lem1  27513  chebbnd1lem3  27515  logdivsum  27577  log2sumbnd  27588  pntlemd  27638  pntlema  27640  pntlemb  27641  pntlemf  27649  pntlemo  27651  ostth2lem1  27662  slotsinbpsd  28449  slotslnbpsd  28450  trkgstr  28452  ttgplusgOLD  28890  ttgdsOLD  28895  axlowdimlem6  28962  eengstr  28995  usgrexmplef  29276  cusgrsizeindb0  29467  usgr2pthlem  29783  uspgrn2crct  29828  usgr2wspthons3  29984  clwwlkn2  30063  wwlksext2clwwlk  30076  eupth2lem3lem4  30250  frgrhash2wsp  30351  2clwwlk2clwwlk  30369  dlwwlknondlwlknonf1olem1  30383  clwlknon2num  30387  numclwlk2lem2f1o  30398  ex-xp  30455  ex-cnv  30456  ex-rn  30459  ex-mod  30468  2exple2exp  32834  resvplusgOLD  33362  fldext2rspun  33732  lmat22e11  33817  lmat22e12  33818  lmat22e21  33819  lmat22e22  33820  lmat22det  33821  oddpwdc  34356  eulerpartlemt  34373  eulerpartlemgh  34380  fib0  34401  fib1  34402  fib3  34405  chtvalz  34644  hgt750lem  34666  hgt750lemb  34671  hgt750leme  34673  problem5  35674  bcprod  35738  opnmbllem0  37663  mblfinlem1  37664  dvasin  37711  areacirclem1  37715  heiborlem3  37820  heiborlem5  37822  heiborlem6  37823  heiborlem7  37824  heiborlem8  37825  heibor  37828  hlhilsplusOLD  41945  12gcd5e1  42004  420gcd8e4  42007  12lcm5e60  42009  60lcm7e420  42011  420lcm8e840  42012  lcm2un  42015  lcmineqlem19  42048  lcmineqlem20  42049  lcmineqlem22  42051  lcmineqlem23  42052  lcmineqlem  42053  3lexlogpow2ineq1  42059  3lexlogpow2ineq2  42060  aks4d1p1p6  42074  aks4d1p1p5  42076  readvrec2  42391  dffltz  42644  flt4lem2  42657  flt4lem5  42660  flt4lem5a  42662  flt4lem5b  42663  flt4lem5c  42664  flt4lem5d  42665  flt4lem5e  42666  flt4lem7  42669  nna4b4nsq  42670  jm2.17a  42972  jm2.17b  42973  jm2.17c  42974  acongrep  42992  acongeq  42995  jm2.27a  43017  jm2.27c  43019  rmydioph  43026  rmxdioph  43028  expdiophlem2  43034  expdioph  43035  frlmpwfi  43110  amgm2d  44211  mnringaddgdOLD  44237  hashnzfz2  44340  lhe4.4ex1a  44348  limsup10exlem  45787  wallispilem5  46084  wallispi2lem1  46086  wallispi2  46088  stirlinglem3  46091  stirlinglem8  46096  stirlinglem10  46098  stirlinglem15  46103  dirkertrigeqlem3  46115  fouriersw  46246  hoicvrrex  46571  ovnsubaddlem1  46585  ovnsubaddlem2  46586  ovnsubadd2lem  46660  ovolval5lem1  46667  ovolval5lem2  46668  elmod2  47357  fmtnoodd  47520  fmtnof1  47522  fmtnosqrt  47526  fmtnorec4  47536  257prm  47548  odz2prm2pw  47550  fmtnoprmfac1lem  47551  fmtnoprmfac1  47552  fmtnoprmfac2lem1  47553  fmtnoprmfac2  47554  fmtno4prm  47562  2pwp1prm  47576  139prmALT  47583  127prm  47586  sfprmdvdsmersenne  47590  lighneallem1  47592  lighneallem3  47594  proththdlem  47600  proththd  47601  iseven5  47651  oddprmALTV  47674  perfectALTVlem1  47708  perfectALTVlem2  47709  perfectALTV  47710  fppr2odd  47718  2exp340mod341  47720  341fppr2  47721  fpprel2  47728  nnsum3primes4  47775  nnsum3primesgbe  47779  evengpoap3  47786  nnsum4primesevenALTV  47788  bgoldbtbndlem1  47792  tgblthelfgott  47802  gpgusgralem  48011  ceilhalfelfzo1  48016  gpg3nbgrvtx0  48032  gpg3kgrtriexlem2  48040  gpg3kgrtriexlem5  48043  gpg5grlic  48047  pw2m1lepw2m1  48437  nnpw2even  48450  logbpw2m1  48488  blenpw2  48499  nnpw2pmod  48504  blen2  48506  nnpw2p  48507  nnpw2pb  48508  blennnt2  48510  nnolog2flm1  48511  dig2nn1st  48526  0dig2pr01  48531  dig2nn0  48532  0dig2nn0e  48533  0dig2nn0o  48534  dig2bits  48535  dignn0flhalflem1  48536  dignn0ehalf  48538  dignn0flhalf  48539  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  nn0sumshdiglem1  48542  nn0sumshdiglem2  48543  nn0mullong  48546  itcovalt2lem2  48597  amgmw2d  49323