Theorem 2nn 9268

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 9165	. 2 ⊢ 2 = (1 + 1)
2		1nn 9117	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 9118	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2302	1 ⊢ 2 ∈ ℕ

Syntax hints:   ∈ wcel 2200  (class class class)co 6000  1c1 7996   + caddc 7998  ℕcn 9106  2c2 9157

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4201  ax-cnex 8086  ax-resscn 8087  ax-1re 8089  ax-addrcl 8092

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-int 3923  df-br 4083  df-iota 5277  df-fv 5325  df-ov 6003  df-inn 9107  df-2 9165

This theorem is referenced by:  3nn  9269  2nn0  9382  2z  9470  uz3m2nn  9764  ige2m1fz1  10301  qbtwnre  10471  flhalf  10517  sqeq0  10819  sqeq0d  10889  facavg  10963  bcn2  10981  resqrexlemnm  11524  abs00ap  11568  geo2sum  12020  geo2lim  12022  ege2le3  12177  ef01bndlem  12262  mod2eq0even  12384  mod2eq1n2dvds  12385  bitsdc  12453  bits0o  12456  bitsp1  12457  bitsp1o  12459  bitsfzolem  12460  bitsfzo  12461  bitsmod  12462  bitsfi  12463  bitscmp  12464  bitsinv1lem  12467  bitsinv1  12468  sqgcd  12545  3lcm2e6woprm  12603  prm2orodd  12643  3prm  12645  4nprm  12646  isprm5lem  12658  divgcdodd  12660  isevengcd2  12675  3lcm2e6  12677  pw2dvdslemn  12682  pw2dvds  12683  pw2dvdseulemle  12684  oddpwdclemxy  12686  oddpwdclemodd  12689  oddpwdclemdc  12690  oddpwdc  12691  sqpweven  12692  2sqpwodd  12693  pythagtriplem4  12786  oddprmdvds  12872  4sqlem5  12900  4sqlem6  12901  4sqlem10  12905  4sqlem12  12920  dec2dvds  12929  dec5nprm  12932  dec2nprm  12933  2expltfac  12957  evenennn  12959  exmidunben  12992  plusgndx  13137  plusgid  13138  plusgndxnn  13139  plusgslid  13140  grpstrg  13154  grpbaseg  13155  grpplusgg  13156  rngstrg  13163  lmodstrd  13192  topgrpstrd  13224  dsndx  13243  dsid  13244  dsslid  13245  dsndxnn  13246  slotsdifdsndx  13253  slotsdifunifndx  13260  imasvalstrd  13298  cnfldstr  14516  dveflem  15394  1sgm2ppw  15663  mersenne  15665  perfect1  15666  perfectlem1  15667  perfectlem2  15668  perfect  15669  lgsval  15677  lgsfvalg  15678  lgsfcl2  15679  lgsval2lem  15683  lgsdir2lem2  15702  lgsdir2  15706  gausslemma2dlem1a  15731  gausslemma2dlem1cl  15732  gausslemma2dlem1f1o  15733  gausslemma2dlem4  15737  gausslemma2d  15742  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem3  15745  lgseisenlem4  15746  lgsquadlemofi  15749  lgsquadlem1  15750  lgsquadlem2  15751  lgsquad2lem2  15755  m1lgs  15758  2lgslem1c  15763  2lgslem3a1  15770  2lgslem3d1  15773  2lgslem4  15776  2lgs  15777  2sqlem3  15790  2sqlem8  15796  ex-fl  16047  ex-ceil  16048  redcwlpolemeq1  16381  nconstwlpolem0  16390