Theorem 8nn 12313

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

Assertion

Ref	Expression
8nn	⊢ 8 ∈ ℕ

Proof of Theorem 8nn

Step	Hyp	Ref	Expression
1		df-8 12287	. 2 ⊢ 8 = (7 + 1)
2		7nn 12310	. . 3 ⊢ 7 ∈ ℕ
3		peano2nn 12230	. . 3 ⊢ (7 ∈ ℕ → (7 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (7 + 1) ∈ ℕ
5	1, 4	eqeltri 2827	1 ⊢ 8 ∈ ℕ

Syntax hints:   ∈ wcel 2104  (class class class)co 7413  1c1 11115   + caddc 11117  ℕcn 12218  7c7 12278  8c8 12279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7729  ax-1cn 11172

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7416  df-om 7860  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-nn 12219  df-2 12281  df-3 12282  df-4 12283  df-5 12284  df-6 12285  df-7 12286  df-8 12287

This theorem is referenced by:  9nn  12316  8nn0  12501  37prm  17060  43prm  17061  83prm  17062  317prm  17065  1259lem4  17073  1259lem5  17074  2503prm  17079  4001prm  17084  ipndx  17281  ipid  17282  ipsstr  17287  phlstr  17297  tngipOLD  24385  quart1cl  26593  quart1lem  26594  quart1  26595  log2tlbnd  26684  bposlem8  27028  lgsdir2lem2  27063  lgsdir2lem3  27064  2lgslem3a1  27137  2lgslem3b1  27138  2lgslem3c1  27139  2lgslem3d1  27140  2lgslem4  27143  2lgsoddprmlem2  27146  pntlemr  27339  pntlemj  27340  edgfid  28513  edgfndx  28514  edgfndxnn  28515  edgfndxidOLD  28517  baseltedgfOLD  28519  ex-prmo  29977  hgt750lem  33959  hgt750lem2  33960  420gcd8e4  41179  420lcm8e840  41184  lcm8un  41193  lcmineqlem23  41224  lcmineqlem  41225  3lexlogpow5ineq2  41228  3lexlogpow2ineq1  41231  rmydioph  42057  fmtnoprmfac2lem1  46534  127prm  46567  mod42tp1mod8  46570  8even  46681  8exp8mod9  46704  9fppr8  46705  nfermltl8rev  46710  nfermltlrev  46712  nnsum4primesevenALTV  46769  wtgoldbnnsum4prm  46770  bgoldbnnsum3prm  46772  bgoldbtbndlem1  46773  tgblthelfgott  46783  tgoldbachlt  46784