Theorem 9cn 12228

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 12198	. 2 ⊢ 9 = (8 + 1)
2		8cn 12225	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11067	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11121	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007  1c1 11010   + caddc 11012  8c8 12189  9c9 12190

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 11067  ax-addcl 11069

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12191  df-3 12192  df-4 12193  df-5 12194  df-6 12195  df-7 12196  df-8 12197  df-9 12198

This theorem is referenced by:  10m1e9  12687  9t2e18  12713  9t8e72  12719  9t9e81  12720  9t11e99  12721  0.999...  15788  cos2bnd  16097  3dvds  16242  3dvdsdec  16243  3dvds2dec  16244  2exp8  17000  139prm  17035  163prm  17036  317prm  17037  631prm  17038  1259lem1  17042  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  sqrt2cxp2logb9e3  26707  mcubic  26755  cubic2  26756  cubic  26757  quartlem1  26765  log2tlbnd  26853  log2ublem3  26856  log2ub  26857  bposlem8  27200  ex-lcm  30402  9p10ne21  30414  1mhdrd  32856  hgt750lem2  34620  60gcd7e1  41982  3lexlogpow5ineq1  42031  3lexlogpow2ineq2  42036  3lexlogpow5ineq5  42037  sq9  42275  sum9cubes  42649  fmtno5lem4  47544  257prm  47549  fmtno4nprmfac193  47562  139prmALT  47584  127prm  47587  8exp8mod9  47724  nfermltl8rev  47730  evengpop3  47786