Theorem 2nn 9399

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 9296	. 2 ⊢ 2 = (1 + 1)
2		1nn 9248	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 9249	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2305	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2203  (class class class)co 6050  1c1 8128   + caddc 8130  ℕcn 9237  2c2 9288

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-sep 4228  ax-cnex 8218  ax-resscn 8219  ax-1re 8221  ax-addrcl 8224

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-int 3950  df-br 4110  df-iota 5312  df-fv 5360  df-ov 6053  df-inn 9238  df-2 9296

This theorem is referenced by:  3nn  9400  2nn0  9513  2z  9605  uz3m2nn  9905  ige2m1fz1  10443  qbtwnre  10616  flhalf  10662  sqeq0  10964  sqeq0d  11034  facavg  11108  bcn2  11126  resqrexlemnm  11703  abs00ap  11747  geo2sum  12200  geo2lim  12202  ege2le3  12357  ef01bndlem  12442  mod2eq0even  12564  mod2eq1n2dvds  12565  bitsdc  12633  bits0o  12636  bitsp1  12637  bitsp1o  12639  bitsfzolem  12640  bitsfzo  12641  bitsmod  12642  bitsfi  12643  bitscmp  12644  bitsinv1lem  12647  bitsinv1  12648  sqgcd  12725  3lcm2e6woprm  12783  prm2orodd  12823  3prm  12825  4nprm  12826  isprm5lem  12838  divgcdodd  12840  isevengcd2  12855  3lcm2e6  12857  pw2dvdslemn  12862  pw2dvds  12863  pw2dvdseulemle  12864  oddpwdclemxy  12866  oddpwdclemodd  12869  oddpwdclemdc  12870  oddpwdc  12871  sqpweven  12872  2sqpwodd  12873  pythagtriplem4  12966  oddprmdvds  13052  4sqlem5  13080  4sqlem6  13081  4sqlem10  13085  4sqlem12  13100  dec2dvds  13109  dec5nprm  13112  dec2nprm  13113  2expltfac  13137  evenennn  13144  exmidunben  13177  plusgndx  13322  plusgid  13323  plusgndxnn  13324  plusgslid  13325  grpstrg  13339  grpbaseg  13340  grpplusgg  13341  rngstrg  13348  lmodstrd  13377  topgrpstrd  13409  dsndx  13428  dsid  13429  dsslid  13430  dsndxnn  13431  slotsdifdsndx  13438  slotsdifunifndx  13445  imasvalstrd  13483  cnfldstr  14706  dveflem  15591  1sgm2ppw  15863  mersenne  15865  perfect1  15866  perfectlem1  15867  perfectlem2  15868  perfect  15869  lgsval  15877  lgsfvalg  15878  lgsfcl2  15879  lgsval2lem  15883  lgsdir2lem2  15902  lgsdir2  15906  gausslemma2dlem1a  15931  gausslemma2dlem1cl  15932  gausslemma2dlem1f1o  15933  gausslemma2dlem4  15937  gausslemma2d  15942  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisenlem4  15946  lgsquadlemofi  15949  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad2lem2  15955  m1lgs  15958  2lgslem1c  15963  2lgslem3a1  15970  2lgslem3d1  15973  2lgslem4  15976  2lgs  15977  2sqlem3  15990  2sqlem8  15996  clwwlkn2  16416  eupth2lem3lem4fi  16468  konigsberglem5  16487  ex-fl  16493  ex-ceil  16494  redcwlpolemeq1  16839  nconstwlpolem0  16849