Theorem 8cn 12240

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 12212	. 2 ⊢ 8 = (7 + 1)
2		7cn 12237	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11082	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11136	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2830	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2113  (class class class)co 7356  ℂcc 11022  1c1 11025   + caddc 11027  7c7 12203  8c8 12204

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 2706  ax-1cn 11082  ax-addcl 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-clel 2809  df-2 12206  df-3 12207  df-4 12208  df-5 12209  df-6 12210  df-7 12211  df-8 12212

This theorem is referenced by:  9cn  12243  9m1e8  12272  8p2e10  12685  8t2e16  12720  8t5e40  12723  cos2bnd  16111  2exp11  17015  2exp16  17016  139prm  17049  163prm  17050  317prm  17051  631prm  17052  1259lem2  17057  1259lem3  17058  1259lem4  17059  1259lem5  17060  2503lem2  17063  2503lem3  17064  2503prm  17065  4001lem1  17066  4001lem2  17067  4001prm  17070  quart1cl  26818  quart1lem  26819  quart1  26820  quartlem1  26821  log2tlbnd  26909  log2ublem3  26912  log2ub  26913  bposlem8  27256  lgsdir2lem1  27290  lgsdir2lem5  27294  2lgslem3a  27361  2lgslem3b  27362  2lgslem3c  27363  2lgslem3d  27364  2lgslem3a1  27365  2lgslem3b1  27366  2lgslem3c1  27367  2lgslem3d1  27368  2lgsoddprmlem1  27373  2lgsoddprmlem2  27374  2lgsoddprmlem3a  27375  2lgsoddprmlem3b  27376  2lgsoddprmlem3c  27377  2lgsoddprmlem3d  27378  ex-exp  30474  hgt750lem2  34758  420lcm8e840  42204  3exp7  42246  3lexlogpow5ineq1  42247  3lexlogpow5ineq5  42253  aks4d1p1  42269  sq8  42494  ex-decpmul  42503  resqrtvalex  43828  imsqrtvalex  43829  fmtno5lem4  47744  257prm  47749  fmtnoprmfac2lem1  47754  fmtno4prmfac  47760  fmtno4nprmfac193  47762  fmtno5faclem3  47769  m3prm  47780  139prmALT  47784  127prm  47787  m7prm  47788  5tcu2e40  47803  2exp340mod341  47921  8exp8mod9  47924  nfermltl8rev  47930  evengpop3  47986  tgoldbachlt  48004