Theorem 2nn 12302

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

Syntax hints:   ∈ wcel 2145  (class class class)co 7400  1c1 11089   + caddc 11091  ℕcn 12221  2c2 12283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pr 5394  ax-un 7722  ax-1cn 11146

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5105  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6291  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-om 7851  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-nn 12222  df-2 12291

This theorem is referenced by:  3nn  12308  0le2  12331  2pos  12333  2ne0  12335  2nn0  12509  2z  12614  uz3m2nn  12906  ige2m1fz1  13632  sqeq0  14144  sqeq0d  14169  expmulnbnd  14259  faclbnd5  14322  bcn2  14343  f1oun2prg  14942  wrdl2exs2  14971  pfx2  14972  wwlktovf  14981  reusq0  15504  climcndslem1  15891  climcndslem2  15892  climcnds  15893  harmonic  15901  geo2sum  15915  geo2lim  15917  ege2le3  16132  ef01bndlem  16228  egt2lt3  16250  nthruc  16296  mod2eq0even  16392  bits0o  16476  bitsp1  16477  bitsfzolem  16480  bitsfzo  16481  bitsmod  16482  bitsfi  16483  bitscmp  16484  bitsinv1lem  16487  bitsinv1  16488  2ebits  16493  bitsinvp1  16495  sadcaddlem  16503  sadadd3  16507  sadaddlem  16512  sadasslem  16516  bitsres  16519  bitsuz  16520  bitsshft  16521  smumullem  16538  smumul  16539  sqgcd  16608  3lcm2e6woprm  16661  prm2orodd  16737  4nprm  16741  prmdvdssq  16765  isevengcd2  16777  3lcm2e6  16779  pythagtriplem4  16867  iserodd  16883  oddprmdvds  16951  prmreclem3  16966  prmreclem5  16968  prmreclem6  16969  4sqlem12  17004  vdwlem3  17031  vdwlem9  17037  vdwlem10  17038  prmo2  17088  dec2dvds  17111  dec5nprm  17114  dec2nprm  17115  2expltfac  17140  5prm  17156  6nprm  17157  7prm  17158  8nprm  17159  10nprmOLD  17162  11prm  17163  17prm  17165  23prm  17167  37prm  17169  43prm  17170  83prm  17171  139prm  17172  163prm  17173  317prm  17174  631prm  17175  1259lem1  17179  1259lem2  17180  1259lem3  17181  1259lem4  17182  1259lem5  17183  1259prm  17184  2503lem1  17185  2503lem2  17186  2503lem3  17187  2503prm  17188  4001lem1  17189  4001lem2  17190  4001lem3  17191  4001lem4  17192  4001prm  17193  plusgndx  17324  plusgid  17325  plusgndxnn  17326  rngstr  17339  lmodstr  17366  topgrpstr  17402  dsndx  17426  dsid  17427  dsndxnn  17428  slotsdifdsndx  17435  slotsdifunifndx  17442  odrngstr  17444  imasvalstr  17492  pmtrprfvalrn  19546  psgnunilem2  19553  psgnprfval  19579  psgnprfval1  19580  cnfldstr  21481  m2detleiblem1  22738  m2detleiblem5  22739  m2detleiblem6  22740  m2detleiblem3  22743  m2detleiblem4  22744  m2detleib  22745  ovollb2lem  25604  ovolunlem1a  25612  ovolunlem1  25613  ovoliunlem1  25618  ovoliunlem3  25620  dyadf  25707  dyadovol  25709  dyadss  25710  dyaddisjlem  25711  dyadmaxlem  25713  opnmbllem  25717  mbfi1fseqlem1  25831  mbfi1fseqlem3  25833  mbfi1fseqlem4  25834  mbfi1fseqlem5  25835  mbfi1fseqlem6  25836  dveflem  26095  aaliou3lem9  26468  quartlem1  26976  quartlem2  26977  zetacvg  27133  lgamgulmlem4  27150  basellem1  27199  basellem2  27200  basellem3  27201  basellem4  27202  basellem5  27203  basellem6  27204  basellem7  27205  basellem8  27206  basellem9  27207  1sgm2ppw  27318  ppiublem1  27320  chtublem  27329  mersenne  27345  perfect1  27346  perfectlem1  27347  perfectlem2  27348  perfect  27349  pcbcctr  27394  bclbnd  27398  bposlem1  27402  bposlem2  27403  bposlem3  27404  bposlem4  27405  bposlem5  27406  bposlem6  27407  bposlem8  27409  lgsdir2lem2  27444  lgsqr  27469  lgsqrmodndvds  27471  gausslemma2dlem1a  27483  gausslemma2d  27492  lgseisenlem1  27493  lgseisenlem2  27494  lgseisenlem3  27495  lgseisenlem4  27496  lgsquadlem1  27498  lgsquadlem2  27499  lgsquad2lem2  27503  2lgslem1c  27511  2lgs  27525  2sqlem3  27538  2sqlem8  27544  chebbnd1lem1  27587  chebbnd1lem3  27589  logdivsum  27651  log2sumbnd  27662  pntlemd  27712  pntlema  27714  pntlemb  27715  pntlemf  27723  pntlemo  27725  ostth2lem1  27736  slotsinbpsd  28664  slotslnbpsd  28665  trkgstr  28667  axlowdimlem6  29202  eengstr  29235  usgrexmplef  29514  cusgrsizeindb0  29704  usgr2pthlem  30017  uspgrn2crct  30062  usgr2wspthons3  30221  clwwlkn2  30300  wwlksext2clwwlk  30313  eupth2lem3lem4  30487  frgrhash2wsp  30588  2clwwlk2clwwlk  30606  dlwwlknondlwlknonf1olem1  30620  clwlknon2num  30624  numclwlk2lem2f1o  30635  ex-xp  30692  ex-cnv  30693  ex-rn  30696  ex-mod  30705  2exple2exp  33086  fldext2rspun  33984  cos9thpiminplylem1  34084  lmat22e11  34120  lmat22e12  34121  lmat22e21  34122  lmat22e22  34123  lmat22det  34124  oddpwdc  34656  eulerpartlemt  34673  eulerpartlemgh  34680  fib0  34701  fib1  34702  fib3  34705  chtvalz  34928  hgt750lem  34950  hgt750lemb  34955  hgt750leme  34957  problem5  36027  bcprod  36096  opnmbllem0  38162  mblfinlem1  38163  dvasin  38210  areacirclem1  38214  heiborlem3  38319  heiborlem5  38321  heiborlem6  38322  heiborlem7  38323  heiborlem8  38324  heibor  38327  12gcd5e1  42627  420gcd8e4  42630  12lcm5e60  42632  60lcm7e420  42634  420lcm8e840  42635  lcm2un  42638  lcmineqlem19  42671  lcmineqlem20  42672  lcmineqlem22  42674  lcmineqlem23  42675  lcmineqlem  42676  3lexlogpow2ineq1  42682  3lexlogpow2ineq2  42683  aks4d1p1p6  42697  aks4d1p1p5  42699  readvrec2  42977  dffltz  43223  flt4lem2  43236  flt4lem5  43239  flt4lem5a  43241  flt4lem5b  43242  flt4lem5c  43243  flt4lem5d  43244  flt4lem5e  43245  flt4lem7  43248  nna4b4nsq  43249  jm2.17a  43544  jm2.17b  43545  jm2.17c  43546  acongrep  43564  acongeq  43567  jm2.27a  43589  jm2.27c  43591  rmydioph  43598  rmxdioph  43600  expdiophlem2  43606  expdioph  43607  frlmpwfi  43682  amgm2d  44781  hashnzfz2  44890  lhe4.4ex1a  44898  limsup10exlem  46345  wallispilem5  46642  wallispi2lem1  46644  wallispi2  46646  stirlinglem3  46649  stirlinglem8  46654  stirlinglem10  46656  stirlinglem15  46661  dirkertrigeqlem3  46673  fouriersw  46804  hoicvrrex  47129  ovnsubaddlem1  47143  ovnsubaddlem2  47144  ovnsubadd2lem  47218  ovolval5lem1  47225  ovolval5lem2  47226  nthrucw  47461  ceilhalfelfzo1  47927  elmod2  47954  fmtnoodd  48141  fmtnof1  48143  fmtnosqrt  48147  fmtnorec4  48157  257prm  48169  odz2prm2pw  48171  fmtnoprmfac1lem  48172  fmtnoprmfac1  48173  fmtnoprmfac2lem1  48174  fmtnoprmfac2  48175  fmtno4prm  48183  2pwp1prm  48197  139prmALT  48204  127prm  48207  sfprmdvdsmersenne  48211  lighneallem1  48213  lighneallem3  48215  proththdlem  48221  proththd  48222  iseven5  48285  oddprmALTV  48308  perfectALTVlem1  48342  perfectALTVlem2  48343  perfectALTV  48344  fppr2odd  48352  2exp340mod341  48354  341fppr2  48355  fpprel2  48362  nnsum3primes4  48409  nnsum3primesgbe  48413  evengpoap3  48420  nnsum4primesevenALTV  48422  bgoldbtbndlem1  48426  tgblthelfgott  48436  gpgusgralem  48677  gpg3nbgrvtx0  48697  gpg3kgrtriexlem2  48705  gpg3kgrtriexlem5  48708  pw2m1lepw2m1  49152  nnpw2even  49161  logbpw2m1  49199  blenpw2  49210  nnpw2pmod  49215  blen2  49217  nnpw2p  49218  nnpw2pb  49219  blennnt2  49221  nnolog2flm1  49222  dig2nn1st  49237  0dig2pr01  49242  dig2nn0  49243  0dig2nn0e  49244  0dig2nn0o  49245  dig2bits  49246  dignn0flhalflem1  49247  dignn0ehalf  49249  dignn0flhalf  49250  nn0sumshdiglemA  49251  nn0sumshdiglemB  49252  nn0sumshdiglem1  49253  nn0sumshdiglem2  49254  nn0mullong  49257  itcovalt2lem2  49308  amgmw2d  50434