Theorem 9cn 12276

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 12246	. 2 ⊢ 9 = (8 + 1)
2		8cn 12273	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11092	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11147	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2837	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2121  (class class class)co 7359  ℂcc 11032  1c1 11035   + caddc 11037  8c8 12237  9c9 12238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-1cn 11092  ax-addcl 11094

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-clel 2816  df-2 12239  df-3 12240  df-4 12241  df-5 12242  df-6 12243  df-7 12244  df-8 12245  df-9 12246

This theorem is referenced by:  10m1e9  12735  9t2e18  12761  9t8e72  12767  9t9e81  12768  9t11e99  12769  0.999...  15841  cos2bnd  16150  3dvds  16295  3dvdsdec  16296  3dvds2dec  16297  2exp8  17054  139prm  17089  163prm  17090  317prm  17091  631prm  17092  1259lem1  17096  1259lem2  17097  1259lem3  17098  1259lem4  17099  1259lem5  17100  2503lem1  17102  2503lem2  17103  2503lem3  17104  2503prm  17105  4001lem1  17106  4001lem2  17107  4001lem3  17108  4001lem4  17109  sqrt2cxp2logb9e3  26784  mcubic  26832  cubic2  26833  cubic  26834  quartlem1  26842  log2tlbnd  26930  log2ublem3  26933  log2ub  26934  bposlem8  27275  ex-lcm  30548  9p10ne21  30560  1mhdrd  32996  hgt750lem2  34846  60gcd7e1  42503  3lexlogpow5ineq1  42552  3lexlogpow2ineq2  42557  3lexlogpow5ineq5  42558  sq9  42788  sum9cubes  43135  fmtno5lem4  48046  257prm  48051  fmtno4nprmfac193  48064  139prmALT  48086  127prm  48089  8exp8mod9  48239  nfermltl8rev  48245  evengpop3  48301