Theorem 8cn 12309

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 12281	. 2 ⊢ 8 = (7 + 1)
2		7cn 12306	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11168	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11220	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2830	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108  1c1 11111   + caddc 11113  7c7 12272  8c8 12273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11168  ax-addcl 11170

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281

This theorem is referenced by:  9cn  12312  9m1e8  12346  8p2e10  12757  8t2e16  12792  8t5e40  12795  cos2bnd  16131  2exp11  17023  2exp16  17024  139prm  17057  163prm  17058  317prm  17059  631prm  17060  1259lem2  17065  1259lem3  17066  1259lem4  17067  1259lem5  17068  2503lem2  17071  2503lem3  17072  2503prm  17073  4001lem1  17074  4001lem2  17075  4001prm  17078  quart1cl  26359  quart1lem  26360  quart1  26361  quartlem1  26362  log2tlbnd  26450  log2ublem3  26453  log2ub  26454  bposlem8  26794  lgsdir2lem1  26828  lgsdir2lem5  26832  2lgslem3a  26899  2lgslem3b  26900  2lgslem3c  26901  2lgslem3d  26902  2lgslem3a1  26903  2lgslem3b1  26904  2lgslem3c1  26905  2lgslem3d1  26906  2lgsoddprmlem1  26911  2lgsoddprmlem2  26912  2lgsoddprmlem3a  26913  2lgsoddprmlem3b  26914  2lgsoddprmlem3c  26915  2lgsoddprmlem3d  26916  ex-exp  29703  hgt750lem2  33664  420lcm8e840  40876  3exp7  40918  3lexlogpow5ineq1  40919  3lexlogpow5ineq5  40925  aks4d1p1  40941  ex-decpmul  41206  resqrtvalex  42396  imsqrtvalex  42397  fmtno5lem4  46224  257prm  46229  fmtnoprmfac2lem1  46234  fmtno4prmfac  46240  fmtno4nprmfac193  46242  fmtno5faclem3  46249  m3prm  46260  139prmALT  46264  127prm  46267  m7prm  46268  5tcu2e40  46283  2exp340mod341  46401  8exp8mod9  46404  nfermltl8rev  46410  evengpop3  46466  tgoldbachlt  46484