Theorem 8cn 12278

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 12250	. 2 ⊢ 8 = (7 + 1)
2		7cn 12275	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11151	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2832	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036  1c1 11039   + caddc 11041  7c7 12241  8c8 12242

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-ext 2708  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249  df-8 12250

This theorem is referenced by:  9cn  12281  9m1e8  12310  8p2e10  12724  8t2e16  12759  8t5e40  12762  cos2bnd  16155  2exp11  17060  2exp16  17061  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001prm  17115  quart1cl  26818  quart1lem  26819  quart1  26820  quartlem1  26821  log2tlbnd  26909  log2ublem3  26912  log2ub  26913  bposlem8  27254  lgsdir2lem1  27288  lgsdir2lem5  27292  2lgslem3a  27359  2lgslem3b  27360  2lgslem3c  27361  2lgslem3d  27362  2lgslem3a1  27363  2lgslem3b1  27364  2lgslem3c1  27365  2lgslem3d1  27366  2lgsoddprmlem1  27371  2lgsoddprmlem2  27372  2lgsoddprmlem3a  27373  2lgsoddprmlem3b  27374  2lgsoddprmlem3c  27375  2lgsoddprmlem3d  27376  ex-exp  30520  hgt750lem2  34796  420lcm8e840  42450  3exp7  42492  3lexlogpow5ineq1  42493  3lexlogpow5ineq5  42499  aks4d1p1  42515  sq8  42729  ex-decpmul  42738  resqrtvalex  44072  imsqrtvalex  44073  sin5tlem4  47324  sin5tlem5  47325  fmtno5lem4  48019  257prm  48024  fmtnoprmfac2lem1  48029  fmtno4prmfac  48035  fmtno4nprmfac193  48037  fmtno5faclem3  48044  m3prm  48055  139prmALT  48059  127prm  48062  m7prm  48063  5tcu2e40  48078  2exp340mod341  48209  8exp8mod9  48212  nfermltl8rev  48218  evengpop3  48274  tgoldbachlt  48292