Theorem 9cn 12368

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 12337	. 2 ⊢ 9 = (8 + 1)
2		8cn 12365	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11185	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11242	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2856	1 ⊢ 9 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7414  ℂcc 11125  1c1 11128   + caddc 11130  8c8 12328  9c9 12329

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 2732  ax-1cn 11185  ax-addcl 11187

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335  df-8 12336  df-9 12337

This theorem is used by:  10m1e9  12840  9t2e18  12866  9t8e72  12872  9t9e81  12873  9t11e99OLD  12875  0.999...  15973  cos2bnd  16279  3dvds  16424  3dvdsdec  16425  3dvds2dec  16426  2exp8  17183  139prm  17219  163prm  17220  317prm  17221  631prm  17222  1259lem1  17226  1259lem2  17227  1259lem3  17228  1259lem4  17229  1259lem5  17230  2503lem1  17232  2503lem2  17233  2503lem3  17234  2503prm  17235  4001lem1  17236  4001lem2  17237  4001lem3  17238  4001lem4  17239  sqrt2cxp2logb9e3  27039  mcubic  27087  cubic2  27088  cubic  27089  quartlem1  27097  log2tlbnd  27185  log2ublem3  27188  log2ub  27189  bposlem8  27530  ex-lcm  30941  9p10ne21  30953  1mhdrd  33364  hgt750lem2  35163  60gcd7e1  42874  3lexlogpow5ineq1  42923  3lexlogpow2ineq2  42928  3lexlogpow5ineq5  42929  25or6to4  43075  sq9  43176  sum9cubes  43521  fmtno5lem4  48462  257prm  48467  fmtno4nprmfac193  48480  139prmALT  48502  127prm  48505  8exp8mod9  48655  nfermltl8rev  48661  evengpop3  48717