Theorem 2nn 9152

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 9049	. 2 ⊢ 2 = (1 + 1)
2		1nn 9001	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 9002	. . 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 5922  1c1 7880   + caddc 7882  ℕcn 8990  2c2 9041

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 4151  ax-cnex 7970  ax-resscn 7971  ax-1re 7973  ax-addrcl 7976

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 3628  df-pr 3629  df-op 3631  df-uni 3840  df-int 3875  df-br 4034  df-iota 5219  df-fv 5266  df-ov 5925  df-inn 8991  df-2 9049

This theorem is referenced by:  3nn  9153  2nn0  9266  2z  9354  uz3m2nn  9647  ige2m1fz1  10184  qbtwnre  10346  flhalf  10392  sqeq0  10694  sqeq0d  10764  facavg  10838  bcn2  10856  resqrexlemnm  11183  abs00ap  11227  geo2sum  11679  geo2lim  11681  ege2le3  11836  ef01bndlem  11921  mod2eq0even  12043  mod2eq1n2dvds  12044  bits0o  12114  bitsp1  12115  bitsp1o  12117  bitsfzolem  12118  bitsfzo  12119  sqgcd  12196  3lcm2e6woprm  12254  prm2orodd  12294  3prm  12296  4nprm  12297  isprm5lem  12309  divgcdodd  12311  isevengcd2  12326  3lcm2e6  12328  pw2dvdslemn  12333  pw2dvds  12334  pw2dvdseulemle  12335  oddpwdclemxy  12337  oddpwdclemodd  12340  oddpwdclemdc  12341  oddpwdc  12342  sqpweven  12343  2sqpwodd  12344  pythagtriplem4  12437  oddprmdvds  12523  4sqlem5  12551  4sqlem6  12552  4sqlem10  12556  4sqlem12  12571  dec2dvds  12580  dec5nprm  12583  dec2nprm  12584  2expltfac  12608  evenennn  12610  exmidunben  12643  plusgndx  12787  plusgid  12788  plusgndxnn  12789  plusgslid  12790  grpstrg  12803  grpbaseg  12804  grpplusgg  12805  rngstrg  12812  lmodstrd  12841  topgrpstrd  12873  dsndx  12888  dsid  12889  dsslid  12890  dsndxnn  12891  slotsdifdsndx  12898  slotsdifunifndx  12905  cnfldstr  14114  dveflem  14962  1sgm2ppw  15231  mersenne  15233  perfect1  15234  perfectlem1  15235  perfectlem2  15236  perfect  15237  lgsval  15245  lgsfvalg  15246  lgsfcl2  15247  lgsval2lem  15251  lgsdir2lem2  15270  lgsdir2  15274  gausslemma2dlem1a  15299  gausslemma2dlem1cl  15300  gausslemma2dlem1f1o  15301  gausslemma2dlem4  15305  gausslemma2d  15310  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgseisenlem4  15314  lgsquadlemofi  15317  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2lem2  15323  m1lgs  15326  2lgslem1c  15331  2lgslem3a1  15338  2lgslem3d1  15341  2lgslem4  15344  2lgs  15345  2sqlem3  15358  2sqlem8  15364  ex-fl  15371  ex-ceil  15372  redcwlpolemeq1  15698  nconstwlpolem0  15707