Theorem 9cn 12262

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 12232	. 2 ⊢ 9 = (8 + 1)
2		8cn 12259	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11102	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11156	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042  1c1 11045   + caddc 11047  8c8 12223  9c9 12224

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 11102  ax-addcl 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230  df-8 12231  df-9 12232

This theorem is referenced by:  10m1e9  12721  9t2e18  12747  9t8e72  12753  9t9e81  12754  9t11e99  12755  0.999...  15823  cos2bnd  16132  3dvds  16277  3dvdsdec  16278  3dvds2dec  16279  2exp8  17035  139prm  17070  163prm  17071  317prm  17072  631prm  17073  1259lem1  17077  1259lem2  17078  1259lem3  17079  1259lem4  17080  1259lem5  17081  2503lem1  17083  2503lem2  17084  2503lem3  17085  2503prm  17086  4001lem1  17087  4001lem2  17088  4001lem3  17089  4001lem4  17090  sqrt2cxp2logb9e3  26685  mcubic  26733  cubic2  26734  cubic  26735  quartlem1  26743  log2tlbnd  26831  log2ublem3  26834  log2ub  26835  bposlem8  27178  ex-lcm  30360  9p10ne21  30372  1mhdrd  32809  hgt750lem2  34616  60gcd7e1  41966  3lexlogpow5ineq1  42015  3lexlogpow2ineq2  42020  3lexlogpow5ineq5  42021  sq9  42259  sum9cubes  42633  fmtno5lem4  47530  257prm  47535  fmtno4nprmfac193  47548  139prmALT  47570  127prm  47573  8exp8mod9  47710  nfermltl8rev  47716  evengpop3  47772