Theorem 8cn 12390

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 12362	. 2 ⊢ 8 = (7 + 1)
2		7cn 12387	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11242	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11296	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2840	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182  1c1 11185   + caddc 11187  7c7 12353  8c8 12354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-addcl 11244

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361  df-8 12362

This theorem is referenced by:  9cn  12393  9m1e8  12427  8p2e10  12838  8t2e16  12873  8t5e40  12876  cos2bnd  16236  2exp11  17137  2exp16  17138  139prm  17171  163prm  17172  317prm  17173  631prm  17174  1259lem2  17179  1259lem3  17180  1259lem4  17181  1259lem5  17182  2503lem2  17185  2503lem3  17186  2503prm  17187  4001lem1  17188  4001lem2  17189  4001prm  17192  quart1cl  26915  quart1lem  26916  quart1  26917  quartlem1  26918  log2tlbnd  27006  log2ublem3  27009  log2ub  27010  bposlem8  27353  lgsdir2lem1  27387  lgsdir2lem5  27391  2lgslem3a  27458  2lgslem3b  27459  2lgslem3c  27460  2lgslem3d  27461  2lgslem3a1  27462  2lgslem3b1  27463  2lgslem3c1  27464  2lgslem3d1  27465  2lgsoddprmlem1  27470  2lgsoddprmlem2  27471  2lgsoddprmlem3a  27472  2lgsoddprmlem3b  27473  2lgsoddprmlem3c  27474  2lgsoddprmlem3d  27475  ex-exp  30482  hgt750lem2  34629  420lcm8e840  41968  3exp7  42010  3lexlogpow5ineq1  42011  3lexlogpow5ineq5  42017  aks4d1p1  42033  sq8  42285  ex-decpmul  42294  resqrtvalex  43607  imsqrtvalex  43608  fmtno5lem4  47430  257prm  47435  fmtnoprmfac2lem1  47440  fmtno4prmfac  47446  fmtno4nprmfac193  47448  fmtno5faclem3  47455  m3prm  47466  139prmALT  47470  127prm  47473  m7prm  47474  5tcu2e40  47489  2exp340mod341  47607  8exp8mod9  47610  nfermltl8rev  47616  evengpop3  47672  tgoldbachlt  47690