Theorem 8cn 12334

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 12305	. 2 ⊢ 8 = (7 + 1)
2		7cn 12331	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11154	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11211	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2865	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2149  (class class class)co 7408  ℂcc 11094  1c1 11097   + caddc 11099  7c7 12296  8c8 12297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11154  ax-addcl 11156

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844  df-2 12299  df-3 12300  df-4 12301  df-5 12302  df-6 12303  df-7 12304  df-8 12305

This theorem is referenced by:  9cn  12337  9m1e8  12370  8p2e10  12792  8t2e16  12827  8t5e40  12830  cos2bnd  16240  2exp11  17145  2exp16  17146  139prm  17180  163prm  17181  317prm  17182  631prm  17183  1259lem2  17188  1259lem3  17189  1259lem4  17190  1259lem5  17191  2503lem2  17194  2503lem3  17195  2503prm  17196  4001lem1  17197  4001lem2  17198  4001prm  17201  quart1cl  26981  quart1lem  26982  quart1  26983  quartlem1  26984  log2tlbnd  27072  log2ublem3  27075  log2ub  27076  bposlem8  27417  lgsdir2lem1  27451  lgsdir2lem5  27455  2lgslem3a  27522  2lgslem3b  27523  2lgslem3c  27524  2lgslem3d  27525  2lgslem3a1  27526  2lgslem3b1  27527  2lgslem3c1  27528  2lgslem3d1  27529  2lgsoddprmlem1  27534  2lgsoddprmlem2  27535  2lgsoddprmlem3a  27536  2lgsoddprmlem3b  27537  2lgsoddprmlem3c  27538  2lgsoddprmlem3d  27539  ex-exp  30738  hgt750lem2  34980  420lcm8e840  42663  3exp7  42705  3lexlogpow5ineq1  42706  3lexlogpow5ineq5  42712  aks4d1p1  42728  sq8  42941  ex-decpmul  42950  resqrtvalex  44256  imsqrtvalex  44257  sin5tlem4  47495  sin5tlem5  47496  fmtno5lem4  48190  257prm  48195  fmtnoprmfac2lem1  48200  fmtno4prmfac  48206  fmtno4nprmfac193  48208  fmtno5faclem3  48215  m3prm  48226  139prmALT  48230  127prm  48233  m7prm  48234  5tcu2e40  48249  2exp340mod341  48380  8exp8mod9  48383  nfermltl8rev  48389  evengpop3  48445  tgoldbachlt  48463