Theorem 8nn 12241

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 12215	. 2 ⊢ 8 = (7 + 1)
2		7nn 12238	. . 3 ⊢ 7 ∈ ℕ
3		peano2nn 12158	. . 3 ⊢ (7 ∈ ℕ → (7 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (7 + 1) ∈ ℕ
5	1, 4	eqeltri 2833	1 ⊢ 8 ∈ ℕ

Syntax hints:   ∈ wcel 2114  (class class class)co 7358  1c1 11028   + caddc 11030  ℕcn 12146  7c7 12206  8c8 12207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5368  ax-un 7680  ax-1cn 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8222  df-wrecs 8253  df-recs 8302  df-rdg 8340  df-nn 12147  df-2 12209  df-3 12210  df-4 12211  df-5 12212  df-6 12213  df-7 12214  df-8 12215

This theorem is referenced by:  9nn  12244  8nn0  12425  37prm  17049  43prm  17050  83prm  17051  317prm  17054  1259lem4  17062  1259lem5  17063  2503prm  17068  4001prm  17073  ipndx  17251  ipid  17252  ipsstr  17257  phlstr  17267  quart1cl  26804  quart1lem  26805  quart1  26806  log2tlbnd  26895  bposlem8  27242  lgsdir2lem2  27277  lgsdir2lem3  27278  2lgslem3a1  27351  2lgslem3b1  27352  2lgslem3c1  27353  2lgslem3d1  27354  2lgslem4  27357  2lgsoddprmlem2  27360  pntlemr  27553  pntlemj  27554  edgfid  29047  edgfndx  29048  edgfndxnn  29049  ex-prmo  30518  hgt750lem  34801  hgt750lem2  34802  420gcd8e4  42437  420lcm8e840  42442  lcm8un  42451  lcmineqlem23  42482  lcmineqlem  42483  3lexlogpow5ineq2  42486  3lexlogpow2ineq1  42489  8ne0  42694  rmydioph  43445  fmtnoprmfac2lem1  48000  127prm  48033  mod42tp1mod8  48036  8even  48147  8exp8mod9  48170  9fppr8  48171  nfermltl8rev  48176  nfermltlrev  48178  nnsum4primesevenALTV  48235  wtgoldbnnsum4prm  48236  bgoldbnnsum3prm  48238  bgoldbtbndlem1  48239  tgblthelfgott  48249  tgoldbachlt  48250