Theorem 8nn 11714

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 11688	. 2 ⊢ 8 = (7 + 1)
2		7nn 11711	. . 3 ⊢ 7 ∈ ℕ
3		peano2nn 11631	. . 3 ⊢ (7 ∈ ℕ → (7 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (7 + 1) ∈ ℕ
5	1, 4	eqeltri 2907	1 ⊢ 8 ∈ ℕ

Syntax hints:   ∈ wcel 2114  (class class class)co 7137  1c1 10519   + caddc 10521  ℕcn 11619  7c7 11679  8c8 11680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7442  ax-1cn 10576

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3012  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3483  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3935  df-pss 3937  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-tp 4553  df-op 4555  df-uni 4820  df-iun 4902  df-br 5048  df-opab 5110  df-mpt 5128  df-tr 5154  df-id 5441  df-eprel 5446  df-po 5455  df-so 5456  df-fr 5495  df-we 5497  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-ov 7140  df-om 7562  df-wrecs 7928  df-recs 7989  df-rdg 8027  df-nn 11620  df-2 11682  df-3 11683  df-4 11684  df-5 11685  df-6 11686  df-7 11687  df-8 11688

This theorem is referenced by:  9nn  11717  8nn0  11902  37prm  16432  43prm  16433  83prm  16434  317prm  16437  1259lem4  16445  1259lem5  16446  2503prm  16451  4001prm  16456  ipndx  16619  ipid  16620  ipsstr  16621  ressip  16630  phlstr  16631  tngip  23234  quart1cl  25413  quart1lem  25414  quart1  25415  log2tlbnd  25504  bposlem8  25848  lgsdir2lem2  25883  lgsdir2lem3  25884  2lgslem3a1  25957  2lgslem3b1  25958  2lgslem3c1  25959  2lgslem3d1  25960  2lgslem4  25963  2lgsoddprmlem2  25966  pntlemr  26159  pntlemj  26160  edgfid  26757  edgfndxnn  26758  edgfndxid  26759  baseltedgf  26760  ex-prmo  28217  hgt750lem  31924  hgt750lem2  31925  420gcd8e4  39139  420lcm8e840  39144  lcm8un  39162  rmydioph  39698  fmtnoprmfac2lem1  43808  127prm  43843  mod42tp1mod8  43847  8even  43958  8exp8mod9  43981  9fppr8  43982  nfermltl8rev  43987  nfermltlrev  43989  nnsum4primesevenALTV  44046  wtgoldbnnsum4prm  44047  bgoldbnnsum3prm  44049  bgoldbtbndlem1  44050  tgblthelfgott  44060  tgoldbachlt  44061