Theorem 2nn 9305

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 9202	. 2 ⊢ 2 = (1 + 1)
2		1nn 9154	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 9155	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2304	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2202  (class class class)co 6018  1c1 8033   + caddc 8035  ℕcn 9143  2c2 9194

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8123  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021  df-inn 9144  df-2 9202

This theorem is referenced by:  3nn  9306  2nn0  9419  2z  9507  uz3m2nn  9807  ige2m1fz1  10344  qbtwnre  10517  flhalf  10563  sqeq0  10865  sqeq0d  10935  facavg  11009  bcn2  11027  resqrexlemnm  11583  abs00ap  11627  geo2sum  12080  geo2lim  12082  ege2le3  12237  ef01bndlem  12322  mod2eq0even  12444  mod2eq1n2dvds  12445  bitsdc  12513  bits0o  12516  bitsp1  12517  bitsp1o  12519  bitsfzolem  12520  bitsfzo  12521  bitsmod  12522  bitsfi  12523  bitscmp  12524  bitsinv1lem  12527  bitsinv1  12528  sqgcd  12605  3lcm2e6woprm  12663  prm2orodd  12703  3prm  12705  4nprm  12706  isprm5lem  12718  divgcdodd  12720  isevengcd2  12735  3lcm2e6  12737  pw2dvdslemn  12742  pw2dvds  12743  pw2dvdseulemle  12744  oddpwdclemxy  12746  oddpwdclemodd  12749  oddpwdclemdc  12750  oddpwdc  12751  sqpweven  12752  2sqpwodd  12753  pythagtriplem4  12846  oddprmdvds  12932  4sqlem5  12960  4sqlem6  12961  4sqlem10  12965  4sqlem12  12980  dec2dvds  12989  dec5nprm  12992  dec2nprm  12993  2expltfac  13017  evenennn  13019  exmidunben  13052  plusgndx  13197  plusgid  13198  plusgndxnn  13199  plusgslid  13200  grpstrg  13214  grpbaseg  13215  grpplusgg  13216  rngstrg  13223  lmodstrd  13252  topgrpstrd  13284  dsndx  13303  dsid  13304  dsslid  13305  dsndxnn  13306  slotsdifdsndx  13313  slotsdifunifndx  13320  imasvalstrd  13358  cnfldstr  14578  dveflem  15456  1sgm2ppw  15725  mersenne  15727  perfect1  15728  perfectlem1  15729  perfectlem2  15730  perfect  15731  lgsval  15739  lgsfvalg  15740  lgsfcl2  15741  lgsval2lem  15745  lgsdir2lem2  15764  lgsdir2  15768  gausslemma2dlem1a  15793  gausslemma2dlem1cl  15794  gausslemma2dlem1f1o  15795  gausslemma2dlem4  15799  gausslemma2d  15804  lgseisenlem1  15805  lgseisenlem2  15806  lgseisenlem3  15807  lgseisenlem4  15808  lgsquadlemofi  15811  lgsquadlem1  15812  lgsquadlem2  15813  lgsquad2lem2  15817  m1lgs  15820  2lgslem1c  15825  2lgslem3a1  15832  2lgslem3d1  15835  2lgslem4  15838  2lgs  15839  2sqlem3  15852  2sqlem8  15858  clwwlkn2  16278  eupth2lem3lem4fi  16330  ex-fl  16343  ex-ceil  16344  redcwlpolemeq1  16685  nconstwlpolem0  16694