Theorem 9cn 11544

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 11508	. 2 ⊢ 9 = (8 + 1)
2		8cn 11540	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 10391	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10444	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2855	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2051  (class class class)co 6974  ℂcc 10331  1c1 10334   + caddc 10336  8c8 11499  9c9 11500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-ext 2743  ax-1cn 10391  ax-addcl 10393

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-cleq 2764  df-clel 2839  df-2 11501  df-3 11502  df-4 11503  df-5 11504  df-6 11505  df-7 11506  df-8 11507  df-9 11508

This theorem is referenced by:  10m1e9  12007  9t2e18  12033  9t8e72  12039  9t9e81  12040  9t11e99  12041  0.999...  15095  cos2bnd  15399  3dvds  15538  3dvdsdec  15539  3dvds2dec  15540  2exp8  16277  139prm  16311  163prm  16312  317prm  16313  631prm  16314  1259lem1  16318  1259lem2  16319  1259lem3  16320  1259lem4  16321  1259lem5  16322  2503lem1  16324  2503lem2  16325  2503lem3  16326  2503prm  16327  4001lem1  16328  4001lem2  16329  4001lem3  16330  4001lem4  16331  sqrt2cxp2logb9e3  25093  mcubic  25141  cubic2  25142  cubic  25143  quartlem1  25151  log2tlbnd  25240  log2ublem3  25243  log2ub  25244  bposlem8  25584  ex-lcm  28030  9p10ne21  28041  1mhdrd  30362  hgt750lem2  31603  fmtno5lem4  43120  257prm  43125  fmtno4nprmfac193  43138  139prmALT  43161  127prm  43165  8exp8mod9  43303  nfermltl8rev  43309  evengpop3  43365