Theorem 2nn 9420

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 9317	. 2 ⊢ 2 = (1 + 1)
2		1nn 9269	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 9270	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2307	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2205  (class class class)co 6059  1c1 8145   + caddc 8147  ℕcn 9258  2c2 9309

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 2216  ax-sep 4234  ax-cnex 8235  ax-resscn 8236  ax-1re 8238  ax-addrcl 8241

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-sn 3701  df-pr 3702  df-op 3704  df-uni 3921  df-int 3956  df-br 4116  df-iota 5318  df-fv 5366  df-ov 6062  df-inn 9259  df-2 9317

This theorem is referenced by:  3nn  9421  2nn0  9534  2z  9626  uz3m2nn  9927  ige2m1fz1  10469  qbtwnre  10644  flhalf  10690  sqeq0  10992  sqeq0d  11063  facavg  11137  bcn2  11155  resqrexlemnm  11733  abs00ap  11777  geo2sum  12230  geo2lim  12232  ege2le3  12387  ef01bndlem  12472  mod2eq0even  12594  mod2eq1n2dvds  12595  bitsdc  12663  bits0o  12666  bitsp1  12667  bitsp1o  12669  bitsfzolem  12670  bitsfzo  12671  bitsmod  12672  bitsfi  12673  bitscmp  12674  bitsinv1lem  12677  bitsinv1  12678  sqgcd  12755  3lcm2e6woprm  12813  prm2orodd  12853  3prm  12855  4nprm  12856  isprm5lem  12868  divgcdodd  12870  isevengcd2  12885  3lcm2e6  12887  pw2dvdslemn  12892  pw2dvds  12893  pw2dvdseulemle  12894  oddpwdclemxy  12896  oddpwdclemodd  12899  oddpwdclemdc  12900  oddpwdc  12901  sqpweven  12902  2sqpwodd  12903  pythagtriplem4  12996  oddprmdvds  13082  4sqlem5  13110  4sqlem6  13111  4sqlem10  13115  4sqlem12  13130  dec2dvds  13139  dec5nprm  13142  dec2nprm  13143  2expltfac  13167  evenennn  13233  exmidunben  13266  plusgndx  13411  plusgid  13412  plusgndxnn  13413  plusgslid  13414  grpstrg  13428  grpbaseg  13429  grpplusgg  13430  rngstrg  13437  lmodstrd  13466  topgrpstrd  13498  dsndx  13517  dsid  13518  dsslid  13519  dsndxnn  13520  slotsdifdsndx  13527  slotsdifunifndx  13534  imasvalstrd  13567  cnfldstr  14837  dveflem  15722  1sgm2ppw  15994  mersenne  15996  perfect1  15997  perfectlem1  15998  perfectlem2  15999  perfect  16000  lgsval  16008  lgsfvalg  16009  lgsfcl2  16010  lgsval2lem  16014  lgsdir2lem2  16033  lgsdir2  16037  gausslemma2dlem1a  16062  gausslemma2dlem1cl  16063  gausslemma2dlem1f1o  16064  gausslemma2dlem4  16068  gausslemma2d  16073  lgseisenlem1  16074  lgseisenlem2  16075  lgseisenlem3  16076  lgseisenlem4  16077  lgsquadlemofi  16080  lgsquadlem1  16081  lgsquadlem2  16082  lgsquad2lem2  16086  m1lgs  16089  2lgslem1c  16094  2lgslem3a1  16101  2lgslem3d1  16104  2lgslem4  16107  2lgs  16108  2sqlem3  16121  2sqlem8  16127  clwwlkn2  16547  eupth2lem3lem4fi  16599  konigsberglem5  16618  ex-fl  16624  ex-ceil  16625  redcwlpolemeq1  16980  nconstwlpolem0  16989