Theorem 8cn 12290

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 12262	. 2 ⊢ 8 = (7 + 1)
2		7cn 12287	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11133	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11187	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2825	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073  1c1 11076   + caddc 11078  7c7 12253  8c8 12254

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-1cn 11133  ax-addcl 11135

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804  df-2 12256  df-3 12257  df-4 12258  df-5 12259  df-6 12260  df-7 12261  df-8 12262

This theorem is referenced by:  9cn  12293  9m1e8  12322  8p2e10  12736  8t2e16  12771  8t5e40  12774  cos2bnd  16163  2exp11  17067  2exp16  17068  139prm  17101  163prm  17102  317prm  17103  631prm  17104  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem2  17119  4001prm  17122  quart1cl  26771  quart1lem  26772  quart1  26773  quartlem1  26774  log2tlbnd  26862  log2ublem3  26865  log2ub  26866  bposlem8  27209  lgsdir2lem1  27243  lgsdir2lem5  27247  2lgslem3a  27314  2lgslem3b  27315  2lgslem3c  27316  2lgslem3d  27317  2lgslem3a1  27318  2lgslem3b1  27319  2lgslem3c1  27320  2lgslem3d1  27321  2lgsoddprmlem1  27326  2lgsoddprmlem2  27327  2lgsoddprmlem3a  27328  2lgsoddprmlem3b  27329  2lgsoddprmlem3c  27330  2lgsoddprmlem3d  27331  ex-exp  30386  hgt750lem2  34650  420lcm8e840  42006  3exp7  42048  3lexlogpow5ineq1  42049  3lexlogpow5ineq5  42055  aks4d1p1  42071  sq8  42292  ex-decpmul  42301  resqrtvalex  43641  imsqrtvalex  43642  fmtno5lem4  47561  257prm  47566  fmtnoprmfac2lem1  47571  fmtno4prmfac  47577  fmtno4nprmfac193  47579  fmtno5faclem3  47586  m3prm  47597  139prmALT  47601  127prm  47604  m7prm  47605  5tcu2e40  47620  2exp340mod341  47738  8exp8mod9  47741  nfermltl8rev  47747  evengpop3  47803  tgoldbachlt  47821