Theorem 2nn 9039

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 8937	. 2 ⊢ 2 = (1 + 1)
2		1nn 8889	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 8890	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2243	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2141  (class class class)co 5853  1c1 7775   + caddc 7777  ℕcn 8878  2c2 8929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-sep 4107  ax-cnex 7865  ax-resscn 7866  ax-1re 7868  ax-addrcl 7871

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-br 3990  df-iota 5160  df-fv 5206  df-ov 5856  df-inn 8879  df-2 8937

This theorem is referenced by:  3nn  9040  2nn0  9152  2z  9240  uz3m2nn  9532  ige2m1fz1  10065  qbtwnre  10213  flhalf  10258  sqeq0  10539  sqeq0d  10608  facavg  10680  bcn2  10698  resqrexlemnm  10982  abs00ap  11026  geo2sum  11477  geo2lim  11479  ege2le3  11634  ef01bndlem  11719  mod2eq0even  11837  mod2eq1n2dvds  11838  sqgcd  11984  3lcm2e6woprm  12040  prm2orodd  12080  3prm  12082  4nprm  12083  isprm5lem  12095  divgcdodd  12097  isevengcd2  12112  3lcm2e6  12114  pw2dvdslemn  12119  pw2dvds  12120  pw2dvdseulemle  12121  oddpwdclemxy  12123  oddpwdclemodd  12126  oddpwdclemdc  12127  oddpwdc  12128  sqpweven  12129  2sqpwodd  12130  pythagtriplem4  12222  oddprmdvds  12306  4sqlem5  12334  4sqlem6  12335  4sqlem10  12339  evenennn  12348  exmidunben  12381  plusgndx  12511  plusgid  12512  plusgslid  12513  grpstrg  12525  grpbaseg  12526  grpplusgg  12527  rngstrg  12533  lmodstrd  12551  topgrpstrd  12569  dsndx  12576  dsid  12577  dsslid  12578  dveflem  13481  lgsval  13699  lgsfvalg  13700  lgsfcl2  13701  lgsval2lem  13705  lgsdir2lem2  13724  lgsdir2  13728  2sqlem3  13747  2sqlem8  13753  ex-fl  13760  ex-ceil  13761  redcwlpolemeq1  14086  nconstwlpolem0  14094