Theorem 9cn 12358

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 12327	. 2 ⊢ 9 = (8 + 1)
2		8cn 12355	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11175	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11232	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2861	1 ⊢ 9 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7419  ℂcc 11115  1c1 11118   + caddc 11120  8c8 12318  9c9 12319

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-1cn 11175  ax-addcl 11177

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840  df-2 12320  df-3 12321  df-4 12322  df-5 12323  df-6 12324  df-7 12325  df-8 12326  df-9 12327

This theorem is used by:  10m1e9  12830  9t2e18  12856  9t8e72  12862  9t9e81  12863  9t11e99OLD  12865  0.999...  15960  cos2bnd  16268  3dvds  16413  3dvdsdec  16414  3dvds2dec  16415  2exp8  17172  139prm  17208  163prm  17209  317prm  17210  631prm  17211  1259lem1  17215  1259lem2  17216  1259lem3  17217  1259lem4  17218  1259lem5  17219  2503lem1  17221  2503lem2  17222  2503lem3  17223  2503prm  17224  4001lem1  17225  4001lem2  17226  4001lem3  17227  4001lem4  17228  sqrt2cxp2logb9e3  27017  mcubic  27065  cubic2  27066  cubic  27067  quartlem1  27075  log2tlbnd  27163  log2ublem3  27166  log2ub  27167  bposlem8  27508  ex-lcm  30882  9p10ne21  30894  1mhdrd  33307  hgt750lem2  35106  60gcd7e1  42832  3lexlogpow5ineq1  42881  3lexlogpow2ineq2  42886  3lexlogpow5ineq5  42887  25or6to4  43033  sq9  43119  sum9cubes  43464  fmtno5lem4  48368  257prm  48373  fmtno4nprmfac193  48386  139prmALT  48408  127prm  48411  8exp8mod9  48561  nfermltl8rev  48567  evengpop3  48623