Theorem 2nn 9466

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

This proof depends on syntax axioms:   ∈ wcel 2209  (class class class)co 6085  1c1 8180   + caddc 8182  ℕcn 9304  2c2 9355

This proof depends on 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 4249  ax-cnex 8270  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276

This proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088  df-inn 9305  df-2 9363

This theorem is used by:  3nn  9467  2nn0  9580  2z  9672  uz3m2nn  9973  ige2m1fz1  10516  qbtwnre  10691  flhalf  10737  sqeq0  11039  sqeq0d  11110  facavg  11184  bcn2  11202  resqrexlemnm  11784  abs00ap  11828  geo2sum  12281  geo2lim  12283  ege2le3  12438  ef01bndlem  12523  mod2eq0even  12645  mod2eq1n2dvds  12646  bitsdc  12714  bits0o  12717  bitsp1  12718  bitsp1o  12720  bitsfzolem  12721  bitsfzo  12722  bitsmod  12723  bitsfi  12724  bitscmp  12725  bitsinv1lem  12728  bitsinv1  12729  sqgcd  12806  3lcm2e6woprm  12864  prm2orodd  12904  3prm  12906  4nprm  12907  isprm5lem  12919  divgcdodd  12921  isevengcd2  12936  3lcm2e6  12938  pw2dvdslemn  12943  pw2dvds  12944  pw2dvdseulemle  12945  oddpwdclemxy  12947  oddpwdclemodd  12950  oddpwdclemdc  12951  oddpwdc  12952  sqpweven  12953  2sqpwodd  12954  pythagtriplem4  13047  oddprmdvds  13133  4sqlem5  13161  4sqlem6  13162  4sqlem10  13166  4sqlem12  13181  dec2dvds  13190  dec5nprm  13193  dec2nprm  13194  2expltfac  13218  evenennn  13284  exmidunben  13317  plusgndx  13463  plusgid  13464  plusgndxnn  13465  plusgslid  13466  grpstrg  13480  grpbaseg  13481  grpplusgg  13482  rngstrg  13489  lmodstrd  13518  topgrpstrd  13550  dsndx  13569  dsid  13570  dsslid  13571  dsndxnn  13572  slotsdifdsndx  13579  slotsdifunifndx  13586  imasvalstrd  13619  cnfldstr  14895  dveflem  15827  1sgm2ppw  16109  mersenne  16111  perfect1  16112  perfectlem1  16113  perfectlem2  16114  perfect  16115  lgsval  16123  lgsfvalg  16124  lgsfcl2  16125  lgsval2lem  16129  lgsdir2lem2  16148  lgsdir2  16152  gausslemma2dlem1a  16177  gausslemma2dlem1cl  16178  gausslemma2dlem1f1o  16179  gausslemma2dlem4  16183  gausslemma2d  16188  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem3  16191  lgseisenlem4  16192  lgsquadlemofi  16195  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2lem2  16201  m1lgs  16204  2lgslem1c  16209  2lgslem3a1  16216  2lgslem3d1  16219  2lgslem4  16222  2lgs  16223  2sqlem3  16236  2sqlem8  16242  clwwlkn2  16662  eupth2lem3lem4fi  16714  konigsberglem5  16733  ex-fl  16739  ex-ceil  16740  redcwlpolemeq1  17104  nconstwlpolem0  17113