Theorem 8cn 12355

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 12326	. 2 ⊢ 8 = (7 + 1)
2		7cn 12352	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11175	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11232	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2861	1 ⊢ 8 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7419  ℂcc 11115  1c1 11118   + caddc 11120  7c7 12317  8c8 12318

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-1cn 11175  ax-addcl 11177

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840  df-2 12320  df-3 12321  df-4 12322  df-5 12323  df-6 12324  df-7 12325  df-8 12326

This theorem is used by:  9cn  12358  9m1e8  12391  8th4div3  12481  8p2e10  12814  8t2e16  12849  8t5e40  12852  cos2bnd  16268  2exp11  17173  2exp16  17174  139prm  17208  163prm  17209  317prm  17210  631prm  17211  1259lem2  17216  1259lem3  17217  1259lem4  17218  1259lem5  17219  2503lem2  17222  2503lem3  17223  2503prm  17224  4001lem1  17225  4001lem2  17226  4001prm  17229  quart1cl  27072  quart1lem  27073  quart1  27074  quartlem1  27075  log2tlbnd  27163  log2ublem3  27166  log2ub  27167  bposlem8  27508  lgsdir2lem1  27542  lgsdir2lem5  27546  2lgslem3a  27613  2lgslem3b  27614  2lgslem3c  27615  2lgslem3d  27616  2lgslem3a1  27617  2lgslem3b1  27618  2lgslem3c1  27619  2lgslem3d1  27620  2lgsoddprmlem1  27625  2lgsoddprmlem2  27626  2lgsoddprmlem3a  27627  2lgsoddprmlem3b  27628  2lgsoddprmlem3c  27629  2lgsoddprmlem3d  27630  ex-exp  30874  hgt750lem2  35106  420lcm8e840  42838  3exp7  42880  3lexlogpow5ineq1  42881  3lexlogpow5ineq5  42887  aks4d1p1  42903  sq8  43118  ex-decpmul  43127  resqrtvalex  44431  imsqrtvalex  44432  sin5tlem4  47673  sin5tlem5  47674  fmtno5lem4  48368  257prm  48373  fmtnoprmfac2lem1  48378  fmtno4prmfac  48384  fmtno4nprmfac193  48386  fmtno5faclem3  48393  m3prm  48404  139prmALT  48408  127prm  48411  m7prm  48412  5tcu2e40  48427  2exp340mod341  48558  8exp8mod9  48561  nfermltl8rev  48567  evengpop3  48623  tgoldbachlt  48641