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  34626  420lcm8e840  41994  3exp7  42036  3lexlogpow5ineq1  42037  3lexlogpow5ineq5  42043  aks4d1p1  42059  sq8  42280  ex-decpmul  42289  resqrtvalex  43628  imsqrtvalex  43629  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