Theorem 8cn 12242

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 12214	. 2 ⊢ 8 = (7 + 1)
2		7cn 12239	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11084	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11138	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2832	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024  1c1 11027   + caddc 11029  7c7 12205  8c8 12206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-addcl 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811  df-2 12208  df-3 12209  df-4 12210  df-5 12211  df-6 12212  df-7 12213  df-8 12214

This theorem is referenced by:  9cn  12245  9m1e8  12274  8p2e10  12687  8t2e16  12722  8t5e40  12725  cos2bnd  16113  2exp11  17017  2exp16  17018  139prm  17051  163prm  17052  317prm  17053  631prm  17054  1259lem2  17059  1259lem3  17060  1259lem4  17061  1259lem5  17062  2503lem2  17065  2503lem3  17066  2503prm  17067  4001lem1  17068  4001lem2  17069  4001prm  17072  quart1cl  26820  quart1lem  26821  quart1  26822  quartlem1  26823  log2tlbnd  26911  log2ublem3  26914  log2ub  26915  bposlem8  27258  lgsdir2lem1  27292  lgsdir2lem5  27296  2lgslem3a  27363  2lgslem3b  27364  2lgslem3c  27365  2lgslem3d  27366  2lgslem3a1  27367  2lgslem3b1  27368  2lgslem3c1  27369  2lgslem3d1  27370  2lgsoddprmlem1  27375  2lgsoddprmlem2  27376  2lgsoddprmlem3a  27377  2lgsoddprmlem3b  27378  2lgsoddprmlem3c  27379  2lgsoddprmlem3d  27380  ex-exp  30525  hgt750lem2  34809  420lcm8e840  42275  3exp7  42317  3lexlogpow5ineq1  42318  3lexlogpow5ineq5  42324  aks4d1p1  42340  sq8  42562  ex-decpmul  42571  resqrtvalex  43896  imsqrtvalex  43897  fmtno5lem4  47812  257prm  47817  fmtnoprmfac2lem1  47822  fmtno4prmfac  47828  fmtno4nprmfac193  47830  fmtno5faclem3  47837  m3prm  47848  139prmALT  47852  127prm  47855  m7prm  47856  5tcu2e40  47871  2exp340mod341  47989  8exp8mod9  47992  nfermltl8rev  47998  evengpop3  48054  tgoldbachlt  48072