Theorem 8cn 12361

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 12333	. 2 ⊢ 8 = (7 + 1)
2		7cn 12358	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11211	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11265	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2835	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2106  (class class class)co 7431  ℂcc 11151  1c1 11154   + caddc 11156  7c7 12324  8c8 12325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-1cn 11211  ax-addcl 11213

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-clel 2814  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333

This theorem is referenced by:  9cn  12364  9m1e8  12398  8p2e10  12811  8t2e16  12846  8t5e40  12849  cos2bnd  16221  2exp11  17124  2exp16  17125  139prm  17158  163prm  17159  317prm  17160  631prm  17161  1259lem2  17166  1259lem3  17167  1259lem4  17168  1259lem5  17169  2503lem2  17172  2503lem3  17173  2503prm  17174  4001lem1  17175  4001lem2  17176  4001prm  17179  quart1cl  26912  quart1lem  26913  quart1  26914  quartlem1  26915  log2tlbnd  27003  log2ublem3  27006  log2ub  27007  bposlem8  27350  lgsdir2lem1  27384  lgsdir2lem5  27388  2lgslem3a  27455  2lgslem3b  27456  2lgslem3c  27457  2lgslem3d  27458  2lgslem3a1  27459  2lgslem3b1  27460  2lgslem3c1  27461  2lgslem3d1  27462  2lgsoddprmlem1  27467  2lgsoddprmlem2  27468  2lgsoddprmlem3a  27469  2lgsoddprmlem3b  27470  2lgsoddprmlem3c  27471  2lgsoddprmlem3d  27472  ex-exp  30479  hgt750lem2  34646  420lcm8e840  41993  3exp7  42035  3lexlogpow5ineq1  42036  3lexlogpow5ineq5  42042  aks4d1p1  42058  sq8  42310  ex-decpmul  42319  resqrtvalex  43635  imsqrtvalex  43636  fmtno5lem4  47481  257prm  47486  fmtnoprmfac2lem1  47491  fmtno4prmfac  47497  fmtno4nprmfac193  47499  fmtno5faclem3  47506  m3prm  47517  139prmALT  47521  127prm  47524  m7prm  47525  5tcu2e40  47540  2exp340mod341  47658  8exp8mod9  47661  nfermltl8rev  47667  evengpop3  47723  tgoldbachlt  47741