Theorem 9cn 12308

Description: The number 9 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
9cn	⊢ 9 ∈ ℂ

Proof of Theorem 9cn

Step	Hyp	Ref	Expression
1		df-9 12278	. 2 ⊢ 9 = (8 + 1)
2		8cn 12305	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11164	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11216	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2829	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2106  (class class class)co 7405  ℂcc 11104  1c1 11107   + caddc 11109  8c8 12269  9c9 12270

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  df-9 12278

This theorem is referenced by:  10m1e9  12769  9t2e18  12795  9t8e72  12801  9t9e81  12802  9t11e99  12803  0.999...  15823  cos2bnd  16127  3dvds  16270  3dvdsdec  16271  3dvds2dec  16272  2exp8  17018  139prm  17053  163prm  17054  317prm  17055  631prm  17056  1259lem1  17060  1259lem2  17061  1259lem3  17062  1259lem4  17063  1259lem5  17064  2503lem1  17066  2503lem2  17067  2503lem3  17068  2503prm  17069  4001lem1  17070  4001lem2  17071  4001lem3  17072  4001lem4  17073  sqrt2cxp2logb9e3  26293  mcubic  26341  cubic2  26342  cubic  26343  quartlem1  26351  log2tlbnd  26439  log2ublem3  26442  log2ub  26443  bposlem8  26783  ex-lcm  29700  9p10ne21  29712  1mhdrd  32069  hgt750lem2  33652  60gcd7e1  40858  3lexlogpow5ineq1  40907  3lexlogpow2ineq2  40912  3lexlogpow5ineq5  40913  fmtno5lem4  46210  257prm  46215  fmtno4nprmfac193  46228  139prmALT  46250  127prm  46253  8exp8mod9  46390  nfermltl8rev  46396  evengpop3  46452