Theorem 2nn 12325

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 12314	. 2 ⊢ 2 = (1 + 1)
2		1nn 12255	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12256	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2861	1 ⊢ 2 ∈ ℕ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7416  1c1 11112   + caddc 11114  ℕcn 12244  2c2 12306

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7738  ax-1cn 11169

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 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7419  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-nn 12245  df-2 12314

This theorem is used by:  3nn  12331  0le2  12354  2pos  12356  2ne0  12358  2nn0  12532  2z  12637  uz3m2nn  12929  ige2m1fz1  13656  sqeq0  14169  sqeq0d  14194  expmulnbnd  14284  faclbnd5  14347  bcn2  14368  f1oun2prg  14973  wrdl2exs2  15002  pfx2  15003  wwlktovf  15012  reusq0  15535  climcndslem1  15921  climcndslem2  15922  climcnds  15923  harmonic  15931  geo2sum  15945  geo2lim  15947  ege2le3  16161  ef01bndlem  16257  egt2lt3  16279  nthruc  16325  mod2eq0even  16421  bits0o  16505  bitsp1  16506  bitsfzolem  16509  bitsfzo  16510  bitsmod  16511  bitsfi  16512  bitscmp  16513  bitsinv1lem  16516  bitsinv1  16517  2ebits  16522  bitsinvp1  16524  sadcaddlem  16532  sadadd3  16536  sadaddlem  16541  sadasslem  16545  bitsres  16548  bitsuz  16549  bitsshft  16550  smumullem  16567  smumul  16568  sqgcd  16637  3lcm2e6woprm  16690  prm2orodd  16766  4nprm  16770  prmdvdssq  16794  isevengcd2  16806  3lcm2e6  16808  pythagtriplem4  16896  iserodd  16912  oddprmdvds  16980  prmreclem3  16995  prmreclem5  16997  prmreclem6  16998  4sqlem12  17033  vdwlem3  17060  vdwlem9  17066  vdwlem10  17067  prmo2  17117  dec2dvds  17140  dec5nprm  17143  dec2nprm  17144  2expltfac  17169  5prm  17185  6nprm  17186  7prm  17187  8nprm  17188  10nprmOLD  17191  11prm  17192  17prm  17194  23prm  17196  37prm  17198  43prm  17199  83prm  17200  139prm  17201  163prm  17202  317prm  17203  631prm  17204  1259lem1  17208  1259lem2  17209  1259lem3  17210  1259lem4  17211  1259lem5  17212  1259prm  17213  2503lem1  17214  2503lem2  17215  2503lem3  17216  2503prm  17217  4001lem1  17218  4001lem2  17219  4001lem3  17220  4001lem4  17221  4001prm  17222  plusgndx  17353  plusgid  17354  plusgndxnn  17355  rngstr  17368  lmodstr  17395  topgrpstr  17431  dsndx  17455  dsid  17456  dsndxnn  17457  slotsdifdsndx  17464  slotsdifunifndx  17471  odrngstr  17473  imasvalstr  17521  pmtrprfvalrn  19581  psgnunilem2  19588  psgnprfval  19614  psgnprfval1  19615  cnfldstr  21553  m2detleiblem1  22810  m2detleiblem5  22811  m2detleiblem6  22812  m2detleiblem3  22815  m2detleiblem4  22816  m2detleib  22817  ovollb2lem  25676  ovolunlem1a  25684  ovolunlem1  25685  ovoliunlem1  25690  ovoliunlem3  25692  dyadf  25779  dyadovol  25781  dyadss  25782  dyaddisjlem  25783  dyadmaxlem  25785  opnmbllem  25789  mbfi1fseqlem1  25903  mbfi1fseqlem3  25905  mbfi1fseqlem4  25906  mbfi1fseqlem5  25907  mbfi1fseqlem6  25908  dveflem  26167  aaliou3lem9  26542  quartlem1  27051  quartlem2  27052  zetacvg  27208  lgamgulmlem4  27225  basellem1  27274  basellem2  27275  basellem3  27276  basellem4  27277  basellem5  27278  basellem6  27279  basellem7  27280  basellem8  27281  basellem9  27282  1sgm2ppw  27393  ppiublem1  27395  chtublem  27404  mersenne  27420  perfect1  27421  perfectlem1  27422  perfectlem2  27423  perfect  27424  pcbcctr  27469  bclbnd  27473  bposlem1  27477  bposlem2  27478  bposlem3  27479  bposlem4  27480  bposlem5  27481  bposlem6  27482  bposlem8  27484  lgsdir2lem2  27519  lgsqr  27544  lgsqrmodndvds  27546  gausslemma2dlem1a  27558  gausslemma2d  27567  lgseisenlem1  27568  lgseisenlem2  27569  lgseisenlem3  27570  lgseisenlem4  27571  lgsquadlem1  27573  lgsquadlem2  27574  lgsquad2lem2  27578  2lgslem1c  27586  2lgs  27600  2sqlem3  27613  2sqlem8  27619  chebbnd1lem1  27662  chebbnd1lem3  27664  logdivsum  27726  log2sumbnd  27737  pntlemd  27787  pntlema  27789  pntlemb  27790  pntlemf  27798  pntlemo  27800  ostth2lem1  27811  slotsinbpsd  28739  slotslnbpsd  28740  trkgstr  28742  axlowdimlem6  29326  eengstr  29359  usgrexmplef  29638  cusgrsizeindb0  29828  usgr2pthlem  30141  uspgrn2crct  30186  usgr2wspthons3  30345  clwwlkn2  30424  wwlksext2clwwlk  30437  eupth2lem3lem4  30611  frgrhash2wsp  30712  2clwwlk2clwwlk  30730  dlwwlknondlwlknonf1olem1  30744  clwlknon2num  30748  numclwlk2lem2f1o  30759  ex-xp  30816  ex-cnv  30817  ex-rn  30820  ex-mod  30829  2exple2exp  33207  fldext2rspun  34095  cos9thpiminplylem1  34195  lmat22e11  34231  lmat22e12  34232  lmat22e21  34233  lmat22e22  34234  lmat22det  34235  oddpwdc  34768  eulerpartlemt  34785  eulerpartlemgh  34792  fib0  34813  fib1  34814  fib3  34817  chtvalz  35040  hgt750lem  35062  hgt750lemb  35067  hgt750leme  35069  problem5  36174  bcprod  36243  opnmbllem0  38340  mblfinlem1  38341  dvasin  38388  areacirclem1  38392  heiborlem3  38497  heiborlem5  38499  heiborlem6  38500  heiborlem7  38501  heiborlem8  38502  heibor  38505  12gcd5e1  42803  420gcd8e4  42806  12lcm5e60  42808  60lcm7e420  42810  420lcm8e840  42811  lcm2un  42814  lcmineqlem19  42847  lcmineqlem20  42848  lcmineqlem22  42850  lcmineqlem23  42851  lcmineqlem  42852  3lexlogpow2ineq1  42858  3lexlogpow2ineq2  42859  aks4d1p1p6  42873  aks4d1p1p5  42875  readvrec2  43155  dffltz  43399  flt4lem2  43412  flt4lem5  43415  flt4lem5a  43417  flt4lem5b  43418  flt4lem5c  43419  flt4lem5d  43420  flt4lem5e  43421  flt4lem7  43424  nna4b4nsq  43425  jm2.17a  43720  jm2.17b  43721  jm2.17c  43722  acongrep  43740  acongeq  43743  jm2.27a  43765  jm2.27c  43767  rmydioph  43774  rmxdioph  43776  expdiophlem2  43782  expdioph  43783  frlmpwfi  43858  amgm2d  44957  hashnzfz2  45064  lhe4.4ex1a  45072  limsup10exlem  46519  wallispilem5  46816  wallispi2lem1  46818  wallispi2  46820  stirlinglem3  46823  stirlinglem8  46828  stirlinglem10  46830  stirlinglem15  46835  dirkertrigeqlem3  46847  fouriersw  46978  hoicvrrex  47303  ovnsubaddlem1  47317  ovnsubaddlem2  47318  ovnsubadd2lem  47392  ovolval5lem1  47399  ovolval5lem2  47400  nthrucw  47640  ceilhalfelfzo1  48104  elmod2  48131  fmtnoodd  48318  fmtnof1  48320  fmtnosqrt  48324  fmtnorec4  48334  257prm  48346  odz2prm2pw  48348  fmtnoprmfac1lem  48349  fmtnoprmfac1  48350  fmtnoprmfac2lem1  48351  fmtnoprmfac2  48352  fmtno4prm  48360  2pwp1prm  48374  139prmALT  48381  127prm  48384  sfprmdvdsmersenne  48388  lighneallem1  48390  lighneallem3  48392  proththdlem  48398  proththd  48399  iseven5  48462  oddprmALTV  48485  perfectALTVlem1  48519  perfectALTVlem2  48520  perfectALTV  48521  fppr2odd  48529  2exp340mod341  48531  341fppr2  48532  fpprel2  48539  nnsum3primes4  48586  nnsum3primesgbe  48590  evengpoap3  48597  nnsum4primesevenALTV  48599  bgoldbtbndlem1  48603  tgblthelfgott  48613  gpgusgralem  48854  gpg3nbgrvtx0  48874  gpg3kgrtriexlem2  48882  gpg3kgrtriexlem5  48885  pw2m1lepw2m1  49333  nnpw2even  49342  logbpw2m1  49380  blenpw2  49391  nnpw2pmod  49396  blen2  49398  nnpw2p  49399  nnpw2pb  49400  blennnt2  49402  nnolog2flm1  49403  dig2nn1st  49418  0dig2pr01  49423  dig2nn0  49424  0dig2nn0e  49425  0dig2nn0o  49426  dig2bits  49427  dignn0flhalflem1  49428  dignn0ehalf  49430  dignn0flhalf  49431  nn0sumshdiglemA  49432  nn0sumshdiglemB  49433  nn0sumshdiglem1  49434  nn0sumshdiglem2  49435  nn0mullong  49438  itcovalt2lem2  49489  amgmw2d  50685