Theorem 8cn 12254

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 12226	. 2 ⊢ 8 = (7 + 1)
2		7cn 12251	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11150	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2833	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036  1c1 11039   + caddc 11041  7c7 12217  8c8 12218

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-2 12220  df-3 12221  df-4 12222  df-5 12223  df-6 12224  df-7 12225  df-8 12226

This theorem is referenced by:  9cn  12257  9m1e8  12286  8p2e10  12699  8t2e16  12734  8t5e40  12737  cos2bnd  16125  2exp11  17029  2exp16  17030  139prm  17063  163prm  17064  317prm  17065  631prm  17066  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  2503lem2  17077  2503lem3  17078  2503prm  17079  4001lem1  17080  4001lem2  17081  4001prm  17084  quart1cl  26835  quart1lem  26836  quart1  26837  quartlem1  26838  log2tlbnd  26926  log2ublem3  26929  log2ub  26930  bposlem8  27273  lgsdir2lem1  27307  lgsdir2lem5  27311  2lgslem3a  27378  2lgslem3b  27379  2lgslem3c  27380  2lgslem3d  27381  2lgslem3a1  27382  2lgslem3b1  27383  2lgslem3c1  27384  2lgslem3d1  27385  2lgsoddprmlem1  27390  2lgsoddprmlem2  27391  2lgsoddprmlem3a  27392  2lgsoddprmlem3b  27393  2lgsoddprmlem3c  27394  2lgsoddprmlem3d  27395  ex-exp  30541  hgt750lem2  34834  420lcm8e840  42385  3exp7  42427  3lexlogpow5ineq1  42428  3lexlogpow5ineq5  42434  aks4d1p1  42450  sq8  42671  ex-decpmul  42680  resqrtvalex  44005  imsqrtvalex  44006  fmtno5lem4  47920  257prm  47925  fmtnoprmfac2lem1  47930  fmtno4prmfac  47936  fmtno4nprmfac193  47938  fmtno5faclem3  47945  m3prm  47956  139prmALT  47960  127prm  47963  m7prm  47964  5tcu2e40  47979  2exp340mod341  48097  8exp8mod9  48100  nfermltl8rev  48106  evengpop3  48162  tgoldbachlt  48180