Theorem 6nn 12326

Description: 6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)

Assertion

Ref	Expression
6nn	⊢ 6 ∈ ℕ

Proof of Theorem 6nn

Step	Hyp	Ref	Expression
1		df-6 12303	. 2 ⊢ 6 = (5 + 1)
2		5nn 12323	. . 3 ⊢ 5 ∈ ℕ
3		peano2nn 12241	. . 3 ⊢ (5 ∈ ℕ → (5 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (5 + 1) ∈ ℕ
5	1, 4	eqeltri 2865	1 ⊢ 6 ∈ ℕ

Syntax hints:   ∈ wcel 2149  (class class class)co 7408  1c1 11097   + caddc 11099  ℕcn 12229  5c5 12294  6c6 12295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402  ax-un 7730  ax-1cn 11154

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7411  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-nn 12230  df-2 12299  df-3 12300  df-4 12301  df-5 12302  df-6 12303

This theorem is referenced by:  7nn  12329  6pos  12350  6nn0  12521  ef01bndlem  16236  sin01bnd  16237  cos01bnd  16238  6gcd4e2  16592  6lcm4e12  16670  83prm  17179  139prm  17180  163prm  17181  prmo6  17186  vscandx  17368  vscaid  17369  lmodstr  17374  ipsstr  17385  lt6abl  19961  psrvalstr  22031  sincos3rdpi  26644  1cubrlem  26968  quart1cl  26981  quart1lem  26982  quart1  26983  log2ub  27076  log2le1  27077  basellem5  27211  basellem8  27214  basellem9  27215  ppiublem1  27328  ppiublem2  27329  ppiub  27330  bpos1  27409  bposlem9  27418  itvndx  28668  itvid  28670  slotsinbpsd  28672  lngndxnitvndx  28674  trkgstr  28675  eengstr  29267  ex-cnv  30725  ex-dm  30727  ex-dvds  30744  ex-gcd  30745  ex-lcm  30746  hgt750lem  34979  60gcd6e6  42656  60gcd7e1  42657  12lcm5e60  42660  60lcm6e60  42661  60lcm7e420  42662  lcm6un  42670  lcmineqlem  42704  3lexlogpow5ineq1  42706  aks4d1p1p5  42727  aks4d1p1  42728  6ne0  42911  rmydioph  43626  expdiophlem2  43634  algstr  43785  goldratmolem2  47505  139prmALT  48230  31prm  48231  127prm  48233  nprmdvdsfacm1lem4  48257  nprmdvdsfacm1  48258  ppivalnnnprmge6  48260  6even  48358  gbowge7  48410  stgoldbwt  48423  sbgoldbwt  48424  mogoldbb  48432  sbgoldbo  48434  nnsum3primesle9  48441  nnsum4primeseven  48447  wtgoldbnnsum4prm  48449  bgoldbnnsum3prm  48451  zlmodzxzequa  49154  zlmodzxznm  49155  zlmodzxzequap  49157  zlmodzxzldeplem3  49160  zlmodzxzldep  49162  ldepsnlinclem2  49164  ldepsnlinc  49166