Theorem 2nn 12284

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 12273	. 2 ⊢ 2 = (1 + 1)
2		1nn 12214	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12215	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2857	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2141  (class class class)co 7390  1c1 11067   + caddc 11069  ℕcn 12203  2c2 12265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387  ax-un 7712  ax-1cn 11124

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6282  df-ord 6343  df-on 6344  df-lim 6345  df-suc 6346  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-ov 7393  df-om 7841  df-2nd 7965  df-frecs 8255  df-wrecs 8286  df-recs 8335  df-rdg 8374  df-nn 12204  df-2 12273

This theorem is referenced by:  3nn  12290  0le2  12313  2pos  12315  2ne0  12317  2nn0  12491  2z  12596  uz3m2nn  12888  ige2m1fz1  13614  sqeq0  14126  sqeq0d  14151  expmulnbnd  14241  faclbnd5  14304  bcn2  14325  f1oun2prg  14923  wrdl2exs2  14952  pfx2  14953  wwlktovf  14962  reusq0  15482  climcndslem1  15869  climcndslem2  15870  climcnds  15871  harmonic  15879  geo2sum  15893  geo2lim  15895  ege2le3  16110  ef01bndlem  16206  egt2lt3  16228  nthruc  16274  mod2eq0even  16370  bits0o  16454  bitsp1  16455  bitsfzolem  16458  bitsfzo  16459  bitsmod  16460  bitsfi  16461  bitscmp  16462  bitsinv1lem  16465  bitsinv1  16466  2ebits  16471  bitsinvp1  16473  sadcaddlem  16481  sadadd3  16485  sadaddlem  16490  sadasslem  16494  bitsres  16497  bitsuz  16498  bitsshft  16499  smumullem  16516  smumul  16517  sqgcd  16586  3lcm2e6woprm  16639  prm2orodd  16715  4nprm  16719  prmdvdssq  16743  isevengcd2  16755  3lcm2e6  16757  pythagtriplem4  16845  iserodd  16861  oddprmdvds  16929  prmreclem3  16944  prmreclem5  16946  prmreclem6  16947  4sqlem12  16982  vdwlem3  17009  vdwlem9  17015  vdwlem10  17016  prmo2  17066  dec2dvds  17089  dec5nprm  17092  dec2nprm  17093  2expltfac  17118  5prm  17134  6nprm  17135  7prm  17136  8nprm  17137  10nprmOLD  17140  11prm  17141  17prm  17143  23prm  17145  37prm  17147  43prm  17148  83prm  17149  139prm  17150  163prm  17151  317prm  17152  631prm  17153  1259lem1  17157  1259lem2  17158  1259lem3  17159  1259lem4  17160  1259lem5  17161  1259prm  17162  2503lem1  17163  2503lem2  17164  2503lem3  17165  2503prm  17166  4001lem1  17167  4001lem2  17168  4001lem3  17169  4001lem4  17170  4001prm  17171  plusgndx  17302  plusgid  17303  plusgndxnn  17304  rngstr  17317  lmodstr  17344  topgrpstr  17380  dsndx  17404  dsid  17405  dsndxnn  17406  slotsdifdsndx  17413  slotsdifunifndx  17420  odrngstr  17422  imasvalstr  17470  pmtrprfvalrn  19518  psgnunilem2  19525  psgnprfval  19551  psgnprfval1  19552  cnfldstr  21413  m2detleiblem1  22671  m2detleiblem5  22672  m2detleiblem6  22673  m2detleiblem3  22676  m2detleiblem4  22677  m2detleib  22678  ovollb2lem  25537  ovolunlem1a  25545  ovolunlem1  25546  ovoliunlem1  25551  ovoliunlem3  25553  dyadf  25640  dyadovol  25642  dyadss  25643  dyaddisjlem  25644  dyadmaxlem  25646  opnmbllem  25650  mbfi1fseqlem1  25764  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mbfi1fseqlem6  25769  dveflem  26028  aaliou3lem9  26401  quartlem1  26909  quartlem2  26910  zetacvg  27066  lgamgulmlem4  27083  basellem1  27132  basellem2  27133  basellem3  27134  basellem4  27135  basellem5  27136  basellem6  27137  basellem7  27138  basellem8  27139  basellem9  27140  1sgm2ppw  27251  ppiublem1  27253  chtublem  27262  mersenne  27278  perfect1  27279  perfectlem1  27280  perfectlem2  27281  perfect  27282  pcbcctr  27327  bclbnd  27331  bposlem1  27335  bposlem2  27336  bposlem3  27337  bposlem4  27338  bposlem5  27339  bposlem6  27340  bposlem8  27342  lgsdir2lem2  27377  lgsqr  27402  lgsqrmodndvds  27404  gausslemma2dlem1a  27416  gausslemma2d  27425  lgseisenlem1  27426  lgseisenlem2  27427  lgseisenlem3  27428  lgseisenlem4  27429  lgsquadlem1  27431  lgsquadlem2  27432  lgsquad2lem2  27436  2lgslem1c  27444  2lgs  27458  2sqlem3  27471  2sqlem8  27477  chebbnd1lem1  27520  chebbnd1lem3  27522  logdivsum  27584  log2sumbnd  27595  pntlemd  27645  pntlema  27647  pntlemb  27648  pntlemf  27656  pntlemo  27658  ostth2lem1  27669  slotsinbpsd  28597  slotslnbpsd  28598  trkgstr  28600  axlowdimlem6  29104  eengstr  29137  usgrexmplef  29416  cusgrsizeindb0  29606  usgr2pthlem  29919  uspgrn2crct  29964  usgr2wspthons3  30123  clwwlkn2  30202  wwlksext2clwwlk  30215  eupth2lem3lem4  30389  frgrhash2wsp  30490  2clwwlk2clwwlk  30508  dlwwlknondlwlknonf1olem1  30522  clwlknon2num  30526  numclwlk2lem2f1o  30537  ex-xp  30594  ex-cnv  30595  ex-rn  30598  ex-mod  30607  2exple2exp  32996  fldext2rspun  33939  cos9thpiminplylem1  34039  lmat22e11  34075  lmat22e12  34076  lmat22e21  34077  lmat22e22  34078  lmat22det  34079  oddpwdc  34611  eulerpartlemt  34628  eulerpartlemgh  34635  fib0  34656  fib1  34657  fib3  34660  chtvalz  34883  hgt750lem  34905  hgt750lemb  34910  hgt750leme  34912  problem5  35979  bcprod  36048  opnmbllem0  38115  mblfinlem1  38116  dvasin  38163  areacirclem1  38167  heiborlem3  38272  heiborlem5  38274  heiborlem6  38275  heiborlem7  38276  heiborlem8  38277  heibor  38280  12gcd5e1  42580  420gcd8e4  42583  12lcm5e60  42585  60lcm7e420  42587  420lcm8e840  42588  lcm2un  42591  lcmineqlem19  42624  lcmineqlem20  42625  lcmineqlem22  42627  lcmineqlem23  42628  lcmineqlem  42629  3lexlogpow2ineq1  42635  3lexlogpow2ineq2  42636  aks4d1p1p6  42650  aks4d1p1p5  42652  readvrec2  42930  dffltz  43176  flt4lem2  43189  flt4lem5  43192  flt4lem5a  43194  flt4lem5b  43195  flt4lem5c  43196  flt4lem5d  43197  flt4lem5e  43198  flt4lem7  43201  nna4b4nsq  43202  jm2.17a  43497  jm2.17b  43498  jm2.17c  43499  acongrep  43517  acongeq  43520  jm2.27a  43542  jm2.27c  43544  rmydioph  43551  rmxdioph  43553  expdiophlem2  43559  expdioph  43560  frlmpwfi  43635  amgm2d  44734  hashnzfz2  44857  lhe4.4ex1a  44865  limsup10exlem  46306  wallispilem5  46603  wallispi2lem1  46605  wallispi2  46607  stirlinglem3  46610  stirlinglem8  46615  stirlinglem10  46617  stirlinglem15  46622  dirkertrigeqlem3  46634  fouriersw  46765  hoicvrrex  47090  ovnsubaddlem1  47104  ovnsubaddlem2  47105  ovnsubadd2lem  47179  ovolval5lem1  47186  ovolval5lem2  47187  nthrucw  47422  ceilhalfelfzo1  47888  elmod2  47915  fmtnoodd  48102  fmtnof1  48104  fmtnosqrt  48108  fmtnorec4  48118  257prm  48130  odz2prm2pw  48132  fmtnoprmfac1lem  48133  fmtnoprmfac1  48134  fmtnoprmfac2lem1  48135  fmtnoprmfac2  48136  fmtno4prm  48144  2pwp1prm  48158  139prmALT  48165  127prm  48168  sfprmdvdsmersenne  48172  lighneallem1  48174  lighneallem3  48176  proththdlem  48182  proththd  48183  iseven5  48246  oddprmALTV  48269  perfectALTVlem1  48303  perfectALTVlem2  48304  perfectALTV  48305  fppr2odd  48313  2exp340mod341  48315  341fppr2  48316  fpprel2  48323  nnsum3primes4  48370  nnsum3primesgbe  48374  evengpoap3  48381  nnsum4primesevenALTV  48383  bgoldbtbndlem1  48387  tgblthelfgott  48397  gpgusgralem  48638  gpg3nbgrvtx0  48658  gpg3kgrtriexlem2  48666  gpg3kgrtriexlem5  48669  pw2m1lepw2m1  49102  nnpw2even  49111  logbpw2m1  49149  blenpw2  49160  nnpw2pmod  49165  blen2  49167  nnpw2p  49168  nnpw2pb  49169  blennnt2  49171  nnolog2flm1  49172  dig2nn1st  49187  0dig2pr01  49192  dig2nn0  49193  0dig2nn0e  49194  0dig2nn0o  49195  dig2bits  49196  dignn0flhalflem1  49197  dignn0ehalf  49199  dignn0flhalf  49200  nn0sumshdiglemA  49201  nn0sumshdiglemB  49202  nn0sumshdiglem1  49203  nn0sumshdiglem2  49204  nn0mullong  49207  itcovalt2lem2  49258  amgmw2d  50385