Theorem 9cn 12443

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 12412	. 2 ⊢ 9 = (8 + 1)
2		8cn 12440	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11258	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11315	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2857	1 ⊢ 9 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7420  ℂcc 11198  1c1 11201   + caddc 11203  8c8 12403  9c9 12404

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 2147  ax-9 2155  ax-ext 2733  ax-1cn 11258  ax-addcl 11260

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836  df-2 12405  df-3 12406  df-4 12407  df-5 12408  df-6 12409  df-7 12410  df-8 12411  df-9 12412

This theorem is used by:  10m1e9  12915  9t2e18  12941  9t8e72  12947  9t9e81  12948  9t11e99OLD  12950  0.999...  16050  cos2bnd  16356  3dvds  16501  3dvdsdec  16502  3dvds2dec  16503  2exp8  17266  139prm  17302  163prm  17303  317prm  17304  631prm  17305  1259lem1  17309  1259lem2  17310  1259lem3  17311  1259lem4  17312  1259lem5  17313  2503lem1  17315  2503lem2  17316  2503lem3  17317  2503prm  17318  4001lem1  17319  4001lem2  17320  4001lem3  17321  4001lem4  17322  sqrt2cxp2logb9e3  27127  mcubic  27175  cubic2  27176  cubic  27177  quartlem1  27185  log2tlbnd  27273  log2ublem3  27276  log2ub  27277  bposlem8  27618  ex-lcm  31059  9p10ne21  31071  1mhdrd  33482  hgt750lem2  35281  60gcd7e1  43055  3lexlogpow5ineq1  43104  3lexlogpow2ineq2  43109  3lexlogpow5ineq5  43110  25or6to4  43256  sq9  43355  sum9cubes  43683  fmtno5lem4  48640  257prm  48645  fmtno4nprmfac193  48658  139prmALT  48680  127prm  48683  8exp8mod9  48833  nfermltl8rev  48839  evengpop3  48895