Theorem 9cn 12364

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 12334	. 2 ⊢ 9 = (8 + 1)
2		8cn 12361	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11211	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11265	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2835	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2106  (class class class)co 7431  ℂcc 11151  1c1 11154   + caddc 11156  8c8 12325  9c9 12326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-1cn 11211  ax-addcl 11213

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-clel 2814  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334

This theorem is referenced by:  10m1e9  12827  9t2e18  12853  9t8e72  12859  9t9e81  12860  9t11e99  12861  0.999...  15914  cos2bnd  16221  3dvds  16365  3dvdsdec  16366  3dvds2dec  16367  2exp8  17123  139prm  17158  163prm  17159  317prm  17160  631prm  17161  1259lem1  17165  1259lem2  17166  1259lem3  17167  1259lem4  17168  1259lem5  17169  2503lem1  17171  2503lem2  17172  2503lem3  17173  2503prm  17174  4001lem1  17175  4001lem2  17176  4001lem3  17177  4001lem4  17178  sqrt2cxp2logb9e3  26857  mcubic  26905  cubic2  26906  cubic  26907  quartlem1  26915  log2tlbnd  27003  log2ublem3  27006  log2ub  27007  bposlem8  27350  ex-lcm  30487  9p10ne21  30499  1mhdrd  32883  hgt750lem2  34646  60gcd7e1  41987  3lexlogpow5ineq1  42036  3lexlogpow2ineq2  42041  3lexlogpow5ineq5  42042  sq9  42311  sum9cubes  42659  fmtno5lem4  47481  257prm  47486  fmtno4nprmfac193  47499  139prmALT  47521  127prm  47524  8exp8mod9  47661  nfermltl8rev  47667  evengpop3  47723