Theorem 2nn 9477

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 9372	. 2 ⊢ 2 = (1 + 1)
2		1nn 9324	. . 3 ⊢ 1 ∈ ℕ
3		peano2nn 9325	. . 3 ⊢ (1 ∈ ℕ → (1 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (1 + 1) ∈ ℕ
5	1, 4	eqeltri 2311	1 ⊢ 2 ∈ ℕ

This proof depends on syntax axioms:   ∈ wcel 2209  (class class class)co 6088  1c1 8186   + caddc 8188  ℕcn 9313  2c2 9364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4251  ax-cnex 8276  ax-resscn 8277  ax-1re 8279  ax-addrcl 8282

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-br 4132  df-iota 5340  df-fv 5388  df-ov 6091  df-inn 9314  df-2 9372

This theorem is used by:  3nn  9478  2nn0  9591  2z  9681  uz3m2nn  9988  ige2m1fz1  10532  qbtwnre  10707  flhalf  10757  sqeq0  11059  sqeq0d  11130  facavg  11205  bcn2  11223  resqrexlemnm  11805  abs00ap  11849  geo2sum  12305  geo2lim  12307  ege2le3  12462  ef01bndlem  12547  mod2eq0even  12669  mod2eq1n2dvds  12670  bitsdc  12738  bits0o  12741  bitsp1  12742  bitsp1o  12744  bitsfzolem  12745  bitsfzo  12746  bitsmod  12747  bitsfi  12748  bitscmp  12749  bitsinv1lem  12752  bitsinv1  12753  sqgcd  12830  3lcm2e6woprm  12888  prm2orodd  12928  3prm  12930  4nprm  12931  isprm5lem  12944  divgcdodd  12946  isevengcd2  12961  3lcm2e6  12963  sqpweven  12979  2sqpwodd  12980  pythagtriplem4  13075  oddprmdvds  13161  4sqlem5  13189  4sqlem6  13190  4sqlem10  13194  4sqlem12  13209  dec2dvds  13218  dec5nprm  13221  dec2nprm  13222  2expltfac  13247  5prm  13251  6nprm  13252  7prm  13253  8nprm  13254  11prm  13257  17prm  13259  23prm  13261  37prm  13263  43prm  13264  83prm  13265  139prm  13266  163prm  13267  317prm  13268  631prm  13269  1259lem1  13270  1259lem2  13271  1259lem3  13272  1259lem4  13273  1259lem5  13274  1259prm  13275  evenennn  13341  exmidunben  13374  plusgndx  13521  plusgid  13522  plusgndxnn  13523  plusgslid  13524  grpstrg  13538  grpbaseg  13539  grpplusgg  13540  rngstrg  13547  lmodstrd  13576  topgrpstrd  13608  dsndx  13627  dsid  13628  dsslid  13629  dsndxnn  13630  slotsdifdsndx  13637  slotsdifunifndx  13644  imasvalstrd  13677  cnfldstr  15003  dveflem  15969  1sgm2ppw  16306  ppiublem1  16308  chtublem  16312  mersenne  16314  perfect1  16315  perfectlem1  16316  perfectlem2  16317  perfect  16318  pcbcctr  16320  bclbnd  16324  bposlem1  16328  bposlem2  16329  bposlem3  16330  bposlem4  16331  bposlem5  16332  bposlem6  16333  bposlem8  16335  lgsval  16345  lgsfvalg  16346  lgsfcl2  16347  lgsval2lem  16351  lgsdir2lem2  16370  lgsdir2  16374  gausslemma2dlem1a  16399  gausslemma2dlem1cl  16400  gausslemma2dlem1f1o  16401  gausslemma2dlem4  16405  gausslemma2d  16410  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem3  16413  lgseisenlem4  16414  lgsquadlemofi  16417  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2lem2  16423  m1lgs  16426  2lgslem1c  16431  2lgslem3a1  16438  2lgslem3d1  16441  2lgslem4  16444  2lgs  16445  2sqlem3  16458  2sqlem8  16464  clwwlkn2  16884  eupth2lem3lem4fi  16936  konigsberglem5  16955  ex-fl  16961  ex-ceil  16962  redcwlpolemeq1  17328  nconstwlpolem0  17337