Theorem 9cn 12453

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 12422	. 2 ⊢ 9 = (8 + 1)
2		8cn 12450	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11268	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11325	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2859	1 ⊢ 9 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7427  ℂcc 11208  1c1 11211   + caddc 11213  8c8 12413  9c9 12414

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-1cn 11268  ax-addcl 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-clel 2838  df-2 12415  df-3 12416  df-4 12417  df-5 12418  df-6 12419  df-7 12420  df-8 12421  df-9 12422

This theorem is used by:  10m1e9  12925  9t2e18  12951  9t8e72  12957  9t9e81  12958  9t11e99OLD  12960  0.999...  16062  cos2bnd  16368  3dvds  16513  3dvdsdec  16514  3dvds2dec  16515  2exp8  17278  139prm  17314  163prm  17315  317prm  17316  631prm  17317  1259lem1  17321  1259lem2  17322  1259lem3  17323  1259lem4  17324  1259lem5  17325  2503lem1  17327  2503lem2  17328  2503lem3  17329  2503prm  17330  4001lem1  17331  4001lem2  17332  4001lem3  17333  4001lem4  17334  sqrt2cxp2logb9e3  27139  mcubic  27187  cubic2  27188  cubic  27189  quartlem1  27197  log2tlbnd  27285  log2ublem3  27288  log2ub  27289  bposlem8  27630  ex-lcm  31071  9p10ne21  31083  1mhdrd  33535  hgt750lem2  35334  60gcd7e1  43195  3lexlogpow5ineq1  43244  3lexlogpow2ineq2  43249  3lexlogpow5ineq5  43250  25or6to4  43396  sq9  43495  sum9cubes  43823  fmtno5lem4  48780  257prm  48785  fmtno4nprmfac193  48798  139prmALT  48820  127prm  48823  8exp8mod9  48973  nfermltl8rev  48979  evengpop3  49035