Theorem 2nn 12219

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7353  1c1 11029   + caddc 11031  ℕcn 12146  2c2 12201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675  ax-1cn 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12147  df-2 12209

This theorem is referenced by:  3nn  12225  2ne0  12250  2nn0  12419  2z  12525  uz3m2nn  12813  ige2m1fz1  13537  sqeq0  14045  sqeq0d  14070  expmulnbnd  14160  faclbnd5  14223  bcn2  14244  f1oun2prg  14842  wrdl2exs2  14871  pfx2  14872  wwlktovf  14881  reusq0  15390  climcndslem1  15774  climcndslem2  15775  climcnds  15776  harmonic  15784  geo2sum  15798  geo2lim  15800  ege2le3  16015  ef01bndlem  16111  egt2lt3  16133  nthruc  16179  mod2eq0even  16275  bits0o  16359  bitsp1  16360  bitsfzolem  16363  bitsfzo  16364  bitsmod  16365  bitsfi  16366  bitscmp  16367  bitsinv1lem  16370  bitsinv1  16371  2ebits  16376  bitsinvp1  16378  sadcaddlem  16386  sadadd3  16390  sadaddlem  16395  sadasslem  16399  bitsres  16402  bitsuz  16403  bitsshft  16404  smumullem  16421  smumul  16422  sqgcd  16491  3lcm2e6woprm  16544  prm2orodd  16620  4nprm  16624  prmdvdssq  16647  isevengcd2  16659  3lcm2e6  16661  pythagtriplem4  16749  iserodd  16765  oddprmdvds  16833  prmreclem3  16848  prmreclem5  16850  prmreclem6  16851  4sqlem12  16886  vdwlem3  16913  vdwlem9  16919  vdwlem10  16920  prmo2  16970  dec2dvds  16993  dec5nprm  16996  dec2nprm  16997  2expltfac  17022  5prm  17038  6nprm  17039  7prm  17040  8nprm  17041  10nprm  17043  11prm  17044  17prm  17046  23prm  17048  37prm  17050  43prm  17051  83prm  17052  139prm  17053  163prm  17054  317prm  17055  631prm  17056  1259lem1  17060  1259lem2  17061  1259lem3  17062  1259lem4  17063  1259lem5  17064  1259prm  17065  2503lem1  17066  2503lem2  17067  2503lem3  17068  2503prm  17069  4001lem1  17070  4001lem2  17071  4001lem3  17072  4001lem4  17073  4001prm  17074  plusgndx  17205  plusgid  17206  plusgndxnn  17207  rngstr  17220  lmodstr  17247  topgrpstr  17283  dsndx  17307  dsid  17308  dsndxnn  17309  slotsdifdsndx  17316  slotsdifunifndx  17323  odrngstr  17325  imasvalstr  17373  pmtrprfvalrn  19385  psgnunilem2  19392  psgnprfval  19418  psgnprfval1  19419  cnfldstr  21281  cnfldstrOLD  21296  m2detleiblem1  22527  m2detleiblem5  22528  m2detleiblem6  22529  m2detleiblem3  22532  m2detleiblem4  22533  m2detleib  22534  ovollb2lem  25405  ovolunlem1a  25413  ovolunlem1  25414  ovoliunlem1  25419  ovoliunlem3  25421  dyadf  25508  dyadovol  25510  dyadss  25511  dyaddisjlem  25512  dyadmaxlem  25514  opnmbllem  25518  mbfi1fseqlem1  25632  mbfi1fseqlem3  25634  mbfi1fseqlem4  25635  mbfi1fseqlem5  25636  mbfi1fseqlem6  25637  dveflem  25899  aaliou3lem9  26274  quartlem1  26783  quartlem2  26784  zetacvg  26941  lgamgulmlem4  26958  basellem1  27007  basellem2  27008  basellem3  27009  basellem4  27010  basellem5  27011  basellem6  27012  basellem7  27013  basellem8  27014  basellem9  27015  1sgm2ppw  27127  ppiublem1  27129  chtublem  27138  mersenne  27154  perfect1  27155  perfectlem1  27156  perfectlem2  27157  perfect  27158  pcbcctr  27203  bclbnd  27207  bposlem1  27211  bposlem2  27212  bposlem3  27213  bposlem4  27214  bposlem5  27215  bposlem6  27216  bposlem8  27218  lgsdir2lem2  27253  lgsqr  27278  lgsqrmodndvds  27280  gausslemma2dlem1a  27292  gausslemma2d  27301  lgseisenlem1  27302  lgseisenlem2  27303  lgseisenlem3  27304  lgseisenlem4  27305  lgsquadlem1  27307  lgsquadlem2  27308  lgsquad2lem2  27312  2lgslem1c  27320  2lgs  27334  2sqlem3  27347  2sqlem8  27353  chebbnd1lem1  27396  chebbnd1lem3  27398  logdivsum  27460  log2sumbnd  27471  pntlemd  27521  pntlema  27523  pntlemb  27524  pntlemf  27532  pntlemo  27534  ostth2lem1  27545  slotsinbpsd  28404  slotslnbpsd  28405  trkgstr  28407  axlowdimlem6  28910  eengstr  28943  usgrexmplef  29222  cusgrsizeindb0  29413  usgr2pthlem  29726  uspgrn2crct  29771  usgr2wspthons3  29927  clwwlkn2  30006  wwlksext2clwwlk  30019  eupth2lem3lem4  30193  frgrhash2wsp  30294  2clwwlk2clwwlk  30312  dlwwlknondlwlknonf1olem1  30326  clwlknon2num  30330  numclwlk2lem2f1o  30341  ex-xp  30398  ex-cnv  30399  ex-rn  30402  ex-mod  30411  2exple2exp  32803  fldext2rspun  33656  cos9thpiminplylem1  33751  lmat22e11  33787  lmat22e12  33788  lmat22e21  33789  lmat22e22  33790  lmat22det  33791  oddpwdc  34324  eulerpartlemt  34341  eulerpartlemgh  34348  fib0  34369  fib1  34370  fib3  34373  chtvalz  34599  hgt750lem  34621  hgt750lemb  34626  hgt750leme  34628  problem5  35644  bcprod  35713  opnmbllem0  37638  mblfinlem1  37639  dvasin  37686  areacirclem1  37690  heiborlem3  37795  heiborlem5  37797  heiborlem6  37798  heiborlem7  37799  heiborlem8  37800  heibor  37803  12gcd5e1  41979  420gcd8e4  41982  12lcm5e60  41984  60lcm7e420  41986  420lcm8e840  41987  lcm2un  41990  lcmineqlem19  42023  lcmineqlem20  42024  lcmineqlem22  42026  lcmineqlem23  42027  lcmineqlem  42028  3lexlogpow2ineq1  42034  3lexlogpow2ineq2  42035  aks4d1p1p6  42049  aks4d1p1p5  42051  readvrec2  42337  dffltz  42610  flt4lem2  42623  flt4lem5  42626  flt4lem5a  42628  flt4lem5b  42629  flt4lem5c  42630  flt4lem5d  42631  flt4lem5e  42632  flt4lem7  42635  nna4b4nsq  42636  jm2.17a  42936  jm2.17b  42937  jm2.17c  42938  acongrep  42956  acongeq  42959  jm2.27a  42981  jm2.27c  42983  rmydioph  42990  rmxdioph  42992  expdiophlem2  42998  expdioph  42999  frlmpwfi  43074  amgm2d  44174  hashnzfz2  44297  lhe4.4ex1a  44305  limsup10exlem  45757  wallispilem5  46054  wallispi2lem1  46056  wallispi2  46058  stirlinglem3  46061  stirlinglem8  46066  stirlinglem10  46068  stirlinglem15  46073  dirkertrigeqlem3  46085  fouriersw  46216  hoicvrrex  46541  ovnsubaddlem1  46555  ovnsubaddlem2  46556  ovnsubadd2lem  46630  ovolval5lem1  46637  ovolval5lem2  46638  ceilhalfelfzo1  47318  elmod2  47343  fmtnoodd  47521  fmtnof1  47523  fmtnosqrt  47527  fmtnorec4  47537  257prm  47549  odz2prm2pw  47551  fmtnoprmfac1lem  47552  fmtnoprmfac1  47553  fmtnoprmfac2lem1  47554  fmtnoprmfac2  47555  fmtno4prm  47563  2pwp1prm  47577  139prmALT  47584  127prm  47587  sfprmdvdsmersenne  47591  lighneallem1  47593  lighneallem3  47595  proththdlem  47601  proththd  47602  iseven5  47652  oddprmALTV  47675  perfectALTVlem1  47709  perfectALTVlem2  47710  perfectALTV  47711  fppr2odd  47719  2exp340mod341  47721  341fppr2  47722  fpprel2  47729  nnsum3primes4  47776  nnsum3primesgbe  47780  evengpoap3  47787  nnsum4primesevenALTV  47789  bgoldbtbndlem1  47793  tgblthelfgott  47803  gpgusgralem  48044  gpg3nbgrvtx0  48064  gpg3kgrtriexlem2  48072  gpg3kgrtriexlem5  48075  pw2m1lepw2m1  48509  nnpw2even  48518  logbpw2m1  48556  blenpw2  48567  nnpw2pmod  48572  blen2  48574  nnpw2p  48575  nnpw2pb  48576  blennnt2  48578  nnolog2flm1  48579  dig2nn1st  48594  0dig2pr01  48599  dig2nn0  48600  0dig2nn0e  48601  0dig2nn0o  48602  dig2bits  48603  dignn0flhalflem1  48604  dignn0ehalf  48606  dignn0flhalf  48607  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0sumshdiglem1  48610  nn0sumshdiglem2  48611  nn0mullong  48614  itcovalt2lem2  48665  amgmw2d  49793