Theorem 8cn 12315

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 12286	. 2 ⊢ 8 = (7 + 1)
2		7cn 12312	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11131	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11188	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2858	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2142  (class class class)co 7396  ℂcc 11071  1c1 11074   + caddc 11076  7c7 12277  8c8 12278

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11131  ax-addcl 11133

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-clel 2837  df-2 12280  df-3 12281  df-4 12282  df-5 12283  df-6 12284  df-7 12285  df-8 12286

This theorem is referenced by:  9cn  12318  9m1e8  12351  8p2e10  12773  8t2e16  12808  8t5e40  12811  cos2bnd  16220  2exp11  17125  2exp16  17126  139prm  17160  163prm  17161  317prm  17162  631prm  17163  1259lem2  17168  1259lem3  17169  1259lem4  17170  1259lem5  17171  2503lem2  17174  2503lem3  17175  2503prm  17176  4001lem1  17177  4001lem2  17178  4001prm  17181  quart1cl  26919  quart1lem  26920  quart1  26921  quartlem1  26922  log2tlbnd  27010  log2ublem3  27013  log2ub  27014  bposlem8  27355  lgsdir2lem1  27389  lgsdir2lem5  27393  2lgslem3a  27460  2lgslem3b  27461  2lgslem3c  27462  2lgslem3d  27463  2lgslem3a1  27464  2lgslem3b1  27465  2lgslem3c1  27466  2lgslem3d1  27467  2lgsoddprmlem1  27472  2lgsoddprmlem2  27473  2lgsoddprmlem3a  27474  2lgsoddprmlem3b  27475  2lgsoddprmlem3c  27476  2lgsoddprmlem3d  27477  ex-exp  30652  hgt750lem2  34946  420lcm8e840  42628  3exp7  42670  3lexlogpow5ineq1  42671  3lexlogpow5ineq5  42677  aks4d1p1  42693  sq8  42906  ex-decpmul  42915  resqrtvalex  44221  imsqrtvalex  44222  sin5tlem4  47470  sin5tlem5  47471  fmtno5lem4  48165  257prm  48170  fmtnoprmfac2lem1  48175  fmtno4prmfac  48181  fmtno4nprmfac193  48183  fmtno5faclem3  48190  m3prm  48201  139prmALT  48205  127prm  48208  m7prm  48209  5tcu2e40  48224  2exp340mod341  48355  8exp8mod9  48358  nfermltl8rev  48364  evengpop3  48420  tgoldbachlt  48438