Theorem 9cn 12257

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 12227	. 2 ⊢ 9 = (8 + 1)
2		8cn 12254	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11150	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2833	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036  1c1 11039   + caddc 11041  8c8 12218  9c9 12219

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 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-2 12220  df-3 12221  df-4 12222  df-5 12223  df-6 12224  df-7 12225  df-8 12226  df-9 12227

This theorem is referenced by:  10m1e9  12715  9t2e18  12741  9t8e72  12747  9t9e81  12748  9t11e99  12749  0.999...  15816  cos2bnd  16125  3dvds  16270  3dvdsdec  16271  3dvds2dec  16272  2exp8  17028  139prm  17063  163prm  17064  317prm  17065  631prm  17066  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  2503lem1  17076  2503lem2  17077  2503lem3  17078  2503prm  17079  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  sqrt2cxp2logb9e3  26780  mcubic  26828  cubic2  26829  cubic  26830  quartlem1  26838  log2tlbnd  26926  log2ublem3  26929  log2ub  26930  bposlem8  27273  ex-lcm  30549  9p10ne21  30561  1mhdrd  33012  hgt750lem2  34834  60gcd7e1  42379  3lexlogpow5ineq1  42428  3lexlogpow2ineq2  42433  3lexlogpow5ineq5  42434  sq9  42672  sum9cubes  43034  fmtno5lem4  47920  257prm  47925  fmtno4nprmfac193  47938  139prmALT  47960  127prm  47963  8exp8mod9  48100  nfermltl8rev  48106  evengpop3  48162