Theorem 9cn 12293

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 12263	. 2 ⊢ 9 = (8 + 1)
2		8cn 12290	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11133	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11187	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2825	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073  1c1 11076   + caddc 11078  8c8 12254  9c9 12255

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 2702  ax-1cn 11133  ax-addcl 11135

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804  df-2 12256  df-3 12257  df-4 12258  df-5 12259  df-6 12260  df-7 12261  df-8 12262  df-9 12263

This theorem is referenced by:  10m1e9  12752  9t2e18  12778  9t8e72  12784  9t9e81  12785  9t11e99  12786  0.999...  15854  cos2bnd  16163  3dvds  16308  3dvdsdec  16309  3dvds2dec  16310  2exp8  17066  139prm  17101  163prm  17102  317prm  17103  631prm  17104  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  2503lem1  17114  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  sqrt2cxp2logb9e3  26716  mcubic  26764  cubic2  26765  cubic  26766  quartlem1  26774  log2tlbnd  26862  log2ublem3  26865  log2ub  26866  bposlem8  27209  ex-lcm  30394  9p10ne21  30406  1mhdrd  32843  hgt750lem2  34650  60gcd7e1  42000  3lexlogpow5ineq1  42049  3lexlogpow2ineq2  42054  3lexlogpow5ineq5  42055  sq9  42293  sum9cubes  42667  fmtno5lem4  47561  257prm  47566  fmtno4nprmfac193  47579  139prmALT  47601  127prm  47604  8exp8mod9  47741  nfermltl8rev  47747  evengpop3  47803