Theorem 8cn 12269

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 12241	. 2 ⊢ 8 = (7 + 1)
2		7cn 12266	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11087	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11142	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2835	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2119  (class class class)co 7356  ℂcc 11027  1c1 11030   + caddc 11032  7c7 12232  8c8 12233

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087  ax-addcl 11089

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-7 12240  df-8 12241

This theorem is referenced by:  9cn  12272  9m1e8  12301  8p2e10  12715  8t2e16  12750  8t5e40  12753  cos2bnd  16146  2exp11  17051  2exp16  17052  139prm  17085  163prm  17086  317prm  17087  631prm  17088  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  2503lem2  17099  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem2  17103  4001prm  17106  quart1cl  26836  quart1lem  26837  quart1  26838  quartlem1  26839  log2tlbnd  26927  log2ublem3  26930  log2ub  26931  bposlem8  27272  lgsdir2lem1  27306  lgsdir2lem5  27310  2lgslem3a  27377  2lgslem3b  27378  2lgslem3c  27379  2lgslem3d  27380  2lgslem3a1  27381  2lgslem3b1  27382  2lgslem3c1  27383  2lgslem3d1  27384  2lgsoddprmlem1  27389  2lgsoddprmlem2  27390  2lgsoddprmlem3a  27391  2lgsoddprmlem3b  27392  2lgsoddprmlem3c  27393  2lgsoddprmlem3d  27394  ex-exp  30538  hgt750lem2  34836  420lcm8e840  42496  3exp7  42538  3lexlogpow5ineq1  42539  3lexlogpow5ineq5  42545  aks4d1p1  42561  sq8  42774  ex-decpmul  42783  resqrtvalex  44089  imsqrtvalex  44090  sin5tlem4  47339  sin5tlem5  47340  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