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

Theorem 9cn 12249
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 12219 . 2 9 = (8 + 1)
2 8cn 12246 . . 3 8 ∈ ℂ
3 ax-1cn 11105 . . 3 1 ∈ ℂ
42, 3addcli 11157 . 2 (8 + 1) ∈ ℂ
51, 4eqeltri 2834 1 9 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  (class class class)co 7353  cc 11045  1c1 11048   + caddc 11050  8c8 12210  9c9 12211
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-1cn 11105  ax-addcl 11107
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2728  df-clel 2814  df-2 12212  df-3 12213  df-4 12214  df-5 12215  df-6 12216  df-7 12217  df-8 12218  df-9 12219
This theorem is referenced by:  10m1e9  12710  9t2e18  12736  9t8e72  12742  9t9e81  12743  9t11e99  12744  0.999...  15758  cos2bnd  16062  3dvds  16205  3dvdsdec  16206  3dvds2dec  16207  2exp8  16953  139prm  16988  163prm  16989  317prm  16990  631prm  16991  1259lem1  16995  1259lem2  16996  1259lem3  16997  1259lem4  16998  1259lem5  16999  2503lem1  17001  2503lem2  17002  2503lem3  17003  2503prm  17004  4001lem1  17005  4001lem2  17006  4001lem3  17007  4001lem4  17008  sqrt2cxp2logb9e3  26133  mcubic  26181  cubic2  26182  cubic  26183  quartlem1  26191  log2tlbnd  26279  log2ublem3  26282  log2ub  26283  bposlem8  26623  ex-lcm  29288  9p10ne21  29300  1mhdrd  31655  hgt750lem2  33134  60gcd7e1  40429  3lexlogpow5ineq1  40478  3lexlogpow2ineq2  40483  3lexlogpow5ineq5  40484  fmtno5lem4  45680  257prm  45685  fmtno4nprmfac193  45698  139prmALT  45720  127prm  45723  8exp8mod9  45860  nfermltl8rev  45866  evengpop3  45922
  Copyright terms: Public domain W3C validator