Theorem 8cn 12272

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 12244	. 2 ⊢ 8 = (7 + 1)
2		7cn 12269	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11090	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11145	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2833	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7361  ℂcc 11030  1c1 11033   + caddc 11035  7c7 12235  8c8 12236

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11090  ax-addcl 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-2 12238  df-3 12239  df-4 12240  df-5 12241  df-6 12242  df-7 12243  df-8 12244

This theorem is referenced by:  9cn  12275  9m1e8  12304  8p2e10  12718  8t2e16  12753  8t5e40  12756  cos2bnd  16149  2exp11  17054  2exp16  17055  139prm  17088  163prm  17089  317prm  17090  631prm  17091  1259lem2  17096  1259lem3  17097  1259lem4  17098  1259lem5  17099  2503lem2  17102  2503lem3  17103  2503prm  17104  4001lem1  17105  4001lem2  17106  4001prm  17109  quart1cl  26834  quart1lem  26835  quart1  26836  quartlem1  26837  log2tlbnd  26925  log2ublem3  26928  log2ub  26929  bposlem8  27271  lgsdir2lem1  27305  lgsdir2lem5  27309  2lgslem3a  27376  2lgslem3b  27377  2lgslem3c  27378  2lgslem3d  27379  2lgslem3a1  27380  2lgslem3b1  27381  2lgslem3c1  27382  2lgslem3d1  27383  2lgsoddprmlem1  27388  2lgsoddprmlem2  27389  2lgsoddprmlem3a  27390  2lgsoddprmlem3b  27391  2lgsoddprmlem3c  27392  2lgsoddprmlem3d  27393  ex-exp  30538  hgt750lem2  34815  420lcm8e840  42467  3exp7  42509  3lexlogpow5ineq1  42510  3lexlogpow5ineq5  42516  aks4d1p1  42532  sq8  42746  ex-decpmul  42755  resqrtvalex  44093  imsqrtvalex  44094  sin5tlem4  47343  sin5tlem5  47344  fmtno5lem4  48034  257prm  48039  fmtnoprmfac2lem1  48044  fmtno4prmfac  48050  fmtno4nprmfac193  48052  fmtno5faclem3  48059  m3prm  48070  139prmALT  48074  127prm  48077  m7prm  48078  5tcu2e40  48093  2exp340mod341  48224  8exp8mod9  48227  nfermltl8rev  48233  evengpop3  48289  tgoldbachlt  48307