Theorem 8cn 11548

Description: The number 8 is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)

Assertion

Ref	Expression
8cn	⊢ 8 ∈ ℂ

Proof of Theorem 8cn

Step	Hyp	Ref	Expression
1		df-8 11515	. 2 ⊢ 8 = (7 + 1)
2		7cn 11544	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 10399	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10452	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2864	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2051  (class class class)co 6982  ℂcc 10339  1c1 10342   + caddc 10344  7c7 11506  8c8 11507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-ext 2752  ax-1cn 10399  ax-addcl 10401

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-cleq 2773  df-clel 2848  df-2 11509  df-3 11510  df-4 11511  df-5 11512  df-6 11513  df-7 11514  df-8 11515

This theorem is referenced by:  9cn  11552  9m1e8  11587  8p2e10  11999  8t2e16  12034  8t5e40  12037  cos2bnd  15407  2exp16  16286  139prm  16319  163prm  16320  317prm  16321  631prm  16322  1259lem2  16327  1259lem3  16328  1259lem4  16329  1259lem5  16330  2503lem2  16333  2503lem3  16334  2503prm  16335  4001lem1  16336  4001lem2  16337  4001prm  16340  quart1cl  25148  quart1lem  25149  quart1  25150  quartlem1  25151  log2tlbnd  25240  log2ublem3  25243  log2ub  25244  bposlem8  25584  lgsdir2lem1  25618  lgsdir2lem5  25622  2lgslem3a  25689  2lgslem3b  25690  2lgslem3c  25691  2lgslem3d  25692  2lgslem3a1  25693  2lgslem3b1  25694  2lgslem3c1  25695  2lgslem3d1  25696  2lgsoddprmlem1  25701  2lgsoddprmlem2  25702  2lgsoddprmlem3a  25703  2lgsoddprmlem3b  25704  2lgsoddprmlem3c  25705  2lgsoddprmlem3d  25706  ex-exp  28022  hgt750lem2  31603  ex-decpmul  38651  fmtno5lem4  43121  257prm  43126  fmtnoprmfac2lem1  43131  fmtno4prmfac  43137  fmtno4nprmfac193  43139  fmtno5faclem3  43146  m3prm  43157  139prmALT  43162  127prm  43166  m7prm  43167  2exp11  43168  5tcu2e40  43183  2exp340mod341  43301  8exp8mod9  43304  nfermltl8rev  43310  evengpop3  43366  tgoldbachlt  43384