Theorem 8cn 12222

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 12194	. 2 ⊢ 8 = (7 + 1)
2		7cn 12219	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11064	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11118	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2827	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004  1c1 11007   + caddc 11009  7c7 12185  8c8 12186

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11064  ax-addcl 11066

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-2 12188  df-3 12189  df-4 12190  df-5 12191  df-6 12192  df-7 12193  df-8 12194

This theorem is referenced by:  9cn  12225  9m1e8  12254  8p2e10  12668  8t2e16  12703  8t5e40  12706  cos2bnd  16097  2exp11  17001  2exp16  17002  139prm  17035  163prm  17036  317prm  17037  631prm  17038  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001prm  17056  quart1cl  26791  quart1lem  26792  quart1  26793  quartlem1  26794  log2tlbnd  26882  log2ublem3  26885  log2ub  26886  bposlem8  27229  lgsdir2lem1  27263  lgsdir2lem5  27267  2lgslem3a  27334  2lgslem3b  27335  2lgslem3c  27336  2lgslem3d  27337  2lgslem3a1  27338  2lgslem3b1  27339  2lgslem3c1  27340  2lgslem3d1  27341  2lgsoddprmlem1  27346  2lgsoddprmlem2  27347  2lgsoddprmlem3a  27348  2lgsoddprmlem3b  27349  2lgsoddprmlem3c  27350  2lgsoddprmlem3d  27351  ex-exp  30430  hgt750lem2  34665  420lcm8e840  42114  3exp7  42156  3lexlogpow5ineq1  42157  3lexlogpow5ineq5  42163  aks4d1p1  42179  sq8  42400  ex-decpmul  42409  resqrtvalex  43748  imsqrtvalex  43749  fmtno5lem4  47666  257prm  47671  fmtnoprmfac2lem1  47676  fmtno4prmfac  47682  fmtno4nprmfac193  47684  fmtno5faclem3  47691  m3prm  47702  139prmALT  47706  127prm  47709  m7prm  47710  5tcu2e40  47725  2exp340mod341  47843  8exp8mod9  47846  nfermltl8rev  47852  evengpop3  47908  tgoldbachlt  47926