Theorem 9cn 12272

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 12242	. 2 ⊢ 9 = (8 + 1)
2		8cn 12269	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11087	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11142	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2835	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2119  (class class class)co 7356  ℂcc 11027  1c1 11030   + caddc 11032  8c8 12233  9c9 12234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087  ax-addcl 11089

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-7 12240  df-8 12241  df-9 12242

This theorem is referenced by:  10m1e9  12731  9t2e18  12757  9t8e72  12763  9t9e81  12764  9t11e99  12765  0.999...  15837  cos2bnd  16146  3dvds  16291  3dvdsdec  16292  3dvds2dec  16293  2exp8  17050  139prm  17085  163prm  17086  317prm  17087  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  2503lem1  17098  2503lem2  17099  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  sqrt2cxp2logb9e3  26781  mcubic  26829  cubic2  26830  cubic  26831  quartlem1  26839  log2tlbnd  26927  log2ublem3  26930  log2ub  26931  bposlem8  27272  ex-lcm  30546  9p10ne21  30558  1mhdrd  32994  hgt750lem2  34836  60gcd7e1  42490  3lexlogpow5ineq1  42539  3lexlogpow2ineq2  42544  3lexlogpow5ineq5  42545  sq9  42775  sum9cubes  43122  fmtno5lem4  48034  257prm  48039  fmtno4nprmfac193  48052  139prmALT  48074  127prm  48077  8exp8mod9  48227  nfermltl8rev  48233  evengpop3  48289