Theorem 9cn 12340

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 12310	. 2 ⊢ 9 = (8 + 1)
2		8cn 12337	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11187	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11241	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2830	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7405  ℂcc 11127  1c1 11130   + caddc 11132  8c8 12301  9c9 12302

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11187  ax-addcl 11189

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809  df-2 12303  df-3 12304  df-4 12305  df-5 12306  df-6 12307  df-7 12308  df-8 12309  df-9 12310

This theorem is referenced by:  10m1e9  12804  9t2e18  12830  9t8e72  12836  9t9e81  12837  9t11e99  12838  0.999...  15897  cos2bnd  16206  3dvds  16350  3dvdsdec  16351  3dvds2dec  16352  2exp8  17108  139prm  17143  163prm  17144  317prm  17145  631prm  17146  1259lem1  17150  1259lem2  17151  1259lem3  17152  1259lem4  17153  1259lem5  17154  2503lem1  17156  2503lem2  17157  2503lem3  17158  2503prm  17159  4001lem1  17160  4001lem2  17161  4001lem3  17162  4001lem4  17163  sqrt2cxp2logb9e3  26761  mcubic  26809  cubic2  26810  cubic  26811  quartlem1  26819  log2tlbnd  26907  log2ublem3  26910  log2ub  26911  bposlem8  27254  ex-lcm  30439  9p10ne21  30451  1mhdrd  32890  hgt750lem2  34684  60gcd7e1  42018  3lexlogpow5ineq1  42067  3lexlogpow2ineq2  42072  3lexlogpow5ineq5  42073  sq9  42347  sum9cubes  42695  fmtno5lem4  47570  257prm  47575  fmtno4nprmfac193  47588  139prmALT  47610  127prm  47613  8exp8mod9  47750  nfermltl8rev  47756  evengpop3  47812