Theorem 8cn 12363

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 12335	. 2 ⊢ 8 = (7 + 1)
2		7cn 12360	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11213	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11267	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2837	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153  1c1 11156   + caddc 11158  7c7 12326  8c8 12327

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-addcl 11215

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335

This theorem is referenced by:  9cn  12366  9m1e8  12400  8p2e10  12813  8t2e16  12848  8t5e40  12851  cos2bnd  16224  2exp11  17127  2exp16  17128  139prm  17161  163prm  17162  317prm  17163  631prm  17164  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  2503lem2  17175  2503lem3  17176  2503prm  17177  4001lem1  17178  4001lem2  17179  4001prm  17182  quart1cl  26897  quart1lem  26898  quart1  26899  quartlem1  26900  log2tlbnd  26988  log2ublem3  26991  log2ub  26992  bposlem8  27335  lgsdir2lem1  27369  lgsdir2lem5  27373  2lgslem3a  27440  2lgslem3b  27441  2lgslem3c  27442  2lgslem3d  27443  2lgslem3a1  27444  2lgslem3b1  27445  2lgslem3c1  27446  2lgslem3d1  27447  2lgsoddprmlem1  27452  2lgsoddprmlem2  27453  2lgsoddprmlem3a  27454  2lgsoddprmlem3b  27455  2lgsoddprmlem3c  27456  2lgsoddprmlem3d  27457  ex-exp  30469  hgt750lem2  34667  420lcm8e840  42012  3exp7  42054  3lexlogpow5ineq1  42055  3lexlogpow5ineq5  42061  aks4d1p1  42077  sq8  42331  ex-decpmul  42340  resqrtvalex  43658  imsqrtvalex  43659  fmtno5lem4  47543  257prm  47548  fmtnoprmfac2lem1  47553  fmtno4prmfac  47559  fmtno4nprmfac193  47561  fmtno5faclem3  47568  m3prm  47579  139prmALT  47583  127prm  47586  m7prm  47587  5tcu2e40  47602  2exp340mod341  47720  8exp8mod9  47723  nfermltl8rev  47729  evengpop3  47785  tgoldbachlt  47803