Theorem 8cn 12338

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 12309	. 2 ⊢ 8 = (7 + 1)
2		7cn 12335	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11158	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11215	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2865	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2149  (class class class)co 7411  ℂcc 11098  1c1 11101   + caddc 11103  7c7 12300  8c8 12301

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11158  ax-addcl 11160

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844  df-2 12303  df-3 12304  df-4 12305  df-5 12306  df-6 12307  df-7 12308  df-8 12309

This theorem is referenced by:  9cn  12341  9m1e8  12374  8p2e10  12796  8t2e16  12831  8t5e40  12834  cos2bnd  16244  2exp11  17149  2exp16  17150  139prm  17184  163prm  17185  317prm  17186  631prm  17187  1259lem2  17192  1259lem3  17193  1259lem4  17194  1259lem5  17195  2503lem2  17198  2503lem3  17199  2503prm  17200  4001lem1  17201  4001lem2  17202  4001prm  17205  quart1cl  26985  quart1lem  26986  quart1  26987  quartlem1  26988  log2tlbnd  27076  log2ublem3  27079  log2ub  27080  bposlem8  27421  lgsdir2lem1  27455  lgsdir2lem5  27459  2lgslem3a  27526  2lgslem3b  27527  2lgslem3c  27528  2lgslem3d  27529  2lgslem3a1  27530  2lgslem3b1  27531  2lgslem3c1  27532  2lgslem3d1  27533  2lgsoddprmlem1  27538  2lgsoddprmlem2  27539  2lgsoddprmlem3a  27540  2lgsoddprmlem3b  27541  2lgsoddprmlem3c  27542  2lgsoddprmlem3d  27543  ex-exp  30742  hgt750lem2  34984  420lcm8e840  42668  3exp7  42710  3lexlogpow5ineq1  42711  3lexlogpow5ineq5  42717  aks4d1p1  42733  sq8  42948  ex-decpmul  42957  resqrtvalex  44263  imsqrtvalex  44264  sin5tlem4  47502  sin5tlem5  47503  fmtno5lem4  48197  257prm  48202  fmtnoprmfac2lem1  48207  fmtno4prmfac  48213  fmtno4nprmfac193  48215  fmtno5faclem3  48222  m3prm  48233  139prmALT  48237  127prm  48240  m7prm  48241  5tcu2e40  48256  2exp340mod341  48387  8exp8mod9  48390  nfermltl8rev  48396  evengpop3  48452  tgoldbachlt  48470