Theorem 9cn 12216

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 12186	. 2 ⊢ 9 = (8 + 1)
2		8cn 12213	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11055	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11109	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7340  ℂcc 10995  1c1 10998   + caddc 11000  8c8 12177  9c9 12178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11055  ax-addcl 11057

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12179  df-3 12180  df-4 12181  df-5 12182  df-6 12183  df-7 12184  df-8 12185  df-9 12186

This theorem is referenced by:  10m1e9  12675  9t2e18  12701  9t8e72  12707  9t9e81  12708  9t11e99  12709  0.999...  15775  cos2bnd  16084  3dvds  16229  3dvdsdec  16230  3dvds2dec  16231  2exp8  16987  139prm  17022  163prm  17023  317prm  17024  631prm  17025  1259lem1  17029  1259lem2  17030  1259lem3  17031  1259lem4  17032  1259lem5  17033  2503lem1  17035  2503lem2  17036  2503lem3  17037  2503prm  17038  4001lem1  17039  4001lem2  17040  4001lem3  17041  4001lem4  17042  sqrt2cxp2logb9e3  26690  mcubic  26738  cubic2  26739  cubic  26740  quartlem1  26748  log2tlbnd  26836  log2ublem3  26839  log2ub  26840  bposlem8  27183  ex-lcm  30389  9p10ne21  30401  1mhdrd  32851  hgt750lem2  34633  60gcd7e1  41995  3lexlogpow5ineq1  42044  3lexlogpow2ineq2  42049  3lexlogpow5ineq5  42050  sq9  42288  sum9cubes  42662  fmtno5lem4  47554  257prm  47559  fmtno4nprmfac193  47572  139prmALT  47594  127prm  47597  8exp8mod9  47734  nfermltl8rev  47740  evengpop3  47796