Theorem 9cn 12003

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 11973	. 2 ⊢ 9 = (8 + 1)
2		8cn 12000	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 10860	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10912	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2835	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800  1c1 10803   + caddc 10805  8c8 11964  9c9 11965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-addcl 10862

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817  df-2 11966  df-3 11967  df-4 11968  df-5 11969  df-6 11970  df-7 11971  df-8 11972  df-9 11973

This theorem is referenced by:  10m1e9  12462  9t2e18  12488  9t8e72  12494  9t9e81  12495  9t11e99  12496  0.999...  15521  cos2bnd  15825  3dvds  15968  3dvdsdec  15969  3dvds2dec  15970  2exp8  16718  139prm  16753  163prm  16754  317prm  16755  631prm  16756  1259lem1  16760  1259lem2  16761  1259lem3  16762  1259lem4  16763  1259lem5  16764  2503lem1  16766  2503lem2  16767  2503lem3  16768  2503prm  16769  4001lem1  16770  4001lem2  16771  4001lem3  16772  4001lem4  16773  sqrt2cxp2logb9e3  25854  mcubic  25902  cubic2  25903  cubic  25904  quartlem1  25912  log2tlbnd  26000  log2ublem3  26003  log2ub  26004  bposlem8  26344  ex-lcm  28723  9p10ne21  28735  1mhdrd  31092  hgt750lem2  32532  60gcd7e1  39941  3lexlogpow5ineq1  39990  3lexlogpow2ineq2  39995  3lexlogpow5ineq5  39996  fmtno5lem4  44896  257prm  44901  fmtno4nprmfac193  44914  139prmALT  44936  127prm  44939  8exp8mod9  45076  nfermltl8rev  45082  evengpop3  45138