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

Theorem 9cn 11729
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 11699 . 2 9 = (8 + 1)
2 8cn 11726 . . 3 8 ∈ ℂ
3 ax-1cn 10588 . . 3 1 ∈ ℂ
42, 3addcli 10640 . 2 (8 + 1) ∈ ℂ
51, 4eqeltri 2889 1 9 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2112  (class class class)co 7139  cc 10528  1c1 10531   + caddc 10533  8c8 11690  9c9 11691
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773  ax-1cn 10588  ax-addcl 10590
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794  df-clel 2873  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699
This theorem is referenced by:  10m1e9  12186  9t2e18  12212  9t8e72  12218  9t9e81  12219  9t11e99  12220  0.999...  15232  cos2bnd  15536  3dvds  15675  3dvdsdec  15676  3dvds2dec  15677  2exp8  16418  139prm  16452  163prm  16453  317prm  16454  631prm  16455  1259lem1  16459  1259lem2  16460  1259lem3  16461  1259lem4  16462  1259lem5  16463  2503lem1  16465  2503lem2  16466  2503lem3  16467  2503prm  16468  4001lem1  16469  4001lem2  16470  4001lem3  16471  4001lem4  16472  sqrt2cxp2logb9e3  25388  mcubic  25436  cubic2  25437  cubic  25438  quartlem1  25446  log2tlbnd  25534  log2ublem3  25537  log2ub  25538  bposlem8  25878  ex-lcm  28246  9p10ne21  28258  1mhdrd  30621  hgt750lem2  32031  60gcd7e1  39286  fmtno5lem4  44060  257prm  44065  fmtno4nprmfac193  44078  139prmALT  44100  127prm  44103  8exp8mod9  44241  nfermltl8rev  44247  evengpop3  44303
  Copyright terms: Public domain W3C validator