Theorem 8cn 12342

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 12314	. 2 ⊢ 8 = (7 + 1)
2		7cn 12339	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11198	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11252	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2821	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2098  (class class class)co 7419  ℂcc 11138  1c1 11141   + caddc 11143  7c7 12305  8c8 12306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-1cn 11198  ax-addcl 11200

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-clel 2802  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312  df-7 12313  df-8 12314

This theorem is referenced by:  9cn  12345  9m1e8  12379  8p2e10  12790  8t2e16  12825  8t5e40  12828  cos2bnd  16168  2exp11  17062  2exp16  17063  139prm  17096  163prm  17097  317prm  17098  631prm  17099  1259lem2  17104  1259lem3  17105  1259lem4  17106  1259lem5  17107  2503lem2  17110  2503lem3  17111  2503prm  17112  4001lem1  17113  4001lem2  17114  4001prm  17117  quart1cl  26831  quart1lem  26832  quart1  26833  quartlem1  26834  log2tlbnd  26922  log2ublem3  26925  log2ub  26926  bposlem8  27269  lgsdir2lem1  27303  lgsdir2lem5  27307  2lgslem3a  27374  2lgslem3b  27375  2lgslem3c  27376  2lgslem3d  27377  2lgslem3a1  27378  2lgslem3b1  27379  2lgslem3c1  27380  2lgslem3d1  27381  2lgsoddprmlem1  27386  2lgsoddprmlem2  27387  2lgsoddprmlem3a  27388  2lgsoddprmlem3b  27389  2lgsoddprmlem3c  27390  2lgsoddprmlem3d  27391  ex-exp  30332  hgt750lem2  34415  420lcm8e840  41614  3exp7  41656  3lexlogpow5ineq1  41657  3lexlogpow5ineq5  41663  aks4d1p1  41679  ex-decpmul  42003  resqrtvalex  43217  imsqrtvalex  43218  fmtno5lem4  47033  257prm  47038  fmtnoprmfac2lem1  47043  fmtno4prmfac  47049  fmtno4nprmfac193  47051  fmtno5faclem3  47058  m3prm  47069  139prmALT  47073  127prm  47076  m7prm  47077  5tcu2e40  47092  2exp340mod341  47210  8exp8mod9  47213  nfermltl8rev  47219  evengpop3  47275  tgoldbachlt  47293