Theorem 2nn 9445

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 9342	. 2 ⊢ 2 = (1 + 1)
2		1nn 9294	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 9295	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2311	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2209  (class class class)co 6075  1c1 8170   + caddc 8172  ℕcn 9283  2c2 9334

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4244  ax-cnex 8260  ax-resscn 8261  ax-1re 8263  ax-addrcl 8266

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-int 3966  df-br 4126  df-iota 5332  df-fv 5380  df-ov 6078  df-inn 9284  df-2 9342

This theorem is referenced by:  3nn  9446  2nn0  9559  2z  9651  uz3m2nn  9952  ige2m1fz1  10494  qbtwnre  10669  flhalf  10715  sqeq0  11017  sqeq0d  11088  facavg  11162  bcn2  11180  resqrexlemnm  11762  abs00ap  11806  geo2sum  12259  geo2lim  12261  ege2le3  12416  ef01bndlem  12501  mod2eq0even  12623  mod2eq1n2dvds  12624  bitsdc  12692  bits0o  12695  bitsp1  12696  bitsp1o  12698  bitsfzolem  12699  bitsfzo  12700  bitsmod  12701  bitsfi  12702  bitscmp  12703  bitsinv1lem  12706  bitsinv1  12707  sqgcd  12784  3lcm2e6woprm  12842  prm2orodd  12882  3prm  12884  4nprm  12885  isprm5lem  12897  divgcdodd  12899  isevengcd2  12914  3lcm2e6  12916  pw2dvdslemn  12921  pw2dvds  12922  pw2dvdseulemle  12923  oddpwdclemxy  12925  oddpwdclemodd  12928  oddpwdclemdc  12929  oddpwdc  12930  sqpweven  12931  2sqpwodd  12932  pythagtriplem4  13025  oddprmdvds  13111  4sqlem5  13139  4sqlem6  13140  4sqlem10  13144  4sqlem12  13159  dec2dvds  13168  dec5nprm  13171  dec2nprm  13172  2expltfac  13196  evenennn  13262  exmidunben  13295  plusgndx  13440  plusgid  13441  plusgndxnn  13442  plusgslid  13443  grpstrg  13457  grpbaseg  13458  grpplusgg  13459  rngstrg  13466  lmodstrd  13495  topgrpstrd  13527  dsndx  13546  dsid  13547  dsslid  13548  dsndxnn  13549  slotsdifdsndx  13556  slotsdifunifndx  13563  imasvalstrd  13596  cnfldstr  14867  dveflem  15750  1sgm2ppw  16023  mersenne  16025  perfect1  16026  perfectlem1  16027  perfectlem2  16028  perfect  16029  lgsval  16037  lgsfvalg  16038  lgsfcl2  16039  lgsval2lem  16043  lgsdir2lem2  16062  lgsdir2  16066  gausslemma2dlem1a  16091  gausslemma2dlem1cl  16092  gausslemma2dlem1f1o  16093  gausslemma2dlem4  16097  gausslemma2d  16102  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem3  16105  lgseisenlem4  16106  lgsquadlemofi  16109  lgsquadlem1  16110  lgsquadlem2  16111  lgsquad2lem2  16115  m1lgs  16118  2lgslem1c  16123  2lgslem3a1  16130  2lgslem3d1  16133  2lgslem4  16136  2lgs  16137  2sqlem3  16150  2sqlem8  16156  clwwlkn2  16576  eupth2lem3lem4fi  16628  konigsberglem5  16647  ex-fl  16653  ex-ceil  16654  redcwlpolemeq1  17009  nconstwlpolem0  17018