Theorem 9cn 11895

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 11865	. 2 ⊢ 9 = (8 + 1)
2		8cn 11892	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 10752	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10804	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2827	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2112  (class class class)co 7191  ℂcc 10692  1c1 10695   + caddc 10697  8c8 11856  9c9 11857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-1cn 10752  ax-addcl 10754

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-clel 2809  df-2 11858  df-3 11859  df-4 11860  df-5 11861  df-6 11862  df-7 11863  df-8 11864  df-9 11865

This theorem is referenced by:  10m1e9  12354  9t2e18  12380  9t8e72  12386  9t9e81  12387  9t11e99  12388  0.999...  15408  cos2bnd  15712  3dvds  15855  3dvdsdec  15856  3dvds2dec  15857  2exp8  16605  139prm  16640  163prm  16641  317prm  16642  631prm  16643  1259lem1  16647  1259lem2  16648  1259lem3  16649  1259lem4  16650  1259lem5  16651  2503lem1  16653  2503lem2  16654  2503lem3  16655  2503prm  16656  4001lem1  16657  4001lem2  16658  4001lem3  16659  4001lem4  16660  sqrt2cxp2logb9e3  25636  mcubic  25684  cubic2  25685  cubic  25686  quartlem1  25694  log2tlbnd  25782  log2ublem3  25785  log2ub  25786  bposlem8  26126  ex-lcm  28495  9p10ne21  28507  1mhdrd  30864  hgt750lem2  32298  60gcd7e1  39696  3lexlogpow5ineq1  39745  3lexlogpow2ineq2  39750  3lexlogpow5ineq5  39751  fmtno5lem4  44624  257prm  44629  fmtno4nprmfac193  44642  139prmALT  44664  127prm  44667  8exp8mod9  44804  nfermltl8rev  44810  evengpop3  44866