Theorem 2nn 9347

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 9244	. 2 ⊢ 2 = (1 + 1)
2		1nn 9196	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 9197	. . 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 6028  1c1 8076   + caddc 8078  ℕcn 9185  2c2 9236

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 2213  ax-sep 4212  ax-cnex 8166  ax-resscn 8167  ax-1re 8169  ax-addrcl 8172

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-int 3934  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031  df-inn 9186  df-2 9244

This theorem is referenced by:  3nn  9348  2nn0  9461  2z  9551  uz3m2nn  9851  ige2m1fz1  10389  qbtwnre  10562  flhalf  10608  sqeq0  10910  sqeq0d  10980  facavg  11054  bcn2  11072  resqrexlemnm  11641  abs00ap  11685  geo2sum  12138  geo2lim  12140  ege2le3  12295  ef01bndlem  12380  mod2eq0even  12502  mod2eq1n2dvds  12503  bitsdc  12571  bits0o  12574  bitsp1  12575  bitsp1o  12577  bitsfzolem  12578  bitsfzo  12579  bitsmod  12580  bitsfi  12581  bitscmp  12582  bitsinv1lem  12585  bitsinv1  12586  sqgcd  12663  3lcm2e6woprm  12721  prm2orodd  12761  3prm  12763  4nprm  12764  isprm5lem  12776  divgcdodd  12778  isevengcd2  12793  3lcm2e6  12795  pw2dvdslemn  12800  pw2dvds  12801  pw2dvdseulemle  12802  oddpwdclemxy  12804  oddpwdclemodd  12807  oddpwdclemdc  12808  oddpwdc  12809  sqpweven  12810  2sqpwodd  12811  pythagtriplem4  12904  oddprmdvds  12990  4sqlem5  13018  4sqlem6  13019  4sqlem10  13023  4sqlem12  13038  dec2dvds  13047  dec5nprm  13050  dec2nprm  13051  2expltfac  13075  evenennn  13077  exmidunben  13110  plusgndx  13255  plusgid  13256  plusgndxnn  13257  plusgslid  13258  grpstrg  13272  grpbaseg  13273  grpplusgg  13274  rngstrg  13281  lmodstrd  13310  topgrpstrd  13342  dsndx  13361  dsid  13362  dsslid  13363  dsndxnn  13364  slotsdifdsndx  13371  slotsdifunifndx  13378  imasvalstrd  13416  cnfldstr  14637  dveflem  15520  1sgm2ppw  15792  mersenne  15794  perfect1  15795  perfectlem1  15796  perfectlem2  15797  perfect  15798  lgsval  15806  lgsfvalg  15807  lgsfcl2  15808  lgsval2lem  15812  lgsdir2lem2  15831  lgsdir2  15835  gausslemma2dlem1a  15860  gausslemma2dlem1cl  15861  gausslemma2dlem1f1o  15862  gausslemma2dlem4  15866  gausslemma2d  15871  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem3  15874  lgseisenlem4  15875  lgsquadlemofi  15878  lgsquadlem1  15879  lgsquadlem2  15880  lgsquad2lem2  15884  m1lgs  15887  2lgslem1c  15892  2lgslem3a1  15899  2lgslem3d1  15902  2lgslem4  15905  2lgs  15906  2sqlem3  15919  2sqlem8  15925  clwwlkn2  16345  eupth2lem3lem4fi  16397  konigsberglem5  16416  ex-fl  16422  ex-ceil  16423  redcwlpolemeq1  16770  nconstwlpolem0  16779