Theorem 8cn 12176

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 12148	. 2 ⊢ 8 = (7 + 1)
2		7cn 12173	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11035	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11087	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2834	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2106  (class class class)co 7342  ℂcc 10975  1c1 10978   + caddc 10980  7c7 12139  8c8 12140

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-1cn 11035  ax-addcl 11037

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1782  df-cleq 2729  df-clel 2815  df-2 12142  df-3 12143  df-4 12144  df-5 12145  df-6 12146  df-7 12147  df-8 12148

This theorem is referenced by:  9cn  12179  9m1e8  12213  8p2e10  12623  8t2e16  12658  8t5e40  12661  cos2bnd  15997  2exp11  16889  2exp16  16890  139prm  16923  163prm  16924  317prm  16925  631prm  16926  1259lem2  16931  1259lem3  16932  1259lem4  16933  1259lem5  16934  2503lem2  16937  2503lem3  16938  2503prm  16939  4001lem1  16940  4001lem2  16941  4001prm  16944  quart1cl  26110  quart1lem  26111  quart1  26112  quartlem1  26113  log2tlbnd  26201  log2ublem3  26204  log2ub  26205  bposlem8  26545  lgsdir2lem1  26579  lgsdir2lem5  26583  2lgslem3a  26650  2lgslem3b  26651  2lgslem3c  26652  2lgslem3d  26653  2lgslem3a1  26654  2lgslem3b1  26655  2lgslem3c1  26656  2lgslem3d1  26657  2lgsoddprmlem1  26662  2lgsoddprmlem2  26663  2lgsoddprmlem3a  26664  2lgsoddprmlem3b  26665  2lgsoddprmlem3c  26666  2lgsoddprmlem3d  26667  ex-exp  29102  hgt750lem2  32930  420lcm8e840  40322  3exp7  40364  3lexlogpow5ineq1  40365  3lexlogpow5ineq5  40371  aks4d1p1  40387  ex-decpmul  40629  resqrtvalex  41624  imsqrtvalex  41625  fmtno5lem4  45424  257prm  45429  fmtnoprmfac2lem1  45434  fmtno4prmfac  45440  fmtno4nprmfac193  45442  fmtno5faclem3  45449  m3prm  45460  139prmALT  45464  127prm  45467  m7prm  45468  5tcu2e40  45483  2exp340mod341  45601  8exp8mod9  45604  nfermltl8rev  45610  evengpop3  45666  tgoldbachlt  45684