Theorem 9cn 12245

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 12215	. 2 ⊢ 9 = (8 + 1)
2		8cn 12242	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11084	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11138	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2832	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024  1c1 11027   + caddc 11029  8c8 12206  9c9 12207

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 2708  ax-1cn 11084  ax-addcl 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811  df-2 12208  df-3 12209  df-4 12210  df-5 12211  df-6 12212  df-7 12213  df-8 12214  df-9 12215

This theorem is referenced by:  10m1e9  12703  9t2e18  12729  9t8e72  12735  9t9e81  12736  9t11e99  12737  0.999...  15804  cos2bnd  16113  3dvds  16258  3dvdsdec  16259  3dvds2dec  16260  2exp8  17016  139prm  17051  163prm  17052  317prm  17053  631prm  17054  1259lem1  17058  1259lem2  17059  1259lem3  17060  1259lem4  17061  1259lem5  17062  2503lem1  17064  2503lem2  17065  2503lem3  17066  2503prm  17067  4001lem1  17068  4001lem2  17069  4001lem3  17070  4001lem4  17071  sqrt2cxp2logb9e3  26765  mcubic  26813  cubic2  26814  cubic  26815  quartlem1  26823  log2tlbnd  26911  log2ublem3  26914  log2ub  26915  bposlem8  27258  ex-lcm  30533  9p10ne21  30545  1mhdrd  32997  hgt750lem2  34809  60gcd7e1  42269  3lexlogpow5ineq1  42318  3lexlogpow2ineq2  42323  3lexlogpow5ineq5  42324  sq9  42563  sum9cubes  42925  fmtno5lem4  47812  257prm  47817  fmtno4nprmfac193  47830  139prmALT  47852  127prm  47855  8exp8mod9  47992  nfermltl8rev  47998  evengpop3  48054