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

Theorem 9cn 12254
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 12224 . 2 9 = (8 + 1)
2 8cn 12251 . . 3 8 ∈ ℂ
3 ax-1cn 11110 . . 3 1 ∈ ℂ
42, 3addcli 11162 . 2 (8 + 1) ∈ ℂ
51, 4eqeltri 2834 1 9 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  (class class class)co 7358  cc 11050  1c1 11053   + caddc 11055  8c8 12215  9c9 12216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-1cn 11110  ax-addcl 11112
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-clel 2815  df-2 12217  df-3 12218  df-4 12219  df-5 12220  df-6 12221  df-7 12222  df-8 12223  df-9 12224
This theorem is referenced by:  10m1e9  12715  9t2e18  12741  9t8e72  12747  9t9e81  12748  9t11e99  12749  0.999...  15767  cos2bnd  16071  3dvds  16214  3dvdsdec  16215  3dvds2dec  16216  2exp8  16962  139prm  16997  163prm  16998  317prm  16999  631prm  17000  1259lem1  17004  1259lem2  17005  1259lem3  17006  1259lem4  17007  1259lem5  17008  2503lem1  17010  2503lem2  17011  2503lem3  17012  2503prm  17013  4001lem1  17014  4001lem2  17015  4001lem3  17016  4001lem4  17017  sqrt2cxp2logb9e3  26152  mcubic  26200  cubic2  26201  cubic  26202  quartlem1  26210  log2tlbnd  26298  log2ublem3  26301  log2ub  26302  bposlem8  26642  ex-lcm  29405  9p10ne21  29417  1mhdrd  31775  hgt750lem2  33268  60gcd7e1  40465  3lexlogpow5ineq1  40514  3lexlogpow2ineq2  40519  3lexlogpow5ineq5  40520  fmtno5lem4  45755  257prm  45760  fmtno4nprmfac193  45773  139prmALT  45795  127prm  45798  8exp8mod9  45935  nfermltl8rev  45941  evengpop3  45997
  Copyright terms: Public domain W3C validator