Theorem 8cn 12283

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 12255	. 2 ⊢ 8 = (7 + 1)
2		7cn 12280	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11126	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11180	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066  1c1 11069   + caddc 11071  7c7 12246  8c8 12247

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-addcl 11128

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12249  df-3 12250  df-4 12251  df-5 12252  df-6 12253  df-7 12254  df-8 12255

This theorem is referenced by:  9cn  12286  9m1e8  12315  8p2e10  12729  8t2e16  12764  8t5e40  12767  cos2bnd  16156  2exp11  17060  2exp16  17061  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001prm  17115  quart1cl  26764  quart1lem  26765  quart1  26766  quartlem1  26767  log2tlbnd  26855  log2ublem3  26858  log2ub  26859  bposlem8  27202  lgsdir2lem1  27236  lgsdir2lem5  27240  2lgslem3a  27307  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  2lgslem3a1  27311  2lgslem3b1  27312  2lgslem3c1  27313  2lgslem3d1  27314  2lgsoddprmlem1  27319  2lgsoddprmlem2  27320  2lgsoddprmlem3a  27321  2lgsoddprmlem3b  27322  2lgsoddprmlem3c  27323  2lgsoddprmlem3d  27324  ex-exp  30379  hgt750lem2  34643  420lcm8e840  41999  3exp7  42041  3lexlogpow5ineq1  42042  3lexlogpow5ineq5  42048  aks4d1p1  42064  sq8  42285  ex-decpmul  42294  resqrtvalex  43634  imsqrtvalex  43635  fmtno5lem4  47557  257prm  47562  fmtnoprmfac2lem1  47567  fmtno4prmfac  47573  fmtno4nprmfac193  47575  fmtno5faclem3  47582  m3prm  47593  139prmALT  47597  127prm  47600  m7prm  47601  5tcu2e40  47616  2exp340mod341  47734  8exp8mod9  47737  nfermltl8rev  47743  evengpop3  47799  tgoldbachlt  47817