Theorem 8cn 12259

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 12231	. 2 ⊢ 8 = (7 + 1)
2		7cn 12256	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11102	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11156	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042  1c1 11045   + caddc 11047  7c7 12222  8c8 12223

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11102  ax-addcl 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230  df-8 12231

This theorem is referenced by:  9cn  12262  9m1e8  12291  8p2e10  12705  8t2e16  12740  8t5e40  12743  cos2bnd  16132  2exp11  17036  2exp16  17037  139prm  17070  163prm  17071  317prm  17072  631prm  17073  1259lem2  17078  1259lem3  17079  1259lem4  17080  1259lem5  17081  2503lem2  17084  2503lem3  17085  2503prm  17086  4001lem1  17087  4001lem2  17088  4001prm  17091  quart1cl  26797  quart1lem  26798  quart1  26799  quartlem1  26800  log2tlbnd  26888  log2ublem3  26891  log2ub  26892  bposlem8  27235  lgsdir2lem1  27269  lgsdir2lem5  27273  2lgslem3a  27340  2lgslem3b  27341  2lgslem3c  27342  2lgslem3d  27343  2lgslem3a1  27344  2lgslem3b1  27345  2lgslem3c1  27346  2lgslem3d1  27347  2lgsoddprmlem1  27352  2lgsoddprmlem2  27353  2lgsoddprmlem3a  27354  2lgsoddprmlem3b  27355  2lgsoddprmlem3c  27356  2lgsoddprmlem3d  27357  ex-exp  30429  hgt750lem2  34636  420lcm8e840  41992  3exp7  42034  3lexlogpow5ineq1  42035  3lexlogpow5ineq5  42041  aks4d1p1  42057  sq8  42278  ex-decpmul  42287  resqrtvalex  43627  imsqrtvalex  43628  fmtno5lem4  47550  257prm  47555  fmtnoprmfac2lem1  47560  fmtno4prmfac  47566  fmtno4nprmfac193  47568  fmtno5faclem3  47575  m3prm  47586  139prmALT  47590  127prm  47593  m7prm  47594  5tcu2e40  47609  2exp340mod341  47727  8exp8mod9  47730  nfermltl8rev  47736  evengpop3  47792  tgoldbachlt  47810