Theorem 2nn 11185

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 11079	. 2 ⊢ 2 = (1 + 1)
2		1nn 11031	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 11032	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2697	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 1990  (class class class)co 6650  1c1 9937   + caddc 9939  ℕcn 11020  2c2 11070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-1cn 9994

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-nn 11021  df-2 11079

This theorem is referenced by:  3nn  11186  2nn0  11309  2z  11409  uz3m2nn  11731  ige2m1fz1  12429  sqeq0  12927  expmulnbnd  12996  sqeq0d  13007  faclbnd5  13085  bcn2  13106  f1oun2prg  13662  wrdl2exs2  13690  wwlktovf  13699  climcndslem1  14581  climcndslem2  14582  climcnds  14583  harmonic  14591  geo2sum  14604  geo2lim  14606  ege2le3  14820  ef01bndlem  14914  egt2lt3  14934  nthruc  14981  mod2eq0even  15070  bits0o  15152  bitsp1  15153  bitsfzolem  15156  bitsfzo  15157  bitsmod  15158  bitsfi  15159  bitscmp  15160  bitsinv1lem  15163  bitsinv1  15164  2ebits  15169  bitsinvp1  15171  sadcaddlem  15179  sadadd3  15183  sadaddlem  15188  sadasslem  15192  bitsres  15195  bitsuz  15196  bitsshft  15197  smumullem  15214  smumul  15215  sqgcd  15278  3lcm2e6woprm  15328  prm2orodd  15404  3prm  15406  4nprm  15407  isevengcd2  15438  3lcm2e6  15440  pythagtriplem4  15524  iserodd  15540  oddprmdvds  15607  prmreclem3  15622  prmreclem5  15624  prmreclem6  15625  4sqlem12  15660  vdwlem3  15687  vdwlem9  15693  vdwlem10  15694  prmo2  15744  dec2dvds  15767  dec5nprm  15770  dec2nprm  15771  2expltfac  15799  5prm  15815  6nprm  15816  7prm  15817  8nprm  15818  10nprm  15820  10nprmOLD  15821  11prm  15822  17prm  15824  23prm  15826  37prm  15828  43prm  15829  83prm  15830  139prm  15831  163prm  15832  317prm  15833  631prm  15834  1259lem1  15838  1259lem2  15839  1259lem3  15840  1259lem4  15841  1259lem5  15842  1259prm  15843  2503lem1  15844  2503lem2  15845  2503lem3  15846  2503prm  15847  4001lem1  15848  4001lem2  15849  4001lem3  15850  4001lem4  15851  4001prm  15852  plusgndx  15976  plusgid  15977  grpstr  15990  grpbase  15991  grpplusg  15992  ressplusg  15993  rngstr  16000  lmodstr  16017  topgrpstr  16042  dsndx  16062  dsid  16063  odrngstr  16066  ressds  16073  imasvalstr  16112  pmtrprfvalrn  17908  psgnunilem2  17915  psgnprfval  17941  psgnprfval1  17942  mgpds  18499  oppradd  18630  sraaddg  19179  srads  19186  opsrplusg  19480  cnfldstr  19748  cnfldfun  19758  zlmplusg  19867  znadd  19889  m2detleiblem1  20430  m2detleiblem5  20431  m2detleiblem6  20432  m2detleiblem3  20435  m2detleiblem4  20436  m2detleib  20437  tmslem  22287  tngplusg  22446  ovollb2lem  23256  ovolunlem1a  23264  ovolunlem1  23265  ovoliunlem1  23270  ovoliunlem3  23272  dyadf  23359  dyadovol  23361  dyadss  23362  dyaddisjlem  23363  dyadmaxlem  23365  opnmbllem  23369  mbfi1fseqlem1  23482  mbfi1fseqlem3  23484  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  mbfi1fseqlem6  23487  dveflem  23742  aaliou3lem9  24105  dcubic1lem  24570  dcubic2  24571  mcubic  24574  quartlem1  24584  quartlem2  24585  zetacvg  24741  lgamgulmlem4  24758  basellem1  24807  basellem2  24808  basellem3  24809  basellem4  24810  basellem5  24811  basellem6  24812  basellem7  24813  basellem8  24814  basellem9  24815  1sgm2ppw  24925  ppiublem1  24927  chtublem  24936  mersenne  24952  perfect1  24953  perfectlem1  24954  perfectlem2  24955  perfect  24956  pcbcctr  25001  bclbnd  25005  bposlem1  25009  bposlem2  25010  bposlem3  25011  bposlem4  25012  bposlem5  25013  bposlem6  25014  bposlem8  25016  lgsdir2lem2  25051  lgsqr  25076  lgsqrmodndvds  25078  gausslemma2dlem1a  25090  gausslemma2d  25099  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgseisenlem4  25103  lgsquadlem1  25105  lgsquadlem2  25106  lgsquad2lem2  25110  2lgslem1c  25118  2lgs  25132  2sqlem3  25145  2sqlem8  25151  chebbnd1lem1  25158  chebbnd1lem3  25160  logdivsum  25222  log2sumbnd  25233  pntlemd  25283  pntlema  25285  pntlemb  25286  pntlemf  25294  pntlemo  25296  ostth2lem1  25307  trkgstr  25343  ttgplusg  25758  ttgds  25761  axlowdimlem6  25827  eengstr  25860  usgrexmplef  26151  cusgrsizeindb0  26345  usgr2pthlem  26659  uspgrn2crct  26700  usgr2wspthons3  26857  clwwlksn2  26910  wwlksext2clwwlk  26924  eupth2lem3lem4  27091  frgrhash2wsp  27196  numclwwlkovf2  27217  numclwwlk2lem1  27235  numclwlk2lem2f  27236  numclwlk2lem2f1o  27238  ex-xp  27293  ex-cnv  27294  ex-rn  27297  ex-mod  27306  resvplusg  29833  lmat22e11  29884  lmat22e12  29885  lmat22e21  29886  lmat22e22  29887  lmat22det  29888  oddpwdc  30416  eulerpartlemt  30433  eulerpartlemgh  30440  fib0  30461  fib1  30462  fib3  30465  chtvalz  30707  hgt750lem  30729  hgt750lemb  30734  hgt750leme  30736  problem5  31563  bcprod  31624  opnmbllem0  33445  mblfinlem1  33446  dvasin  33496  areacirclem1  33500  heiborlem3  33612  heiborlem5  33614  heiborlem6  33615  heiborlem7  33616  heiborlem8  33617  heibor  33620  hlhilsplus  37232  jm2.17a  37527  jm2.17b  37528  jm2.17c  37529  acongrep  37547  acongeq  37550  jm2.27a  37572  jm2.27c  37574  rmydioph  37581  rmxdioph  37583  expdiophlem2  37589  expdioph  37590  frlmpwfi  37668  amgm2d  38501  hashnzfz2  38520  lhe4.4ex1a  38528  limsup10exlem  40004  wallispilem5  40286  wallispi2lem1  40288  wallispi2  40290  stirlinglem3  40293  stirlinglem8  40298  stirlinglem10  40300  stirlinglem15  40305  dirkertrigeqlem3  40317  fouriersw  40448  hoicvrrex  40770  ovnsubaddlem1  40784  ovnsubaddlem2  40785  ovnsubadd2lem  40859  ovolval5lem1  40866  ovolval5lem2  40867  elmod2  41340  pfx2  41412  fmtnoodd  41445  fmtnof1  41447  fmtnosqrt  41451  fmtnorec4  41461  257prm  41473  odz2prm2pw  41475  fmtnoprmfac1lem  41476  fmtnoprmfac1  41477  fmtnoprmfac2lem1  41478  fmtnoprmfac2  41479  fmtno4prm  41487  2pwp1prm  41503  139prmALT  41511  127prm  41515  sfprmdvdsmersenne  41520  lighneallem1  41522  lighneallem3  41524  proththdlem  41530  proththd  41531  iseven5  41576  oddprmALTV  41598  perfectALTVlem1  41630  perfectALTVlem2  41631  perfectALTV  41632  nnsum3primes4  41676  nnsum3primesgbe  41680  evengpoap3  41687  nnsum4primesevenALTV  41689  bgoldbtbndlem1  41693  tgblthelfgott  41703  tgblthelfgottOLD  41709  pw2m1lepw2m1  42310  nnpw2even  42323  logbpw2m1  42361  blenpw2  42372  nnpw2pmod  42377  blen2  42379  nnpw2p  42380  nnpw2pb  42381  blennnt2  42383  nnolog2flm1  42384  dig2nn1st  42399  0dig2pr01  42404  dig2nn0  42405  0dig2nn0e  42406  0dig2nn0o  42407  dig2bits  42408  dignn0flhalflem1  42409  dignn0ehalf  42411  dignn0flhalf  42412  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414  nn0sumshdiglem1  42415  nn0sumshdiglem2  42416  nn0mullong  42419  amgmw2d  42550