Theorem 8cn 11735

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 11707	. 2 ⊢ 8 = (7 + 1)
2		7cn 11732	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 10595	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10647	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2909	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535  1c1 10538   + caddc 10540  7c7 11698  8c8 11699

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-ext 2793  ax-1cn 10595  ax-addcl 10597

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893  df-2 11701  df-3 11702  df-4 11703  df-5 11704  df-6 11705  df-7 11706  df-8 11707

This theorem is referenced by:  9cn  11738  9m1e8  11772  8p2e10  12179  8t2e16  12214  8t5e40  12217  cos2bnd  15541  2exp16  16424  139prm  16457  163prm  16458  317prm  16459  631prm  16460  1259lem2  16465  1259lem3  16466  1259lem4  16467  1259lem5  16468  2503lem2  16471  2503lem3  16472  2503prm  16473  4001lem1  16474  4001lem2  16475  4001prm  16478  quart1cl  25432  quart1lem  25433  quart1  25434  quartlem1  25435  log2tlbnd  25523  log2ublem3  25526  log2ub  25527  bposlem8  25867  lgsdir2lem1  25901  lgsdir2lem5  25905  2lgslem3a  25972  2lgslem3b  25973  2lgslem3c  25974  2lgslem3d  25975  2lgslem3a1  25976  2lgslem3b1  25977  2lgslem3c1  25978  2lgslem3d1  25979  2lgsoddprmlem1  25984  2lgsoddprmlem2  25985  2lgsoddprmlem3a  25986  2lgsoddprmlem3b  25987  2lgsoddprmlem3c  25988  2lgsoddprmlem3d  25989  ex-exp  28229  hgt750lem2  31923  ex-decpmul  39198  fmtno5lem4  43738  257prm  43743  fmtnoprmfac2lem1  43748  fmtno4prmfac  43754  fmtno4nprmfac193  43756  fmtno5faclem3  43763  m3prm  43774  139prmALT  43779  127prm  43783  m7prm  43784  2exp11  43785  5tcu2e40  43800  2exp340mod341  43918  8exp8mod9  43921  nfermltl8rev  43927  evengpop3  43983  tgoldbachlt  44001