Theorem 9cn 12336

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 12305	. 2 ⊢ 9 = (8 + 1)
2		8cn 12333	. . 3 ⊢ 8 ∈ ℂ
3		ax-1cn 11153	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11210	. 2 ⊢ (8 + 1) ∈ ℂ
5	1, 4	eqeltri 2859	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093  1c1 11096   + caddc 11098  8c8 12296  9c9 12297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-addcl 11155

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838  df-2 12298  df-3 12299  df-4 12300  df-5 12301  df-6 12302  df-7 12303  df-8 12304  df-9 12305

This theorem is referenced by:  10m1e9  12807  9t2e18  12833  9t8e72  12839  9t9e81  12840  9t11e99OLD  12842  0.999...  15931  cos2bnd  16239  3dvds  16384  3dvdsdec  16385  3dvds2dec  16386  2exp8  17143  139prm  17179  163prm  17180  317prm  17181  631prm  17182  1259lem1  17186  1259lem2  17187  1259lem3  17188  1259lem4  17189  1259lem5  17190  2503lem1  17192  2503lem2  17193  2503lem3  17194  2503prm  17195  4001lem1  17196  4001lem2  17197  4001lem3  17198  4001lem4  17199  sqrt2cxp2logb9e3  26964  mcubic  27012  cubic2  27013  cubic  27014  quartlem1  27022  log2tlbnd  27110  log2ublem3  27113  log2ub  27114  bposlem8  27455  ex-lcm  30809  9p10ne21  30821  1mhdrd  33235  hgt750lem2  35039  60gcd7e1  42792  3lexlogpow5ineq1  42841  3lexlogpow2ineq2  42846  3lexlogpow5ineq5  42847  25or6to4  42993  sq9  43079  sum9cubes  43424  fmtno5lem4  48328  257prm  48333  fmtno4nprmfac193  48346  139prmALT  48368  127prm  48371  8exp8mod9  48521  nfermltl8rev  48527  evengpop3  48583