Theorem 8cn 12305

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 12277	. 2 ⊢ 8 = (7 + 1)
2		7cn 12302	. . 3 ⊢ 7 ∈ ℂ
3		ax-1cn 11164	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11216	. 2 ⊢ (7 + 1) ∈ ℂ
5	1, 4	eqeltri 2829	1 ⊢ 8 ∈ ℂ

Syntax hints:   ∈ wcel 2106  (class class class)co 7405  ℂcc 11104  1c1 11107   + caddc 11109  7c7 12268  8c8 12269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-1cn 11164  ax-addcl 11166

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277

This theorem is referenced by:  9cn  12308  9m1e8  12342  8p2e10  12753  8t2e16  12788  8t5e40  12791  cos2bnd  16127  2exp11  17019  2exp16  17020  139prm  17053  163prm  17054  317prm  17055  631prm  17056  1259lem2  17061  1259lem3  17062  1259lem4  17063  1259lem5  17064  2503lem2  17067  2503lem3  17068  2503prm  17069  4001lem1  17070  4001lem2  17071  4001prm  17074  quart1cl  26348  quart1lem  26349  quart1  26350  quartlem1  26351  log2tlbnd  26439  log2ublem3  26442  log2ub  26443  bposlem8  26783  lgsdir2lem1  26817  lgsdir2lem5  26821  2lgslem3a  26888  2lgslem3b  26889  2lgslem3c  26890  2lgslem3d  26891  2lgslem3a1  26892  2lgslem3b1  26893  2lgslem3c1  26894  2lgslem3d1  26895  2lgsoddprmlem1  26900  2lgsoddprmlem2  26901  2lgsoddprmlem3a  26902  2lgsoddprmlem3b  26903  2lgsoddprmlem3c  26904  2lgsoddprmlem3d  26905  ex-exp  29692  hgt750lem2  33652  420lcm8e840  40864  3exp7  40906  3lexlogpow5ineq1  40907  3lexlogpow5ineq5  40913  aks4d1p1  40929  ex-decpmul  41201  resqrtvalex  42381  imsqrtvalex  42382  fmtno5lem4  46210  257prm  46215  fmtnoprmfac2lem1  46220  fmtno4prmfac  46226  fmtno4nprmfac193  46228  fmtno5faclem3  46235  m3prm  46246  139prmALT  46250  127prm  46253  m7prm  46254  5tcu2e40  46269  2exp340mod341  46387  8exp8mod9  46390  nfermltl8rev  46396  evengpop3  46452  tgoldbachlt  46470