Theorem 8cn 12440

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 12411	. 2 ⊢ 8 = (7 + 1)
2		7cn 12437	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11258	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11315	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2857	1 ⊢ 8 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7420  ℂcc 11198  1c1 11201   + caddc 11203  7c7 12402  8c8 12403

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11258  ax-addcl 11260

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836  df-2 12405  df-3 12406  df-4 12407  df-5 12408  df-6 12409  df-7 12410  df-8 12411

This theorem is used by:  9cn  12443  9m1e8  12476  8th4div3  12566  8p2e10  12899  8t2e16  12934  8t5e40  12937  cos2bnd  16356  2exp11  17267  2exp16  17268  139prm  17302  163prm  17303  317prm  17304  631prm  17305  1259lem2  17310  1259lem3  17311  1259lem4  17312  1259lem5  17313  2503lem2  17316  2503lem3  17317  2503prm  17318  4001lem1  17319  4001lem2  17320  4001prm  17323  quart1cl  27182  quart1lem  27183  quart1  27184  quartlem1  27185  log2tlbnd  27273  log2ublem3  27276  log2ub  27277  bposlem8  27618  lgsdir2lem1  27652  lgsdir2lem5  27656  2lgslem3a  27723  2lgslem3b  27724  2lgslem3c  27725  2lgslem3d  27726  2lgslem3a1  27727  2lgslem3b1  27728  2lgslem3c1  27729  2lgslem3d1  27730  2lgsoddprmlem1  27735  2lgsoddprmlem2  27736  2lgsoddprmlem3a  27737  2lgsoddprmlem3b  27738  2lgsoddprmlem3c  27739  2lgsoddprmlem3d  27740  ex-exp  31051  hgt750lem2  35281  420lcm8e840  43061  3exp7  43103  3lexlogpow5ineq1  43104  3lexlogpow5ineq5  43110  aks4d1p1  43126  sq8  43354  ex-decpmul  43363  resqrtvalex  44644  imsqrtvalex  44645  sin5tlem4  47921  sin5tlem5  47922  fmtno5lem4  48640  257prm  48645  fmtnoprmfac2lem1  48650  fmtno4prmfac  48656  fmtno4nprmfac193  48658  fmtno5faclem3  48665  m3prm  48676  139prmALT  48680  127prm  48683  m7prm  48684  5tcu2e40  48699  2exp340mod341  48830  8exp8mod9  48833  nfermltl8rev  48839  evengpop3  48895  tgoldbachlt  48913