Theorem 8cn 12333

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 12304	. 2 ⊢ 8 = (7 + 1)
2		7cn 12330	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11153	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11210	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2859	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093  1c1 11096   + caddc 11098  7c7 12295  8c8 12296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-addcl 11155

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838  df-2 12298  df-3 12299  df-4 12300  df-5 12301  df-6 12302  df-7 12303  df-8 12304

This theorem is referenced by:  9cn  12336  9m1e8  12369  8th4div3  12459  8p2e10  12791  8t2e16  12826  8t5e40  12829  cos2bnd  16239  2exp11  17144  2exp16  17145  139prm  17179  163prm  17180  317prm  17181  631prm  17182  1259lem2  17187  1259lem3  17188  1259lem4  17189  1259lem5  17190  2503lem2  17193  2503lem3  17194  2503prm  17195  4001lem1  17196  4001lem2  17197  4001prm  17200  quart1cl  27019  quart1lem  27020  quart1  27021  quartlem1  27022  log2tlbnd  27110  log2ublem3  27113  log2ub  27114  bposlem8  27455  lgsdir2lem1  27489  lgsdir2lem5  27493  2lgslem3a  27560  2lgslem3b  27561  2lgslem3c  27562  2lgslem3d  27563  2lgslem3a1  27564  2lgslem3b1  27565  2lgslem3c1  27566  2lgslem3d1  27567  2lgsoddprmlem1  27572  2lgsoddprmlem2  27573  2lgsoddprmlem3a  27574  2lgsoddprmlem3b  27575  2lgsoddprmlem3c  27576  2lgsoddprmlem3d  27577  ex-exp  30801  hgt750lem2  35039  420lcm8e840  42798  3exp7  42840  3lexlogpow5ineq1  42841  3lexlogpow5ineq5  42847  aks4d1p1  42863  sq8  43078  ex-decpmul  43087  resqrtvalex  44391  imsqrtvalex  44392  sin5tlem4  47633  sin5tlem5  47634  fmtno5lem4  48328  257prm  48333  fmtnoprmfac2lem1  48338  fmtno4prmfac  48344  fmtno4nprmfac193  48346  fmtno5faclem3  48353  m3prm  48364  139prmALT  48368  127prm  48371  m7prm  48372  5tcu2e40  48387  2exp340mod341  48518  8exp8mod9  48521  nfermltl8rev  48527  evengpop3  48583  tgoldbachlt  48601