Theorem 8cn 12079

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 12051	. 2 ⊢ 8 = (7 + 1)
2		7cn 12076	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 10938	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10990	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2836	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2107  (class class class)co 7284  ℂcc 10878  1c1 10881   + caddc 10883  7c7 12042  8c8 12043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-1cn 10938  ax-addcl 10940

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817  df-2 12045  df-3 12046  df-4 12047  df-5 12048  df-6 12049  df-7 12050  df-8 12051

This theorem is referenced by:  9cn  12082  9m1e8  12116  8p2e10  12526  8t2e16  12561  8t5e40  12564  cos2bnd  15906  2exp11  16800  2exp16  16801  139prm  16834  163prm  16835  317prm  16836  631prm  16837  1259lem2  16842  1259lem3  16843  1259lem4  16844  1259lem5  16845  2503lem2  16848  2503lem3  16849  2503prm  16850  4001lem1  16851  4001lem2  16852  4001prm  16855  quart1cl  26013  quart1lem  26014  quart1  26015  quartlem1  26016  log2tlbnd  26104  log2ublem3  26107  log2ub  26108  bposlem8  26448  lgsdir2lem1  26482  lgsdir2lem5  26486  2lgslem3a  26553  2lgslem3b  26554  2lgslem3c  26555  2lgslem3d  26556  2lgslem3a1  26557  2lgslem3b1  26558  2lgslem3c1  26559  2lgslem3d1  26560  2lgsoddprmlem1  26565  2lgsoddprmlem2  26566  2lgsoddprmlem3a  26567  2lgsoddprmlem3b  26568  2lgsoddprmlem3c  26569  2lgsoddprmlem3d  26570  ex-exp  28823  hgt750lem2  32641  420lcm8e840  40026  3exp7  40068  3lexlogpow5ineq1  40069  3lexlogpow5ineq5  40075  aks4d1p1  40091  ex-decpmul  40327  resqrtvalex  41260  imsqrtvalex  41261  fmtno5lem4  45019  257prm  45024  fmtnoprmfac2lem1  45029  fmtno4prmfac  45035  fmtno4nprmfac193  45037  fmtno5faclem3  45044  m3prm  45055  139prmALT  45059  127prm  45062  m7prm  45063  5tcu2e40  45078  2exp340mod341  45196  8exp8mod9  45199  nfermltl8rev  45205  evengpop3  45261  tgoldbachlt  45279