Theorem 2nn 9171

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 9068	. 2 ⊢ 2 = (1 + 1)
2		1nn 9020	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 9021	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2269	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2167  (class class class)co 5925  1c1 7899   + caddc 7901  ℕcn 9009  2c2 9060

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152  ax-cnex 7989  ax-resscn 7990  ax-1re 7992  ax-addrcl 7995

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-int 3876  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928  df-inn 9010  df-2 9068

This theorem is referenced by:  3nn  9172  2nn0  9285  2z  9373  uz3m2nn  9666  ige2m1fz1  10203  qbtwnre  10365  flhalf  10411  sqeq0  10713  sqeq0d  10783  facavg  10857  bcn2  10875  resqrexlemnm  11202  abs00ap  11246  geo2sum  11698  geo2lim  11700  ege2le3  11855  ef01bndlem  11940  mod2eq0even  12062  mod2eq1n2dvds  12063  bitsdc  12131  bits0o  12134  bitsp1  12135  bitsp1o  12137  bitsfzolem  12138  bitsfzo  12139  bitsmod  12140  bitsfi  12141  bitscmp  12142  bitsinv1lem  12145  bitsinv1  12146  sqgcd  12223  3lcm2e6woprm  12281  prm2orodd  12321  3prm  12323  4nprm  12324  isprm5lem  12336  divgcdodd  12338  isevengcd2  12353  3lcm2e6  12355  pw2dvdslemn  12360  pw2dvds  12361  pw2dvdseulemle  12362  oddpwdclemxy  12364  oddpwdclemodd  12367  oddpwdclemdc  12368  oddpwdc  12369  sqpweven  12370  2sqpwodd  12371  pythagtriplem4  12464  oddprmdvds  12550  4sqlem5  12578  4sqlem6  12579  4sqlem10  12583  4sqlem12  12598  dec2dvds  12607  dec5nprm  12610  dec2nprm  12611  2expltfac  12635  evenennn  12637  exmidunben  12670  plusgndx  12814  plusgid  12815  plusgndxnn  12816  plusgslid  12817  grpstrg  12830  grpbaseg  12831  grpplusgg  12832  rngstrg  12839  lmodstrd  12868  topgrpstrd  12900  dsndx  12919  dsid  12920  dsslid  12921  dsndxnn  12922  slotsdifdsndx  12929  slotsdifunifndx  12936  imasvalstrd  12974  cnfldstr  14192  dveflem  15070  1sgm2ppw  15339  mersenne  15341  perfect1  15342  perfectlem1  15343  perfectlem2  15344  perfect  15345  lgsval  15353  lgsfvalg  15354  lgsfcl2  15355  lgsval2lem  15359  lgsdir2lem2  15378  lgsdir2  15382  gausslemma2dlem1a  15407  gausslemma2dlem1cl  15408  gausslemma2dlem1f1o  15409  gausslemma2dlem4  15413  gausslemma2d  15418  lgseisenlem1  15419  lgseisenlem2  15420  lgseisenlem3  15421  lgseisenlem4  15422  lgsquadlemofi  15425  lgsquadlem1  15426  lgsquadlem2  15427  lgsquad2lem2  15431  m1lgs  15434  2lgslem1c  15439  2lgslem3a1  15446  2lgslem3d1  15449  2lgslem4  15452  2lgs  15453  2sqlem3  15466  2sqlem8  15472  ex-fl  15479  ex-ceil  15480  redcwlpolemeq1  15811  nconstwlpolem0  15820