Theorem 8cn 12480

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 12451	. 2 ⊢ 8 = (7 + 1)
2		7cn 12477	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11297	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11354	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2860	1 ⊢ 8 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2147  (class class class)co 7451  ℂcc 11237  1c1 11240   + caddc 11242  7c7 12442  8c8 12443

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-addcl 11299

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839  df-2 12445  df-3 12446  df-4 12447  df-5 12448  df-6 12449  df-7 12450  df-8 12451

This theorem is used by:  9cn  12483  9m1e8  12516  8th4div3  12606  8p2e10  12939  8t2e16  12974  8t5e40  12977  cos2bnd  16400  2exp11  17311  2exp16  17312  139prm  17346  163prm  17347  317prm  17348  631prm  17349  1259lem2  17354  1259lem3  17355  1259lem4  17356  1259lem5  17357  2503lem2  17360  2503lem3  17361  2503prm  17362  4001lem1  17363  4001lem2  17364  4001prm  17367  quart1cl  27239  quart1lem  27240  quart1  27241  quartlem1  27242  log2tlbnd  27330  log2ublem3  27333  log2ub  27334  bposlem8  27675  lgsdir2lem1  27709  lgsdir2lem5  27713  2lgslem3a  27780  2lgslem3b  27781  2lgslem3c  27782  2lgslem3d  27783  2lgslem3a1  27784  2lgslem3b1  27785  2lgslem3c1  27786  2lgslem3d1  27787  2lgsoddprmlem1  27792  2lgsoddprmlem2  27793  2lgsoddprmlem3a  27794  2lgsoddprmlem3b  27795  2lgsoddprmlem3c  27796  2lgsoddprmlem3d  27797  ex-exp  31108  hgt750lem2  35392  420lcm8e840  43327  3exp7  43369  3lexlogpow5ineq1  43370  3lexlogpow5ineq5  43376  aks4d1p1  43392  sq8  43620  ex-decpmul  43629  resqrtvalex  44906  imsqrtvalex  44907  sin5tlem4  48195  sin5tlem5  48196  fmtno5lem4  48914  257prm  48919  fmtnoprmfac2lem1  48924  fmtno4prmfac  48930  fmtno4nprmfac193  48932  fmtno5faclem3  48939  m3prm  48950  139prmALT  48954  127prm  48957  m7prm  48958  5tcu2e40  48973  2exp340mod341  49104  8exp8mod9  49107  nfermltl8rev  49113  evengpop3  49169  tgoldbachlt  49187