Theorem 8cn 12450

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 12421	. 2 ⊢ 8 = (7 + 1)
2		7cn 12447	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11268	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11325	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2859	1 ⊢ 8 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7427  ℂcc 11208  1c1 11211   + caddc 11213  7c7 12412  8c8 12413

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-1cn 11268  ax-addcl 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-clel 2838  df-2 12415  df-3 12416  df-4 12417  df-5 12418  df-6 12419  df-7 12420  df-8 12421

This theorem is used by:  9cn  12453  9m1e8  12486  8th4div3  12576  8p2e10  12909  8t2e16  12944  8t5e40  12947  cos2bnd  16368  2exp11  17279  2exp16  17280  139prm  17314  163prm  17315  317prm  17316  631prm  17317  1259lem2  17322  1259lem3  17323  1259lem4  17324  1259lem5  17325  2503lem2  17328  2503lem3  17329  2503prm  17330  4001lem1  17331  4001lem2  17332  4001prm  17335  quart1cl  27194  quart1lem  27195  quart1  27196  quartlem1  27197  log2tlbnd  27285  log2ublem3  27288  log2ub  27289  bposlem8  27630  lgsdir2lem1  27664  lgsdir2lem5  27668  2lgslem3a  27735  2lgslem3b  27736  2lgslem3c  27737  2lgslem3d  27738  2lgslem3a1  27739  2lgslem3b1  27740  2lgslem3c1  27741  2lgslem3d1  27742  2lgsoddprmlem1  27747  2lgsoddprmlem2  27748  2lgsoddprmlem3a  27749  2lgsoddprmlem3b  27750  2lgsoddprmlem3c  27751  2lgsoddprmlem3d  27752  ex-exp  31063  hgt750lem2  35334  420lcm8e840  43201  3exp7  43243  3lexlogpow5ineq1  43244  3lexlogpow5ineq5  43250  aks4d1p1  43266  sq8  43494  ex-decpmul  43503  resqrtvalex  44785  imsqrtvalex  44786  sin5tlem4  48061  sin5tlem5  48062  fmtno5lem4  48780  257prm  48785  fmtnoprmfac2lem1  48790  fmtno4prmfac  48796  fmtno4nprmfac193  48798  fmtno5faclem3  48805  m3prm  48816  139prmALT  48820  127prm  48823  m7prm  48824  5tcu2e40  48839  2exp340mod341  48970  8exp8mod9  48973  nfermltl8rev  48979  evengpop3  49035  tgoldbachlt  49053