Theorem 9cn 11731

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 11701	. 2 ⊢ 9 = (8 + 1)
2		8cn 11728	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 10589	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10641	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2909	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2110  (class class class)co 7150  ℂcc 10529  1c1 10532   + caddc 10534  8c8 11692  9c9 11693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793  ax-1cn 10589  ax-addcl 10591

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893  df-2 11694  df-3 11695  df-4 11696  df-5 11697  df-6 11698  df-7 11699  df-8 11700  df-9 11701

This theorem is referenced by:  10m1e9  12188  9t2e18  12214  9t8e72  12220  9t9e81  12221  9t11e99  12222  0.999...  15231  cos2bnd  15535  3dvds  15674  3dvdsdec  15675  3dvds2dec  15676  2exp8  16417  139prm  16451  163prm  16452  317prm  16453  631prm  16454  1259lem1  16458  1259lem2  16459  1259lem3  16460  1259lem4  16461  1259lem5  16462  2503lem1  16464  2503lem2  16465  2503lem3  16466  2503prm  16467  4001lem1  16468  4001lem2  16469  4001lem3  16470  4001lem4  16471  sqrt2cxp2logb9e3  25371  mcubic  25419  cubic2  25420  cubic  25421  quartlem1  25429  log2tlbnd  25517  log2ublem3  25520  log2ub  25521  bposlem8  25861  ex-lcm  28231  9p10ne21  28243  1mhdrd  30587  hgt750lem2  31918  fmtno5lem4  43711  257prm  43716  fmtno4nprmfac193  43729  139prmALT  43752  127prm  43756  8exp8mod9  43894  nfermltl8rev  43900  evengpop3  43956