Theorem 9cn 12286

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066  1c1 11069   + caddc 11071  8c8 12247  9c9 12248

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 11126  ax-addcl 11128

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12249  df-3 12250  df-4 12251  df-5 12252  df-6 12253  df-7 12254  df-8 12255  df-9 12256

This theorem is referenced by:  10m1e9  12745  9t2e18  12771  9t8e72  12777  9t9e81  12778  9t11e99  12779  0.999...  15847  cos2bnd  16156  3dvds  16301  3dvdsdec  16302  3dvds2dec  16303  2exp8  17059  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  sqrt2cxp2logb9e3  26709  mcubic  26757  cubic2  26758  cubic  26759  quartlem1  26767  log2tlbnd  26855  log2ublem3  26858  log2ub  26859  bposlem8  27202  ex-lcm  30387  9p10ne21  30399  1mhdrd  32836  hgt750lem2  34643  60gcd7e1  41993  3lexlogpow5ineq1  42042  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  sq9  42286  sum9cubes  42660  fmtno5lem4  47557  257prm  47562  fmtno4nprmfac193  47575  139prmALT  47597  127prm  47600  8exp8mod9  47737  nfermltl8rev  47743  evengpop3  47799