Theorem 9cn 11736

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 11706	. 2 ⊢ 9 = (8 + 1)
2		8cn 11733	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 10594	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10646	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2909	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2110  (class class class)co 7155  ℂcc 10534  1c1 10537   + caddc 10539  8c8 11697  9c9 11698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793  ax-1cn 10594  ax-addcl 10596

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893  df-2 11699  df-3 11700  df-4 11701  df-5 11702  df-6 11703  df-7 11704  df-8 11705  df-9 11706

This theorem is referenced by:  10m1e9  12193  9t2e18  12219  9t8e72  12225  9t9e81  12226  9t11e99  12227  0.999...  15236  cos2bnd  15540  3dvds  15679  3dvdsdec  15680  3dvds2dec  15681  2exp8  16422  139prm  16456  163prm  16457  317prm  16458  631prm  16459  1259lem1  16463  1259lem2  16464  1259lem3  16465  1259lem4  16466  1259lem5  16467  2503lem1  16469  2503lem2  16470  2503lem3  16471  2503prm  16472  4001lem1  16473  4001lem2  16474  4001lem3  16475  4001lem4  16476  sqrt2cxp2logb9e3  25376  mcubic  25424  cubic2  25425  cubic  25426  quartlem1  25434  log2tlbnd  25522  log2ublem3  25525  log2ub  25526  bposlem8  25866  ex-lcm  28236  9p10ne21  28248  1mhdrd  30592  hgt750lem2  31923  fmtno5lem4  43717  257prm  43722  fmtno4nprmfac193  43735  139prmALT  43758  127prm  43762  8exp8mod9  43900  nfermltl8rev  43906  evengpop3  43962