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 11216	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11270	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2822	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2099  (class class class)co 7424  ℂcc 11156  1c1 11159   + caddc 11161  8c8 12325  9c9 12326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-1cn 11216  ax-addcl 11218

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-clel 2803  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  12825  9t2e18  12851  9t8e72  12857  9t9e81  12858  9t11e99  12859  0.999...  15885  cos2bnd  16190  3dvds  16333  3dvdsdec  16334  3dvds2dec  16335  2exp8  17091  139prm  17126  163prm  17127  317prm  17128  631prm  17129  1259lem1  17133  1259lem2  17134  1259lem3  17135  1259lem4  17136  1259lem5  17137  2503lem1  17139  2503lem2  17140  2503lem3  17141  2503prm  17142  4001lem1  17143  4001lem2  17144  4001lem3  17145  4001lem4  17146  sqrt2cxp2logb9e3  26827  mcubic  26875  cubic2  26876  cubic  26877  quartlem1  26885  log2tlbnd  26973  log2ublem3  26976  log2ub  26977  bposlem8  27320  ex-lcm  30391  9p10ne21  30403  1mhdrd  32777  hgt750lem2  34498  60gcd7e1  41704  3lexlogpow5ineq1  41753  3lexlogpow2ineq2  41758  3lexlogpow5ineq5  41759  sq9  42105  sum9cubes  42326  fmtno5lem4  47128  257prm  47133  fmtno4nprmfac193  47146  139prmALT  47168  127prm  47171  8exp8mod9  47308  nfermltl8rev  47314  evengpop3  47370