Theorem 8cn 11892

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 11864	. 2 ⊢ 8 = (7 + 1)
2		7cn 11889	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 10752	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10804	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2827	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2112  (class class class)co 7191  ℂcc 10692  1c1 10695   + caddc 10697  7c7 11855  8c8 11856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-1cn 10752  ax-addcl 10754

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-clel 2809  df-2 11858  df-3 11859  df-4 11860  df-5 11861  df-6 11862  df-7 11863  df-8 11864

This theorem is referenced by:  9cn  11895  9m1e8  11929  8p2e10  12338  8t2e16  12373  8t5e40  12376  cos2bnd  15712  2exp11  16606  2exp16  16607  139prm  16640  163prm  16641  317prm  16642  631prm  16643  1259lem2  16648  1259lem3  16649  1259lem4  16650  1259lem5  16651  2503lem2  16654  2503lem3  16655  2503prm  16656  4001lem1  16657  4001lem2  16658  4001prm  16661  quart1cl  25691  quart1lem  25692  quart1  25693  quartlem1  25694  log2tlbnd  25782  log2ublem3  25785  log2ub  25786  bposlem8  26126  lgsdir2lem1  26160  lgsdir2lem5  26164  2lgslem3a  26231  2lgslem3b  26232  2lgslem3c  26233  2lgslem3d  26234  2lgslem3a1  26235  2lgslem3b1  26236  2lgslem3c1  26237  2lgslem3d1  26238  2lgsoddprmlem1  26243  2lgsoddprmlem2  26244  2lgsoddprmlem3a  26245  2lgsoddprmlem3b  26246  2lgsoddprmlem3c  26247  2lgsoddprmlem3d  26248  ex-exp  28487  hgt750lem2  32298  420lcm8e840  39702  3exp7  39744  3lexlogpow5ineq1  39745  3lexlogpow5ineq5  39751  aks4d1p1  39766  ex-decpmul  39968  resqrtvalex  40870  imsqrtvalex  40871  fmtno5lem4  44624  257prm  44629  fmtnoprmfac2lem1  44634  fmtno4prmfac  44640  fmtno4nprmfac193  44642  fmtno5faclem3  44649  m3prm  44660  139prmALT  44664  127prm  44667  m7prm  44668  5tcu2e40  44683  2exp340mod341  44801  8exp8mod9  44804  nfermltl8rev  44810  evengpop3  44866  tgoldbachlt  44884