MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  9cn Structured version   Visualization version   GIF version

Theorem 9cn 12366
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
StepHypRef Expression
1 df-9 12336 . 2 9 = (8 + 1)
2 8cn 12363 . . 3 8 ∈ ℂ
3 ax-1cn 11213 . . 3 1 ∈ ℂ
42, 3addcli 11267 . 2 (8 + 1) ∈ ℂ
51, 4eqeltri 2837 1 9 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2108  (class class class)co 7431  cc 11153  1c1 11156   + caddc 11158  8c8 12327  9c9 12328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-addcl 11215
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336
This theorem is referenced by:  10m1e9  12829  9t2e18  12855  9t8e72  12861  9t9e81  12862  9t11e99  12863  0.999...  15917  cos2bnd  16224  3dvds  16368  3dvdsdec  16369  3dvds2dec  16370  2exp8  17126  139prm  17161  163prm  17162  317prm  17163  631prm  17164  1259lem1  17168  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  2503lem1  17174  2503lem2  17175  2503lem3  17176  2503prm  17177  4001lem1  17178  4001lem2  17179  4001lem3  17180  4001lem4  17181  sqrt2cxp2logb9e3  26842  mcubic  26890  cubic2  26891  cubic  26892  quartlem1  26900  log2tlbnd  26988  log2ublem3  26991  log2ub  26992  bposlem8  27335  ex-lcm  30477  9p10ne21  30489  1mhdrd  32898  hgt750lem2  34667  60gcd7e1  42006  3lexlogpow5ineq1  42055  3lexlogpow2ineq2  42060  3lexlogpow5ineq5  42061  sq9  42332  sum9cubes  42682  fmtno5lem4  47543  257prm  47548  fmtno4nprmfac193  47561  139prmALT  47583  127prm  47586  8exp8mod9  47723  nfermltl8rev  47729  evengpop3  47785
  Copyright terms: Public domain W3C validator