Theorem 9cn 12275

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 12245	. 2 ⊢ 9 = (8 + 1)
2		8cn 12272	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11090	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11145	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2833	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7361  ℂcc 11030  1c1 11033   + caddc 11035  8c8 12236  9c9 12237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11090  ax-addcl 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-2 12238  df-3 12239  df-4 12240  df-5 12241  df-6 12242  df-7 12243  df-8 12244  df-9 12245

This theorem is referenced by:  10m1e9  12734  9t2e18  12760  9t8e72  12766  9t9e81  12767  9t11e99  12768  0.999...  15840  cos2bnd  16149  3dvds  16294  3dvdsdec  16295  3dvds2dec  16296  2exp8  17053  139prm  17088  163prm  17089  317prm  17090  631prm  17091  1259lem1  17095  1259lem2  17096  1259lem3  17097  1259lem4  17098  1259lem5  17099  2503lem1  17101  2503lem2  17102  2503lem3  17103  2503prm  17104  4001lem1  17105  4001lem2  17106  4001lem3  17107  4001lem4  17108  sqrt2cxp2logb9e3  26779  mcubic  26827  cubic2  26828  cubic  26829  quartlem1  26837  log2tlbnd  26925  log2ublem3  26928  log2ub  26929  bposlem8  27271  ex-lcm  30546  9p10ne21  30558  1mhdrd  32993  hgt750lem2  34815  60gcd7e1  42461  3lexlogpow5ineq1  42510  3lexlogpow2ineq2  42515  3lexlogpow5ineq5  42516  sq9  42747  sum9cubes  43122  fmtno5lem4  48034  257prm  48039  fmtno4nprmfac193  48052  139prmALT  48074  127prm  48077  8exp8mod9  48227  nfermltl8rev  48233  evengpop3  48289