Theorem 9cn 12243

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 12213	. 2 ⊢ 9 = (8 + 1)
2		8cn 12240	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11082	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11136	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2830	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2113  (class class class)co 7356  ℂcc 11022  1c1 11025   + caddc 11027  8c8 12204  9c9 12205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-1cn 11082  ax-addcl 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-clel 2809  df-2 12206  df-3 12207  df-4 12208  df-5 12209  df-6 12210  df-7 12211  df-8 12212  df-9 12213

This theorem is referenced by:  10m1e9  12701  9t2e18  12727  9t8e72  12733  9t9e81  12734  9t11e99  12735  0.999...  15802  cos2bnd  16111  3dvds  16256  3dvdsdec  16257  3dvds2dec  16258  2exp8  17014  139prm  17049  163prm  17050  317prm  17051  631prm  17052  1259lem1  17056  1259lem2  17057  1259lem3  17058  1259lem4  17059  1259lem5  17060  2503lem1  17062  2503lem2  17063  2503lem3  17064  2503prm  17065  4001lem1  17066  4001lem2  17067  4001lem3  17068  4001lem4  17069  sqrt2cxp2logb9e3  26763  mcubic  26811  cubic2  26812  cubic  26813  quartlem1  26821  log2tlbnd  26909  log2ublem3  26912  log2ub  26913  bposlem8  27256  ex-lcm  30482  9p10ne21  30494  1mhdrd  32946  hgt750lem2  34758  60gcd7e1  42198  3lexlogpow5ineq1  42247  3lexlogpow2ineq2  42252  3lexlogpow5ineq5  42253  sq9  42495  sum9cubes  42857  fmtno5lem4  47744  257prm  47749  fmtno4nprmfac193  47762  139prmALT  47784  127prm  47787  8exp8mod9  47924  nfermltl8rev  47930  evengpop3  47986