Theorem 2nn 12218

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 12208	. 2 ⊢ 2 = (1 + 1)
2		1nn 12156	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12157	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2832	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  1c1 11027   + caddc 11029  ℕcn 12145  2c2 12200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-1cn 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-nn 12146  df-2 12208

This theorem is referenced by:  3nn  12224  2ne0  12249  2nn0  12418  2z  12523  uz3m2nn  12807  ige2m1fz1  13532  sqeq0  14043  sqeq0d  14068  expmulnbnd  14158  faclbnd5  14221  bcn2  14242  f1oun2prg  14840  wrdl2exs2  14869  pfx2  14870  wwlktovf  14879  reusq0  15388  climcndslem1  15772  climcndslem2  15773  climcnds  15774  harmonic  15782  geo2sum  15796  geo2lim  15798  ege2le3  16013  ef01bndlem  16109  egt2lt3  16131  nthruc  16177  mod2eq0even  16273  bits0o  16357  bitsp1  16358  bitsfzolem  16361  bitsfzo  16362  bitsmod  16363  bitsfi  16364  bitscmp  16365  bitsinv1lem  16368  bitsinv1  16369  2ebits  16374  bitsinvp1  16376  sadcaddlem  16384  sadadd3  16388  sadaddlem  16393  sadasslem  16397  bitsres  16400  bitsuz  16401  bitsshft  16402  smumullem  16419  smumul  16420  sqgcd  16489  3lcm2e6woprm  16542  prm2orodd  16618  4nprm  16622  prmdvdssq  16645  isevengcd2  16657  3lcm2e6  16659  pythagtriplem4  16747  iserodd  16763  oddprmdvds  16831  prmreclem3  16846  prmreclem5  16848  prmreclem6  16849  4sqlem12  16884  vdwlem3  16911  vdwlem9  16917  vdwlem10  16918  prmo2  16968  dec2dvds  16991  dec5nprm  16994  dec2nprm  16995  2expltfac  17020  5prm  17036  6nprm  17037  7prm  17038  8nprm  17039  10nprm  17041  11prm  17042  17prm  17044  23prm  17046  37prm  17048  43prm  17049  83prm  17050  139prm  17051  163prm  17052  317prm  17053  631prm  17054  1259lem1  17058  1259lem2  17059  1259lem3  17060  1259lem4  17061  1259lem5  17062  1259prm  17063  2503lem1  17064  2503lem2  17065  2503lem3  17066  2503prm  17067  4001lem1  17068  4001lem2  17069  4001lem3  17070  4001lem4  17071  4001prm  17072  plusgndx  17203  plusgid  17204  plusgndxnn  17205  rngstr  17218  lmodstr  17245  topgrpstr  17281  dsndx  17305  dsid  17306  dsndxnn  17307  slotsdifdsndx  17314  slotsdifunifndx  17321  odrngstr  17323  imasvalstr  17371  pmtrprfvalrn  19417  psgnunilem2  19424  psgnprfval  19450  psgnprfval1  19451  cnfldstr  21311  cnfldstrOLD  21326  m2detleiblem1  22568  m2detleiblem5  22569  m2detleiblem6  22570  m2detleiblem3  22573  m2detleiblem4  22574  m2detleib  22575  ovollb2lem  25445  ovolunlem1a  25453  ovolunlem1  25454  ovoliunlem1  25459  ovoliunlem3  25461  dyadf  25548  dyadovol  25550  dyadss  25551  dyaddisjlem  25552  dyadmaxlem  25554  opnmbllem  25558  mbfi1fseqlem1  25672  mbfi1fseqlem3  25674  mbfi1fseqlem4  25675  mbfi1fseqlem5  25676  mbfi1fseqlem6  25677  dveflem  25939  aaliou3lem9  26314  quartlem1  26823  quartlem2  26824  zetacvg  26981  lgamgulmlem4  26998  basellem1  27047  basellem2  27048  basellem3  27049  basellem4  27050  basellem5  27051  basellem6  27052  basellem7  27053  basellem8  27054  basellem9  27055  1sgm2ppw  27167  ppiublem1  27169  chtublem  27178  mersenne  27194  perfect1  27195  perfectlem1  27196  perfectlem2  27197  perfect  27198  pcbcctr  27243  bclbnd  27247  bposlem1  27251  bposlem2  27252  bposlem3  27253  bposlem4  27254  bposlem5  27255  bposlem6  27256  bposlem8  27258  lgsdir2lem2  27293  lgsqr  27318  lgsqrmodndvds  27320  gausslemma2dlem1a  27332  gausslemma2d  27341  lgseisenlem1  27342  lgseisenlem2  27343  lgseisenlem3  27344  lgseisenlem4  27345  lgsquadlem1  27347  lgsquadlem2  27348  lgsquad2lem2  27352  2lgslem1c  27360  2lgs  27374  2sqlem3  27387  2sqlem8  27393  chebbnd1lem1  27436  chebbnd1lem3  27438  logdivsum  27500  log2sumbnd  27511  pntlemd  27561  pntlema  27563  pntlemb  27564  pntlemf  27572  pntlemo  27574  ostth2lem1  27585  slotsinbpsd  28513  slotslnbpsd  28514  trkgstr  28516  axlowdimlem6  29020  eengstr  29053  usgrexmplef  29332  cusgrsizeindb0  29523  usgr2pthlem  29836  uspgrn2crct  29881  usgr2wspthons3  30040  clwwlkn2  30119  wwlksext2clwwlk  30132  eupth2lem3lem4  30306  frgrhash2wsp  30407  2clwwlk2clwwlk  30425  dlwwlknondlwlknonf1olem1  30439  clwlknon2num  30443  numclwlk2lem2f1o  30454  ex-xp  30511  ex-cnv  30512  ex-rn  30515  ex-mod  30524  2exple2exp  32926  fldext2rspun  33839  cos9thpiminplylem1  33939  lmat22e11  33975  lmat22e12  33976  lmat22e21  33977  lmat22e22  33978  lmat22det  33979  oddpwdc  34511  eulerpartlemt  34528  eulerpartlemgh  34535  fib0  34556  fib1  34557  fib3  34560  chtvalz  34786  hgt750lem  34808  hgt750lemb  34813  hgt750leme  34815  problem5  35863  bcprod  35932  opnmbllem0  37857  mblfinlem1  37858  dvasin  37905  areacirclem1  37909  heiborlem3  38014  heiborlem5  38016  heiborlem6  38017  heiborlem7  38018  heiborlem8  38019  heibor  38022  12gcd5e1  42257  420gcd8e4  42260  12lcm5e60  42262  60lcm7e420  42264  420lcm8e840  42265  lcm2un  42268  lcmineqlem19  42301  lcmineqlem20  42302  lcmineqlem22  42304  lcmineqlem23  42305  lcmineqlem  42306  3lexlogpow2ineq1  42312  3lexlogpow2ineq2  42313  aks4d1p1p6  42327  aks4d1p1p5  42329  readvrec2  42616  dffltz  42877  flt4lem2  42890  flt4lem5  42893  flt4lem5a  42895  flt4lem5b  42896  flt4lem5c  42897  flt4lem5d  42898  flt4lem5e  42899  flt4lem7  42902  nna4b4nsq  42903  jm2.17a  43202  jm2.17b  43203  jm2.17c  43204  acongrep  43222  acongeq  43225  jm2.27a  43247  jm2.27c  43249  rmydioph  43256  rmxdioph  43258  expdiophlem2  43264  expdioph  43265  frlmpwfi  43340  amgm2d  44439  hashnzfz2  44562  lhe4.4ex1a  44570  limsup10exlem  46016  wallispilem5  46313  wallispi2lem1  46315  wallispi2  46317  stirlinglem3  46320  stirlinglem8  46325  stirlinglem10  46327  stirlinglem15  46332  dirkertrigeqlem3  46344  fouriersw  46475  hoicvrrex  46800  ovnsubaddlem1  46814  ovnsubaddlem2  46815  ovnsubadd2lem  46889  ovolval5lem1  46896  ovolval5lem2  46897  nthrucw  47130  ceilhalfelfzo1  47576  elmod2  47601  fmtnoodd  47779  fmtnof1  47781  fmtnosqrt  47785  fmtnorec4  47795  257prm  47807  odz2prm2pw  47809  fmtnoprmfac1lem  47810  fmtnoprmfac1  47811  fmtnoprmfac2lem1  47812  fmtnoprmfac2  47813  fmtno4prm  47821  2pwp1prm  47835  139prmALT  47842  127prm  47845  sfprmdvdsmersenne  47849  lighneallem1  47851  lighneallem3  47853  proththdlem  47859  proththd  47860  iseven5  47910  oddprmALTV  47933  perfectALTVlem1  47967  perfectALTVlem2  47968  perfectALTV  47969  fppr2odd  47977  2exp340mod341  47979  341fppr2  47980  fpprel2  47987  nnsum3primes4  48034  nnsum3primesgbe  48038  evengpoap3  48045  nnsum4primesevenALTV  48047  bgoldbtbndlem1  48051  tgblthelfgott  48061  gpgusgralem  48302  gpg3nbgrvtx0  48322  gpg3kgrtriexlem2  48330  gpg3kgrtriexlem5  48333  pw2m1lepw2m1  48766  nnpw2even  48775  logbpw2m1  48813  blenpw2  48824  nnpw2pmod  48829  blen2  48831  nnpw2p  48832  nnpw2pb  48833  blennnt2  48835  nnolog2flm1  48836  dig2nn1st  48851  0dig2pr01  48856  dig2nn0  48857  0dig2nn0e  48858  0dig2nn0o  48859  dig2bits  48860  dignn0flhalflem1  48861  dignn0ehalf  48863  dignn0flhalf  48864  nn0sumshdiglemA  48865  nn0sumshdiglemB  48866  nn0sumshdiglem1  48867  nn0sumshdiglem2  48868  nn0mullong  48871  itcovalt2lem2  48922  amgmw2d  50049