Theorem 8cn 12365

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 12336	. 2 ⊢ 8 = (7 + 1)
2		7cn 12362	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11185	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11242	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2856	1 ⊢ 8 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7414  ℂcc 11125  1c1 11128   + caddc 11130  7c7 12327  8c8 12328

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 2732  ax-1cn 11185  ax-addcl 11187

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335  df-8 12336

This theorem is used by:  9cn  12368  9m1e8  12401  8th4div3  12491  8p2e10  12824  8t2e16  12859  8t5e40  12862  cos2bnd  16279  2exp11  17184  2exp16  17185  139prm  17219  163prm  17220  317prm  17221  631prm  17222  1259lem2  17227  1259lem3  17228  1259lem4  17229  1259lem5  17230  2503lem2  17233  2503lem3  17234  2503prm  17235  4001lem1  17236  4001lem2  17237  4001prm  17240  quart1cl  27094  quart1lem  27095  quart1  27096  quartlem1  27097  log2tlbnd  27185  log2ublem3  27188  log2ub  27189  bposlem8  27530  lgsdir2lem1  27564  lgsdir2lem5  27568  2lgslem3a  27635  2lgslem3b  27636  2lgslem3c  27637  2lgslem3d  27638  2lgslem3a1  27639  2lgslem3b1  27640  2lgslem3c1  27641  2lgslem3d1  27642  2lgsoddprmlem1  27647  2lgsoddprmlem2  27648  2lgsoddprmlem3a  27649  2lgsoddprmlem3b  27650  2lgsoddprmlem3c  27651  2lgsoddprmlem3d  27652  ex-exp  30933  hgt750lem2  35163  420lcm8e840  42880  3exp7  42922  3lexlogpow5ineq1  42923  3lexlogpow5ineq5  42929  aks4d1p1  42945  sq8  43175  ex-decpmul  43184  resqrtvalex  44488  imsqrtvalex  44489  sin5tlem4  47743  sin5tlem5  47744  fmtno5lem4  48462  257prm  48467  fmtnoprmfac2lem1  48472  fmtno4prmfac  48478  fmtno4nprmfac193  48480  fmtno5faclem3  48487  m3prm  48498  139prmALT  48502  127prm  48505  m7prm  48506  5tcu2e40  48521  2exp340mod341  48652  8exp8mod9  48655  nfermltl8rev  48661  evengpop3  48717  tgoldbachlt  48735