Theorem 6nn 11967

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 11945	. 2 ⊢ 6 = (5 + 1)
2		5nn 11964	. . 3 ⊢ 5 ∈ ℕ
3		peano2nn 11890	. . 3 ⊢ (5 ∈ ℕ → (5 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (5 + 1) ∈ ℕ
5	1, 4	eqeltri 2836	1 ⊢ 6 ∈ ℕ

Syntax hints:   ∈ wcel 2112  (class class class)co 7252  1c1 10778   + caddc 10780  ℕcn 11878  5c5 11936  6c6 11937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5216  ax-nul 5223  ax-pr 5346  ax-un 7563  ax-1cn 10835

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3425  df-sbc 3713  df-csb 3830  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5153  df-tr 5186  df-id 5479  df-eprel 5485  df-po 5493  df-so 5494  df-fr 5534  df-we 5536  df-xp 5585  df-rel 5586  df-cnv 5587  df-co 5588  df-dm 5589  df-rn 5590  df-res 5591  df-ima 5592  df-pred 6189  df-ord 6251  df-on 6252  df-lim 6253  df-suc 6254  df-iota 6373  df-fun 6417  df-fn 6418  df-f 6419  df-f1 6420  df-fo 6421  df-f1o 6422  df-fv 6423  df-ov 7255  df-om 7685  df-wrecs 8089  df-recs 8150  df-rdg 8188  df-nn 11879  df-2 11941  df-3 11942  df-4 11943  df-5 11944  df-6 11945

This theorem is referenced by:  7nn  11970  6nn0  12159  ef01bndlem  15796  sin01bnd  15797  cos01bnd  15798  6gcd4e2  16149  6lcm4e12  16224  83prm  16727  139prm  16728  163prm  16729  prmo6  16734  vscandx  16930  vscaid  16931  lmodstr  16936  ipsstr  16946  lt6abl  19386  psrvalstr  21004  opsrvscaOLD  21144  tngvscaOLD  23689  sincos3rdpi  25553  1cubrlem  25871  quart1cl  25884  quart1lem  25885  quart1  25886  log2ub  25979  log2le1  25980  basellem5  26114  basellem8  26117  basellem9  26118  ppiublem1  26230  ppiublem2  26231  ppiub  26232  bpos1  26311  bposlem9  26320  itvndx  26678  itvid  26680  slotsinbpsd  26682  trkgstr  26684  ttgval  27115  ttglemOLD  27117  ttgvscaOLD  27124  ttgdsOLD  27126  eengstr  27226  ex-cnv  28677  ex-dm  28679  ex-dvds  28696  ex-gcd  28697  ex-lcm  28698  resvvscaOLD  31414  hgt750lem  32506  60gcd6e6  39919  60gcd7e1  39920  12lcm5e60  39923  60lcm6e60  39924  60lcm7e420  39925  lcm6un  39933  lcmineqlem  39967  3lexlogpow5ineq1  39969  aks4d1p1p5  39989  aks4d1p1  39990  rmydioph  40724  expdiophlem2  40732  algstr  40890  mnringvscadOLD  41705  139prmALT  44909  31prm  44910  127prm  44912  6even  45024  gbowge7  45076  stgoldbwt  45089  sbgoldbwt  45090  mogoldbb  45098  sbgoldbo  45100  nnsum3primesle9  45107  nnsum4primeseven  45113  wtgoldbnnsum4prm  45115  bgoldbnnsum3prm  45117  zlmodzxzequa  45698  zlmodzxznm  45699  zlmodzxzequap  45701  zlmodzxzldeplem3  45704  zlmodzxzldep  45706  ldepsnlinclem2  45708  ldepsnlinc  45710