Theorem 8cn 12225

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 12197	. 2 ⊢ 8 = (7 + 1)
2		7cn 12222	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11067	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11121	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007  1c1 11010   + caddc 11012  7c7 12188  8c8 12189

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 11067  ax-addcl 11069

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12191  df-3 12192  df-4 12193  df-5 12194  df-6 12195  df-7 12196  df-8 12197

This theorem is referenced by:  9cn  12228  9m1e8  12257  8p2e10  12671  8t2e16  12706  8t5e40  12709  cos2bnd  16097  2exp11  17001  2exp16  17002  139prm  17035  163prm  17036  317prm  17037  631prm  17038  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001prm  17056  quart1cl  26762  quart1lem  26763  quart1  26764  quartlem1  26765  log2tlbnd  26853  log2ublem3  26856  log2ub  26857  bposlem8  27200  lgsdir2lem1  27234  lgsdir2lem5  27238  2lgslem3a  27305  2lgslem3b  27306  2lgslem3c  27307  2lgslem3d  27308  2lgslem3a1  27309  2lgslem3b1  27310  2lgslem3c1  27311  2lgslem3d1  27312  2lgsoddprmlem1  27317  2lgsoddprmlem2  27318  2lgsoddprmlem3a  27319  2lgsoddprmlem3b  27320  2lgsoddprmlem3c  27321  2lgsoddprmlem3d  27322  ex-exp  30394  hgt750lem2  34620  420lcm8e840  41988  3exp7  42030  3lexlogpow5ineq1  42031  3lexlogpow5ineq5  42037  aks4d1p1  42053  sq8  42274  ex-decpmul  42283  resqrtvalex  43622  imsqrtvalex  43623  fmtno5lem4  47544  257prm  47549  fmtnoprmfac2lem1  47554  fmtno4prmfac  47560  fmtno4nprmfac193  47562  fmtno5faclem3  47569  m3prm  47580  139prmALT  47584  127prm  47587  m7prm  47588  5tcu2e40  47603  2exp340mod341  47721  8exp8mod9  47724  nfermltl8rev  47730  evengpop3  47786  tgoldbachlt  47804