Theorem 9cn 12281

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 12251	. 2 ⊢ 9 = (8 + 1)
2		8cn 12278	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11151	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2832	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036  1c1 11039   + caddc 11041  8c8 12242  9c9 12243

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249  df-8 12250  df-9 12251

This theorem is referenced by:  10m1e9  12740  9t2e18  12766  9t8e72  12772  9t9e81  12773  9t11e99  12774  0.999...  15846  cos2bnd  16155  3dvds  16300  3dvdsdec  16301  3dvds2dec  16302  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  26763  mcubic  26811  cubic2  26812  cubic  26813  quartlem1  26821  log2tlbnd  26909  log2ublem3  26912  log2ub  26913  bposlem8  27254  ex-lcm  30528  9p10ne21  30540  1mhdrd  32975  hgt750lem2  34796  60gcd7e1  42444  3lexlogpow5ineq1  42493  3lexlogpow2ineq2  42498  3lexlogpow5ineq5  42499  sq9  42730  sum9cubes  43105  fmtno5lem4  48019  257prm  48024  fmtno4nprmfac193  48037  139prmALT  48059  127prm  48062  8exp8mod9  48212  nfermltl8rev  48218  evengpop3  48274