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 11192	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11246	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2831	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7410  ℂcc 11132  1c1 11135   + caddc 11137  7c7 12305  8c8 12306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-1cn 11192  ax-addcl 11194

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-clel 2810  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  12793  8t2e16  12828  8t5e40  12831  cos2bnd  16211  2exp11  17114  2exp16  17115  139prm  17148  163prm  17149  317prm  17150  631prm  17151  1259lem2  17156  1259lem3  17157  1259lem4  17158  1259lem5  17159  2503lem2  17162  2503lem3  17163  2503prm  17164  4001lem1  17165  4001lem2  17166  4001prm  17169  quart1cl  26821  quart1lem  26822  quart1  26823  quartlem1  26824  log2tlbnd  26912  log2ublem3  26915  log2ub  26916  bposlem8  27259  lgsdir2lem1  27293  lgsdir2lem5  27297  2lgslem3a  27364  2lgslem3b  27365  2lgslem3c  27366  2lgslem3d  27367  2lgslem3a1  27368  2lgslem3b1  27369  2lgslem3c1  27370  2lgslem3d1  27371  2lgsoddprmlem1  27376  2lgsoddprmlem2  27377  2lgsoddprmlem3a  27378  2lgsoddprmlem3b  27379  2lgsoddprmlem3c  27380  2lgsoddprmlem3d  27381  ex-exp  30436  hgt750lem2  34689  420lcm8e840  42029  3exp7  42071  3lexlogpow5ineq1  42072  3lexlogpow5ineq5  42078  aks4d1p1  42094  sq8  42313  ex-decpmul  42322  resqrtvalex  43636  imsqrtvalex  43637  fmtno5lem4  47537  257prm  47542  fmtnoprmfac2lem1  47547  fmtno4prmfac  47553  fmtno4nprmfac193  47555  fmtno5faclem3  47562  m3prm  47573  139prmALT  47577  127prm  47580  m7prm  47581  5tcu2e40  47596  2exp340mod341  47714  8exp8mod9  47717  nfermltl8rev  47723  evengpop3  47779  tgoldbachlt  47797