Theorem 2nn 12456

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 12445	. 2 ⊢ 2 = (1 + 1)
2		1nn 12386	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12387	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2860	1 ⊢ 2 ∈ ℕ

This proof depends on syntax axioms:   ∈ wcel 2147  (class class class)co 7451  1c1 11240   + caddc 11242  ℕcn 12375  2c2 12437

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783  ax-1cn 11297

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-nn 12376  df-2 12445

This theorem is used by:  3nn  12462  0le2  12485  2pos  12487  2ne0  12489  2nn0  12663  2z  12768  uz3m2nn  13061  ige2m1fz1  13790  sqeq0  14303  sqeq0d  14328  expmulnbnd  14420  faclbnd5  14483  bcn2  14504  f1oun2prg  15111  wrdl2exs2  15140  pfx2  15141  wwlktovf  15152  reusq0  15676  climcndslem1  16062  climcndslem2  16063  climcnds  16064  harmonic  16072  geo2sum  16086  geo2lim  16088  ege2le3  16300  ef01bndlem  16396  egt2lt3  16418  nthruc  16464  mod2eq0even  16560  bits0o  16644  bitsp1  16645  bitsfzolem  16648  bitsfzo  16649  bitsmod  16650  bitsfi  16651  bitscmp  16652  bitsinv1lem  16655  bitsinv1  16656  2ebits  16661  bitsinvp1  16663  sadcaddlem  16671  sadadd3  16675  sadaddlem  16680  sadasslem  16684  bitsres  16687  bitsuz  16688  bitsshft  16689  smumullem  16706  smumul  16707  sqgcd  16780  dvdssqnn  16785  3lcm2e6woprm  16834  prm2orodd  16910  4nprm  16914  prmdvdssq  16938  isevengcd2  16950  3lcm2e6  16952  pythagtriplem4  17041  iserodd  17057  oddprmdvds  17125  prmreclem3  17140  prmreclem5  17142  prmreclem6  17143  4sqlem12  17178  vdwlem3  17205  vdwlem9  17211  vdwlem10  17212  prmo2  17262  dec2dvds  17285  dec5nprm  17288  dec2nprm  17289  2expltfac  17314  5prm  17330  6nprm  17331  7prm  17332  8nprm  17333  10nprmOLD  17336  11prm  17337  17prm  17339  23prm  17341  37prm  17343  43prm  17344  83prm  17345  139prm  17346  163prm  17347  317prm  17348  631prm  17349  1259lem1  17353  1259lem2  17354  1259lem3  17355  1259lem4  17356  1259lem5  17357  1259prm  17358  2503lem1  17359  2503lem2  17360  2503lem3  17361  2503prm  17362  4001lem1  17363  4001lem2  17364  4001lem3  17365  4001lem4  17366  4001prm  17367  plusgndx  17500  plusgid  17501  plusgndxnn  17502  rngstr  17515  lmodstr  17542  topgrpstr  17578  dsndx  17602  dsid  17603  dsndxnn  17604  slotsdifdsndx  17611  slotsdifunifndx  17618  odrngstr  17620  basendxneufndx  17634  imasvalstr  17672  pmtrprfvalrn  19753  psgnunilem2  19760  psgnprfval  19786  psgnprfval1  19787  cnfldstr  21731  cnfldfunALT  21745  m2detleiblem1  22994  m2detleiblem5  22995  m2detleiblem6  22996  m2detleiblem3  22999  m2detleiblem4  23000  m2detleib  23001  ovollb2lem  25864  ovolunlem1a  25872  ovolunlem1  25873  ovoliunlem1  25878  ovoliunlem3  25880  dyadf  25967  dyadovol  25969  dyadss  25970  dyaddisjlem  25971  dyadmaxlem  25973  opnmbllem  25977  mbfi1fseqlem1  26091  mbfi1fseqlem3  26093  mbfi1fseqlem4  26094  mbfi1fseqlem5  26095  mbfi1fseqlem6  26096  dveflem  26354  aaliou3lem9  26734  quartlem1  27242  quartlem2  27243  zetacvg  27399  lgamgulmlem4  27416  basellem1  27465  basellem2  27466  basellem3  27467  basellem4  27468  basellem5  27469  basellem6  27470  basellem7  27471  basellem8  27472  basellem9  27473  1sgm2ppw  27584  ppiublem1  27586  chtublem  27595  mersenne  27611  perfect1  27612  perfectlem1  27613  perfectlem2  27614  perfect  27615  pcbcctr  27660  bclbnd  27664  bposlem1  27668  bposlem2  27669  bposlem3  27670  bposlem4  27671  bposlem5  27672  bposlem6  27673  bposlem8  27675  lgsdir2lem2  27710  lgsqr  27735  lgsqrmodndvds  27737  gausslemma2dlem1a  27749  gausslemma2d  27758  lgseisenlem1  27759  lgseisenlem2  27760  lgseisenlem3  27761  lgseisenlem4  27762  lgsquadlem1  27764  lgsquadlem2  27765  lgsquad2lem2  27769  2lgslem1c  27777  2lgs  27791  2sqlem3  27804  2sqlem8  27810  chebbnd1lem1  27853  chebbnd1lem3  27855  logdivsum  27917  log2sumbnd  27928  pntlemd  27978  pntlema  27980  pntlemb  27981  pntlemf  27989  pntlemo  27991  ostth2lem1  28002  flt4lem5  28037  flt4lem5a  28039  flt4lem5b  28040  flt4lem5c  28041  flt4lem5d  28042  flt4lem5e  28043  flt4lem7  28046  slotsinbpsd  28960  slotslnbpsd  28961  trkgstr  28963  angmgmlem  29452  angmgmbas  29455  axlowdimlem6  29582  eengstr  29615  usgrexmplef  29897  cusgrsizeindb0  30087  usgr2pthlem  30406  uspgrn2crct  30454  usgr2wspthons3  30613  clwwlkn2  30692  wwlksext2clwwlk  30705  eupth2lem3lem4  30889  frgrhash2wsp  30990  2clwwlk2clwwlk  31008  dlwwlknondlwlknonf1olem1  31022  clwlknon2num  31026  numclwlk2lem2f1o  31037  ex-xp  31094  ex-cnv  31095  ex-rn  31098  ex-mod  31107  2exple2exp  33521  fldext2rspun  34425  cos9thpiminplylem1  34525  lmat22e11  34561  lmat22e12  34562  lmat22e21  34563  lmat22e22  34564  lmat22det  34565  oddpwdc  35097  eulerpartlemt  35114  eulerpartlemgh  35121  fib0  35142  fib1  35143  fib3  35146  chtvalz  35369  hgt750lem  35391  hgt750lemb  35396  hgt750leme  35398  problem5  36642  bcprod  36718  opnmbllem0  38842  mblfinlem1  38843  dvasin  38890  areacirclem1  38894  heiborlem3  39013  heiborlem5  39015  heiborlem6  39016  heiborlem7  39017  heiborlem8  39018  heibor  39021  12gcd5e1  43319  420gcd8e4  43322  12lcm5e60  43324  60lcm7e420  43326  420lcm8e840  43327  lcm2un  43330  lcmineqlem19  43363  lcmineqlem20  43364  lcmineqlem22  43366  lcmineqlem23  43367  lcmineqlem  43368  3lexlogpow2ineq1  43374  3lexlogpow2ineq2  43375  aks4d1p1p6  43389  aks4d1p1p5  43391  readvrec2  43678  dffltz  43936  jm2.17a  44233  jm2.17b  44234  jm2.17c  44235  acongrep  44253  acongeq  44256  jm2.27a  44278  jm2.27c  44280  rmydioph  44287  rmxdioph  44289  expdiophlem2  44295  expdioph  44296  frlmpwfi  44366  amgm2d  45459  hashnzfz2  45566  lhe4.4ex1a  45574  limsup10exlem  47055  wallispilem5  47352  wallispi2lem1  47354  wallispi2  47356  stirlinglem3  47359  stirlinglem8  47364  stirlinglem10  47366  stirlinglem15  47371  dirkertrigeqlem3  47383  fouriersw  47514  hoicvrrex  47839  ovnsubaddlem1  47853  ovnsubaddlem2  47854  ovnsubadd2lem  47928  ovolval5lem1  47935  ovolval5lem2  47936  numtowerdt  48189  ceilhalfelfzo1  48677  elmod2  48704  fmtnoodd  48891  fmtnof1  48893  fmtnosqrt  48897  fmtnorec4  48907  257prm  48919  odz2prm2pw  48921  fmtnoprmfac1lem  48922  fmtnoprmfac1  48923  fmtnoprmfac2lem1  48924  fmtnoprmfac2  48925  fmtno4prm  48933  2pwp1prm  48947  139prmALT  48954  127prm  48957  sfprmdvdsmersenne  48961  lighneallem1  48963  lighneallem3  48965  proththdlem  48971  proththd  48972  iseven5  49035  oddprmALTV  49058  perfectALTVlem1  49092  perfectALTVlem2  49093  perfectALTV  49094  fppr2odd  49102  2exp340mod341  49104  341fppr2  49105  fpprel2  49112  nnsum3primes4  49159  nnsum3primesgbe  49163  evengpoap3  49170  nnsum4primesevenALTV  49172  bgoldbtbndlem1  49176  tgblthelfgott  49186  gpgusgralem  49427  gpg3nbgrvtx0  49447  gpg3kgrtriexlem2  49455  gpg3kgrtriexlem5  49458  bru2  49751  pw2m1lepw2m1  49963  nnpw2even  49972  logbpw2m1  50010  blenpw2  50021  nnpw2pmod  50026  blen2  50028  nnpw2p  50029  nnpw2pb  50030  blennnt2  50032  nnolog2flm1  50033  dig2nn1st  50048  0dig2pr01  50053  dig2nn0  50054  0dig2nn0e  50055  0dig2nn0o  50056  dig2bits  50057  dignn0flhalflem1  50058  dignn0ehalf  50060  dignn0flhalf  50061  nn0sumshdiglemA  50062  nn0sumshdiglemB  50063  nn0sumshdiglem1  50064  nn0sumshdiglem2  50065  nn0mullong  50068  itcovalt2lem2  50119  2elfz13  51372  veronesevrowd  51407  veroquadgsumlem  51411  amgmw2d  51417