Theorem 2nn 9280

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 9177	. 2 ⊢ 2 = (1 + 1)
2		1nn 9129	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 9130	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2302	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2200  (class class class)co 6007  1c1 8008   + caddc 8010  ℕcn 9118  2c2 9169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4202  ax-cnex 8098  ax-resscn 8099  ax-1re 8101  ax-addrcl 8104

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010  df-inn 9119  df-2 9177

This theorem is referenced by:  3nn  9281  2nn0  9394  2z  9482  uz3m2nn  9776  ige2m1fz1  10313  qbtwnre  10484  flhalf  10530  sqeq0  10832  sqeq0d  10902  facavg  10976  bcn2  10994  resqrexlemnm  11537  abs00ap  11581  geo2sum  12033  geo2lim  12035  ege2le3  12190  ef01bndlem  12275  mod2eq0even  12397  mod2eq1n2dvds  12398  bitsdc  12466  bits0o  12469  bitsp1  12470  bitsp1o  12472  bitsfzolem  12473  bitsfzo  12474  bitsmod  12475  bitsfi  12476  bitscmp  12477  bitsinv1lem  12480  bitsinv1  12481  sqgcd  12558  3lcm2e6woprm  12616  prm2orodd  12656  3prm  12658  4nprm  12659  isprm5lem  12671  divgcdodd  12673  isevengcd2  12688  3lcm2e6  12690  pw2dvdslemn  12695  pw2dvds  12696  pw2dvdseulemle  12697  oddpwdclemxy  12699  oddpwdclemodd  12702  oddpwdclemdc  12703  oddpwdc  12704  sqpweven  12705  2sqpwodd  12706  pythagtriplem4  12799  oddprmdvds  12885  4sqlem5  12913  4sqlem6  12914  4sqlem10  12918  4sqlem12  12933  dec2dvds  12942  dec5nprm  12945  dec2nprm  12946  2expltfac  12970  evenennn  12972  exmidunben  13005  plusgndx  13150  plusgid  13151  plusgndxnn  13152  plusgslid  13153  grpstrg  13167  grpbaseg  13168  grpplusgg  13169  rngstrg  13176  lmodstrd  13205  topgrpstrd  13237  dsndx  13256  dsid  13257  dsslid  13258  dsndxnn  13259  slotsdifdsndx  13266  slotsdifunifndx  13273  imasvalstrd  13311  cnfldstr  14530  dveflem  15408  1sgm2ppw  15677  mersenne  15679  perfect1  15680  perfectlem1  15681  perfectlem2  15682  perfect  15683  lgsval  15691  lgsfvalg  15692  lgsfcl2  15693  lgsval2lem  15697  lgsdir2lem2  15716  lgsdir2  15720  gausslemma2dlem1a  15745  gausslemma2dlem1cl  15746  gausslemma2dlem1f1o  15747  gausslemma2dlem4  15751  gausslemma2d  15756  lgseisenlem1  15757  lgseisenlem2  15758  lgseisenlem3  15759  lgseisenlem4  15760  lgsquadlemofi  15763  lgsquadlem1  15764  lgsquadlem2  15765  lgsquad2lem2  15769  m1lgs  15772  2lgslem1c  15777  2lgslem3a1  15784  2lgslem3d1  15787  2lgslem4  15790  2lgs  15791  2sqlem3  15804  2sqlem8  15810  ex-fl  16113  ex-ceil  16114  redcwlpolemeq1  16449  nconstwlpolem0  16458