Theorem 2nn 12305

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 12294	. 2 ⊢ 2 = (1 + 1)
2		1nn 12235	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 12236	. . 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 12224  2c2 12286

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 5251  ax-nul 5261  ax-pr 5395  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 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  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 12225  df-2 12294

This theorem is referenced by:  3nn  12311  0le2  12334  2pos  12336  2ne0  12338  2nn0  12512  2z  12617  uz3m2nn  12909  ige2m1fz1  13635  sqeq0  14147  sqeq0d  14172  expmulnbnd  14262  faclbnd5  14325  bcn2  14346  f1oun2prg  14944  wrdl2exs2  14973  pfx2  14974  wwlktovf  14983  reusq0  15506  climcndslem1  15893  climcndslem2  15894  climcnds  15895  harmonic  15903  geo2sum  15917  geo2lim  15919  ege2le3  16134  ef01bndlem  16230  egt2lt3  16252  nthruc  16298  mod2eq0even  16394  bits0o  16478  bitsp1  16479  bitsfzolem  16482  bitsfzo  16483  bitsmod  16484  bitsfi  16485  bitscmp  16486  bitsinv1lem  16489  bitsinv1  16490  2ebits  16495  bitsinvp1  16497  sadcaddlem  16505  sadadd3  16509  sadaddlem  16514  sadasslem  16518  bitsres  16521  bitsuz  16522  bitsshft  16523  smumullem  16540  smumul  16541  sqgcd  16610  3lcm2e6woprm  16663  prm2orodd  16739  4nprm  16743  prmdvdssq  16767  isevengcd2  16779  3lcm2e6  16781  pythagtriplem4  16869  iserodd  16885  oddprmdvds  16953  prmreclem3  16968  prmreclem5  16970  prmreclem6  16971  4sqlem12  17006  vdwlem3  17033  vdwlem9  17039  vdwlem10  17040  prmo2  17090  dec2dvds  17113  dec5nprm  17116  dec2nprm  17117  2expltfac  17142  5prm  17158  6nprm  17159  7prm  17160  8nprm  17161  10nprmOLD  17164  11prm  17165  17prm  17167  23prm  17169  37prm  17171  43prm  17172  83prm  17173  139prm  17174  163prm  17175  317prm  17176  631prm  17177  1259lem1  17181  1259lem2  17182  1259lem3  17183  1259lem4  17184  1259lem5  17185  1259prm  17186  2503lem1  17187  2503lem2  17188  2503lem3  17189  2503prm  17190  4001lem1  17191  4001lem2  17192  4001lem3  17193  4001lem4  17194  4001prm  17195  plusgndx  17326  plusgid  17327  plusgndxnn  17328  rngstr  17341  lmodstr  17368  topgrpstr  17404  dsndx  17428  dsid  17429  dsndxnn  17430  slotsdifdsndx  17437  slotsdifunifndx  17444  odrngstr  17446  imasvalstr  17494  pmtrprfvalrn  19549  psgnunilem2  19556  psgnprfval  19582  psgnprfval1  19583  cnfldstr  21484  m2detleiblem1  22742  m2detleiblem5  22743  m2detleiblem6  22744  m2detleiblem3  22747  m2detleiblem4  22748  m2detleib  22749  ovollb2lem  25608  ovolunlem1a  25616  ovolunlem1  25617  ovoliunlem1  25622  ovoliunlem3  25624  dyadf  25711  dyadovol  25713  dyadss  25714  dyaddisjlem  25715  dyadmaxlem  25717  opnmbllem  25721  mbfi1fseqlem1  25835  mbfi1fseqlem3  25837  mbfi1fseqlem4  25838  mbfi1fseqlem5  25839  mbfi1fseqlem6  25840  dveflem  26099  aaliou3lem9  26472  quartlem1  26980  quartlem2  26981  zetacvg  27137  lgamgulmlem4  27154  basellem1  27203  basellem2  27204  basellem3  27205  basellem4  27206  basellem5  27207  basellem6  27208  basellem7  27209  basellem8  27210  basellem9  27211  1sgm2ppw  27322  ppiublem1  27324  chtublem  27333  mersenne  27349  perfect1  27350  perfectlem1  27351  perfectlem2  27352  perfect  27353  pcbcctr  27398  bclbnd  27402  bposlem1  27406  bposlem2  27407  bposlem3  27408  bposlem4  27409  bposlem5  27410  bposlem6  27411  bposlem8  27413  lgsdir2lem2  27448  lgsqr  27473  lgsqrmodndvds  27475  gausslemma2dlem1a  27487  gausslemma2d  27496  lgseisenlem1  27497  lgseisenlem2  27498  lgseisenlem3  27499  lgseisenlem4  27500  lgsquadlem1  27502  lgsquadlem2  27503  lgsquad2lem2  27507  2lgslem1c  27515  2lgs  27529  2sqlem3  27542  2sqlem8  27548  chebbnd1lem1  27591  chebbnd1lem3  27593  logdivsum  27655  log2sumbnd  27666  pntlemd  27716  pntlema  27718  pntlemb  27719  pntlemf  27727  pntlemo  27729  ostth2lem1  27740  slotsinbpsd  28668  slotslnbpsd  28669  trkgstr  28671  axlowdimlem6  29206  eengstr  29239  usgrexmplef  29518  cusgrsizeindb0  29708  usgr2pthlem  30021  uspgrn2crct  30066  usgr2wspthons3  30225  clwwlkn2  30304  wwlksext2clwwlk  30317  eupth2lem3lem4  30491  frgrhash2wsp  30592  2clwwlk2clwwlk  30610  dlwwlknondlwlknonf1olem1  30624  clwlknon2num  30628  numclwlk2lem2f1o  30639  ex-xp  30696  ex-cnv  30697  ex-rn  30700  ex-mod  30709  2exple2exp  33091  fldext2rspun  33989  cos9thpiminplylem1  34089  lmat22e11  34125  lmat22e12  34126  lmat22e21  34127  lmat22e22  34128  lmat22det  34129  oddpwdc  34661  eulerpartlemt  34678  eulerpartlemgh  34685  fib0  34706  fib1  34707  fib3  34710  chtvalz  34933  hgt750lem  34955  hgt750lemb  34960  hgt750leme  34962  problem5  36032  bcprod  36101  opnmbllem0  38167  mblfinlem1  38168  dvasin  38215  areacirclem1  38219  heiborlem3  38324  heiborlem5  38326  heiborlem6  38327  heiborlem7  38328  heiborlem8  38329  heibor  38332  12gcd5e1  42632  420gcd8e4  42635  12lcm5e60  42637  60lcm7e420  42639  420lcm8e840  42640  lcm2un  42643  lcmineqlem19  42676  lcmineqlem20  42677  lcmineqlem22  42679  lcmineqlem23  42680  lcmineqlem  42681  3lexlogpow2ineq1  42687  3lexlogpow2ineq2  42688  aks4d1p1p6  42702  aks4d1p1p5  42704  readvrec2  42982  dffltz  43228  flt4lem2  43241  flt4lem5  43244  flt4lem5a  43246  flt4lem5b  43247  flt4lem5c  43248  flt4lem5d  43249  flt4lem5e  43250  flt4lem7  43253  nna4b4nsq  43254  jm2.17a  43549  jm2.17b  43550  jm2.17c  43551  acongrep  43569  acongeq  43572  jm2.27a  43594  jm2.27c  43596  rmydioph  43603  rmxdioph  43605  expdiophlem2  43611  expdioph  43612  frlmpwfi  43687  amgm2d  44786  hashnzfz2  44895  lhe4.4ex1a  44903  limsup10exlem  46344  wallispilem5  46641  wallispi2lem1  46643  wallispi2  46645  stirlinglem3  46648  stirlinglem8  46653  stirlinglem10  46655  stirlinglem15  46660  dirkertrigeqlem3  46672  fouriersw  46803  hoicvrrex  47128  ovnsubaddlem1  47142  ovnsubaddlem2  47143  ovnsubadd2lem  47217  ovolval5lem1  47224  ovolval5lem2  47225  nthrucw  47460  ceilhalfelfzo1  47926  elmod2  47953  fmtnoodd  48140  fmtnof1  48142  fmtnosqrt  48146  fmtnorec4  48156  257prm  48168  odz2prm2pw  48170  fmtnoprmfac1lem  48171  fmtnoprmfac1  48172  fmtnoprmfac2lem1  48173  fmtnoprmfac2  48174  fmtno4prm  48182  2pwp1prm  48196  139prmALT  48203  127prm  48206  sfprmdvdsmersenne  48210  lighneallem1  48212  lighneallem3  48214  proththdlem  48220  proththd  48221  iseven5  48284  oddprmALTV  48307  perfectALTVlem1  48341  perfectALTVlem2  48342  perfectALTV  48343  fppr2odd  48351  2exp340mod341  48353  341fppr2  48354  fpprel2  48361  nnsum3primes4  48408  nnsum3primesgbe  48412  evengpoap3  48419  nnsum4primesevenALTV  48421  bgoldbtbndlem1  48425  tgblthelfgott  48435  gpgusgralem  48676  gpg3nbgrvtx0  48696  gpg3kgrtriexlem2  48704  gpg3kgrtriexlem5  48707  pw2m1lepw2m1  49151  nnpw2even  49160  logbpw2m1  49198  blenpw2  49209  nnpw2pmod  49214  blen2  49216  nnpw2p  49217  nnpw2pb  49218  blennnt2  49220  nnolog2flm1  49221  dig2nn1st  49236  0dig2pr01  49241  dig2nn0  49242  0dig2nn0e  49243  0dig2nn0o  49244  dig2bits  49245  dignn0flhalflem1  49246  dignn0ehalf  49248  dignn0flhalf  49249  nn0sumshdiglemA  49250  nn0sumshdiglemB  49251  nn0sumshdiglem1  49252  nn0sumshdiglem2  49253  nn0mullong  49256  itcovalt2lem2  49307  amgmw2d  50433