Theorem 9cn 12312

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 12282	. 2 ⊢ 9 = (8 + 1)
2		8cn 12309	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11168	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11220	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2830	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108  1c1 11111   + caddc 11113  8c8 12273  9c9 12274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11168  ax-addcl 11170

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282

This theorem is referenced by:  10m1e9  12773  9t2e18  12799  9t8e72  12805  9t9e81  12806  9t11e99  12807  0.999...  15827  cos2bnd  16131  3dvds  16274  3dvdsdec  16275  3dvds2dec  16276  2exp8  17022  139prm  17057  163prm  17058  317prm  17059  631prm  17060  1259lem1  17064  1259lem2  17065  1259lem3  17066  1259lem4  17067  1259lem5  17068  2503lem1  17070  2503lem2  17071  2503lem3  17072  2503prm  17073  4001lem1  17074  4001lem2  17075  4001lem3  17076  4001lem4  17077  sqrt2cxp2logb9e3  26304  mcubic  26352  cubic2  26353  cubic  26354  quartlem1  26362  log2tlbnd  26450  log2ublem3  26453  log2ub  26454  bposlem8  26794  ex-lcm  29711  9p10ne21  29723  1mhdrd  32082  hgt750lem2  33664  60gcd7e1  40870  3lexlogpow5ineq1  40919  3lexlogpow2ineq2  40924  3lexlogpow5ineq5  40925  sq9  41204  sum9cubes  41414  fmtno5lem4  46224  257prm  46229  fmtno4nprmfac193  46242  139prmALT  46264  127prm  46267  8exp8mod9  46404  nfermltl8rev  46410  evengpop3  46466