Theorem 6nn 12297

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 12275	. 2 ⊢ 6 = (5 + 1)
2		5nn 12294	. . 3 ⊢ 5 ∈ ℕ
3		peano2nn 12220	. . 3 ⊢ (5 ∈ ℕ → (5 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (5 + 1) ∈ ℕ
5	1, 4	eqeltri 2821	1 ⊢ 6 ∈ ℕ

Syntax hints:   ∈ wcel 2098  (class class class)co 7401  1c1 11106   + caddc 11108  ℕcn 12208  5c5 12266  6c6 12267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417  ax-un 7718  ax-1cn 11163

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7404  df-om 7849  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275

This theorem is referenced by:  7nn  12300  6nn0  12489  ef01bndlem  16123  sin01bnd  16124  cos01bnd  16125  6gcd4e2  16476  6lcm4e12  16549  83prm  17052  139prm  17053  163prm  17054  prmo6  17059  vscandx  17260  vscaid  17261  lmodstr  17266  ipsstr  17277  lt6abl  19800  psrvalstr  21769  opsrvscaOLD  21914  tngvscaOLD  24471  sincos3rdpi  26356  1cubrlem  26677  quart1cl  26690  quart1lem  26691  quart1  26692  log2ub  26785  log2le1  26786  basellem5  26921  basellem8  26924  basellem9  26925  ppiublem1  27039  ppiublem2  27040  ppiub  27041  bpos1  27120  bposlem9  27129  itvndx  28112  itvid  28114  slotsinbpsd  28116  lngndxnitvndx  28118  trkgstr  28119  ttgvalOLD  28551  ttglemOLD  28553  ttgvscaOLD  28560  ttgdsOLD  28562  eengstr  28662  ex-cnv  30114  ex-dm  30116  ex-dvds  30133  ex-gcd  30134  ex-lcm  30135  resvvscaOLD  32879  hgt750lem  34118  60gcd6e6  41328  60gcd7e1  41329  12lcm5e60  41332  60lcm6e60  41333  60lcm7e420  41334  lcm6un  41342  lcmineqlem  41376  3lexlogpow5ineq1  41378  aks4d1p1p5  41399  aks4d1p1  41400  rmydioph  42208  expdiophlem2  42216  algstr  42374  mnringvscadOLD  43439  139prmALT  46715  31prm  46716  127prm  46718  6even  46830  gbowge7  46882  stgoldbwt  46895  sbgoldbwt  46896  mogoldbb  46904  sbgoldbo  46906  nnsum3primesle9  46913  nnsum4primeseven  46919  wtgoldbnnsum4prm  46921  bgoldbnnsum3prm  46923  zlmodzxzequa  47331  zlmodzxznm  47332  zlmodzxzequap  47334  zlmodzxzldeplem3  47337  zlmodzxzldep  47339  ldepsnlinclem2  47341  ldepsnlinc  47343