Theorem 2nn 12259

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 12249	. 2 ⊢ 2 = (1 + 1)
2		1nn 12197	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12198	. . 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 7387  1c1 11069   + caddc 11071  ℕcn 12186  2c2 12241

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 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187  df-2 12249

This theorem is referenced by:  3nn  12265  2ne0  12290  2nn0  12459  2z  12565  uz3m2nn  12853  ige2m1fz1  13577  sqeq0  14085  sqeq0d  14110  expmulnbnd  14200  faclbnd5  14263  bcn2  14284  f1oun2prg  14883  wrdl2exs2  14912  pfx2  14913  wwlktovf  14922  reusq0  15431  climcndslem1  15815  climcndslem2  15816  climcnds  15817  harmonic  15825  geo2sum  15839  geo2lim  15841  ege2le3  16056  ef01bndlem  16152  egt2lt3  16174  nthruc  16220  mod2eq0even  16316  bits0o  16400  bitsp1  16401  bitsfzolem  16404  bitsfzo  16405  bitsmod  16406  bitsfi  16407  bitscmp  16408  bitsinv1lem  16411  bitsinv1  16412  2ebits  16417  bitsinvp1  16419  sadcaddlem  16427  sadadd3  16431  sadaddlem  16436  sadasslem  16440  bitsres  16443  bitsuz  16444  bitsshft  16445  smumullem  16462  smumul  16463  sqgcd  16532  3lcm2e6woprm  16585  prm2orodd  16661  4nprm  16665  prmdvdssq  16688  isevengcd2  16700  3lcm2e6  16702  pythagtriplem4  16790  iserodd  16806  oddprmdvds  16874  prmreclem3  16889  prmreclem5  16891  prmreclem6  16892  4sqlem12  16927  vdwlem3  16954  vdwlem9  16960  vdwlem10  16961  prmo2  17011  dec2dvds  17034  dec5nprm  17037  dec2nprm  17038  2expltfac  17063  5prm  17079  6nprm  17080  7prm  17081  8nprm  17082  10nprm  17084  11prm  17085  17prm  17087  23prm  17089  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  plusgndx  17246  plusgid  17247  plusgndxnn  17248  rngstr  17261  lmodstr  17288  topgrpstr  17324  dsndx  17348  dsid  17349  dsndxnn  17350  slotsdifdsndx  17357  slotsdifunifndx  17364  odrngstr  17366  imasvalstr  17414  pmtrprfvalrn  19418  psgnunilem2  19425  psgnprfval  19451  psgnprfval1  19452  cnfldstr  21266  cnfldstrOLD  21281  m2detleiblem1  22511  m2detleiblem5  22512  m2detleiblem6  22513  m2detleiblem3  22516  m2detleiblem4  22517  m2detleib  22518  ovollb2lem  25389  ovolunlem1a  25397  ovolunlem1  25398  ovoliunlem1  25403  ovoliunlem3  25405  dyadf  25492  dyadovol  25494  dyadss  25495  dyaddisjlem  25496  dyadmaxlem  25498  opnmbllem  25502  mbfi1fseqlem1  25616  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  mbfi1fseqlem6  25621  dveflem  25883  aaliou3lem9  26258  quartlem1  26767  quartlem2  26768  zetacvg  26925  lgamgulmlem4  26942  basellem1  26991  basellem2  26992  basellem3  26993  basellem4  26994  basellem5  26995  basellem6  26996  basellem7  26997  basellem8  26998  basellem9  26999  1sgm2ppw  27111  ppiublem1  27113  chtublem  27122  mersenne  27138  perfect1  27139  perfectlem1  27140  perfectlem2  27141  perfect  27142  pcbcctr  27187  bclbnd  27191  bposlem1  27195  bposlem2  27196  bposlem3  27197  bposlem4  27198  bposlem5  27199  bposlem6  27200  bposlem8  27202  lgsdir2lem2  27237  lgsqr  27262  lgsqrmodndvds  27264  gausslemma2dlem1a  27276  gausslemma2d  27285  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgseisenlem4  27289  lgsquadlem1  27291  lgsquadlem2  27292  lgsquad2lem2  27296  2lgslem1c  27304  2lgs  27318  2sqlem3  27331  2sqlem8  27337  chebbnd1lem1  27380  chebbnd1lem3  27382  logdivsum  27444  log2sumbnd  27455  pntlemd  27505  pntlema  27507  pntlemb  27508  pntlemf  27516  pntlemo  27518  ostth2lem1  27529  slotsinbpsd  28368  slotslnbpsd  28369  trkgstr  28371  axlowdimlem6  28874  eengstr  28907  usgrexmplef  29186  cusgrsizeindb0  29377  usgr2pthlem  29693  uspgrn2crct  29738  usgr2wspthons3  29894  clwwlkn2  29973  wwlksext2clwwlk  29986  eupth2lem3lem4  30160  frgrhash2wsp  30261  2clwwlk2clwwlk  30279  dlwwlknondlwlknonf1olem1  30293  clwlknon2num  30297  numclwlk2lem2f1o  30308  ex-xp  30365  ex-cnv  30366  ex-rn  30369  ex-mod  30378  2exple2exp  32770  fldext2rspun  33677  cos9thpiminplylem1  33772  lmat22e11  33808  lmat22e12  33809  lmat22e21  33810  lmat22e22  33811  lmat22det  33812  oddpwdc  34345  eulerpartlemt  34362  eulerpartlemgh  34369  fib0  34390  fib1  34391  fib3  34394  chtvalz  34620  hgt750lem  34642  hgt750lemb  34647  hgt750leme  34649  problem5  35656  bcprod  35725  opnmbllem0  37650  mblfinlem1  37651  dvasin  37698  areacirclem1  37702  heiborlem3  37807  heiborlem5  37809  heiborlem6  37810  heiborlem7  37811  heiborlem8  37812  heibor  37815  12gcd5e1  41991  420gcd8e4  41994  12lcm5e60  41996  60lcm7e420  41998  420lcm8e840  41999  lcm2un  42002  lcmineqlem19  42035  lcmineqlem20  42036  lcmineqlem22  42038  lcmineqlem23  42039  lcmineqlem  42040  3lexlogpow2ineq1  42046  3lexlogpow2ineq2  42047  aks4d1p1p6  42061  aks4d1p1p5  42063  readvrec2  42349  dffltz  42622  flt4lem2  42635  flt4lem5  42638  flt4lem5a  42640  flt4lem5b  42641  flt4lem5c  42642  flt4lem5d  42643  flt4lem5e  42644  flt4lem7  42647  nna4b4nsq  42648  jm2.17a  42949  jm2.17b  42950  jm2.17c  42951  acongrep  42969  acongeq  42972  jm2.27a  42994  jm2.27c  42996  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  expdioph  43012  frlmpwfi  43087  amgm2d  44187  hashnzfz2  44310  lhe4.4ex1a  44318  limsup10exlem  45770  wallispilem5  46067  wallispi2lem1  46069  wallispi2  46071  stirlinglem3  46074  stirlinglem8  46079  stirlinglem10  46081  stirlinglem15  46086  dirkertrigeqlem3  46098  fouriersw  46229  hoicvrrex  46554  ovnsubaddlem1  46568  ovnsubaddlem2  46569  ovnsubadd2lem  46643  ovolval5lem1  46650  ovolval5lem2  46651  ceilhalfelfzo1  47331  elmod2  47356  fmtnoodd  47534  fmtnof1  47536  fmtnosqrt  47540  fmtnorec4  47550  257prm  47562  odz2prm2pw  47564  fmtnoprmfac1lem  47565  fmtnoprmfac1  47566  fmtnoprmfac2lem1  47567  fmtnoprmfac2  47568  fmtno4prm  47576  2pwp1prm  47590  139prmALT  47597  127prm  47600  sfprmdvdsmersenne  47604  lighneallem1  47606  lighneallem3  47608  proththdlem  47614  proththd  47615  iseven5  47665  oddprmALTV  47688  perfectALTVlem1  47722  perfectALTVlem2  47723  perfectALTV  47724  fppr2odd  47732  2exp340mod341  47734  341fppr2  47735  fpprel2  47742  nnsum3primes4  47789  nnsum3primesgbe  47793  evengpoap3  47800  nnsum4primesevenALTV  47802  bgoldbtbndlem1  47806  tgblthelfgott  47816  gpgusgralem  48047  gpg3nbgrvtx0  48067  gpg3kgrtriexlem2  48075  gpg3kgrtriexlem5  48078  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