Theorem 2nn 9180

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 9077	. 2 ⊢ 2 = (1 + 1)
2		1nn 9029	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 9030	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2277	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2175  (class class class)co 5934  1c1 7908   + caddc 7910  ℕcn 9018  2c2 9069

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-sep 4161  ax-cnex 7998  ax-resscn 7999  ax-1re 8001  ax-addrcl 8004

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-v 2773  df-un 3169  df-in 3171  df-ss 3178  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-int 3885  df-br 4044  df-iota 5229  df-fv 5276  df-ov 5937  df-inn 9019  df-2 9077

This theorem is referenced by:  3nn  9181  2nn0  9294  2z  9382  uz3m2nn  9676  ige2m1fz1  10213  qbtwnre  10380  flhalf  10426  sqeq0  10728  sqeq0d  10798  facavg  10872  bcn2  10890  resqrexlemnm  11248  abs00ap  11292  geo2sum  11744  geo2lim  11746  ege2le3  11901  ef01bndlem  11986  mod2eq0even  12108  mod2eq1n2dvds  12109  bitsdc  12177  bits0o  12180  bitsp1  12181  bitsp1o  12183  bitsfzolem  12184  bitsfzo  12185  bitsmod  12186  bitsfi  12187  bitscmp  12188  bitsinv1lem  12191  bitsinv1  12192  sqgcd  12269  3lcm2e6woprm  12327  prm2orodd  12367  3prm  12369  4nprm  12370  isprm5lem  12382  divgcdodd  12384  isevengcd2  12399  3lcm2e6  12401  pw2dvdslemn  12406  pw2dvds  12407  pw2dvdseulemle  12408  oddpwdclemxy  12410  oddpwdclemodd  12413  oddpwdclemdc  12414  oddpwdc  12415  sqpweven  12416  2sqpwodd  12417  pythagtriplem4  12510  oddprmdvds  12596  4sqlem5  12624  4sqlem6  12625  4sqlem10  12629  4sqlem12  12644  dec2dvds  12653  dec5nprm  12656  dec2nprm  12657  2expltfac  12681  evenennn  12683  exmidunben  12716  plusgndx  12860  plusgid  12861  plusgndxnn  12862  plusgslid  12863  grpstrg  12876  grpbaseg  12877  grpplusgg  12878  rngstrg  12885  lmodstrd  12914  topgrpstrd  12946  dsndx  12965  dsid  12966  dsslid  12967  dsndxnn  12968  slotsdifdsndx  12975  slotsdifunifndx  12982  imasvalstrd  13020  cnfldstr  14238  dveflem  15116  1sgm2ppw  15385  mersenne  15387  perfect1  15388  perfectlem1  15389  perfectlem2  15390  perfect  15391  lgsval  15399  lgsfvalg  15400  lgsfcl2  15401  lgsval2lem  15405  lgsdir2lem2  15424  lgsdir2  15428  gausslemma2dlem1a  15453  gausslemma2dlem1cl  15454  gausslemma2dlem1f1o  15455  gausslemma2dlem4  15459  gausslemma2d  15464  lgseisenlem1  15465  lgseisenlem2  15466  lgseisenlem3  15467  lgseisenlem4  15468  lgsquadlemofi  15471  lgsquadlem1  15472  lgsquadlem2  15473  lgsquad2lem2  15477  m1lgs  15480  2lgslem1c  15485  2lgslem3a1  15492  2lgslem3d1  15495  2lgslem4  15498  2lgs  15499  2sqlem3  15512  2sqlem8  15518  ex-fl  15525  ex-ceil  15526  redcwlpolemeq1  15857  nconstwlpolem0  15866