Theorem 9cn 12393

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 12363	. 2 ⊢ 9 = (8 + 1)
2		8cn 12390	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11242	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11296	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2840	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182  1c1 11185   + caddc 11187  8c8 12354  9c9 12355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-addcl 11244

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361  df-8 12362  df-9 12363

This theorem is referenced by:  10m1e9  12854  9t2e18  12880  9t8e72  12886  9t9e81  12887  9t11e99  12888  0.999...  15929  cos2bnd  16236  3dvds  16379  3dvdsdec  16380  3dvds2dec  16381  2exp8  17136  139prm  17171  163prm  17172  317prm  17173  631prm  17174  1259lem1  17178  1259lem2  17179  1259lem3  17180  1259lem4  17181  1259lem5  17182  2503lem1  17184  2503lem2  17185  2503lem3  17186  2503prm  17187  4001lem1  17188  4001lem2  17189  4001lem3  17190  4001lem4  17191  sqrt2cxp2logb9e3  26860  mcubic  26908  cubic2  26909  cubic  26910  quartlem1  26918  log2tlbnd  27006  log2ublem3  27009  log2ub  27010  bposlem8  27353  ex-lcm  30490  9p10ne21  30502  1mhdrd  32880  hgt750lem2  34629  60gcd7e1  41962  3lexlogpow5ineq1  42011  3lexlogpow2ineq2  42016  3lexlogpow5ineq5  42017  sq9  42286  sum9cubes  42627  fmtno5lem4  47430  257prm  47435  fmtno4nprmfac193  47448  139prmALT  47470  127prm  47473  8exp8mod9  47610  nfermltl8rev  47616  evengpop3  47672