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

Theorem 8cn 11722
 Description: The number 8 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
8cn 8 ∈ ℂ

Proof of Theorem 8cn
StepHypRef Expression
1 df-8 11694 . 2 8 = (7 + 1)
2 7cn 11719 . . 3 7 ∈ ℂ
3 ax-1cn 10584 . . 3 1 ∈ ℂ
42, 3addcli 10636 . 2 (7 + 1) ∈ ℂ
51, 4eqeltri 2886 1 8 ∈ ℂ
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524  1c1 10527   + caddc 10529  7c7 11685  8c8 11686 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 2113  ax-9 2121  ax-ext 2770  ax-1cn 10584  ax-addcl 10586 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694 This theorem is referenced by:  9cn  11725  9m1e8  11759  8p2e10  12166  8t2e16  12201  8t5e40  12204  cos2bnd  15533  2exp16  16416  139prm  16449  163prm  16450  317prm  16451  631prm  16452  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  2503lem2  16463  2503lem3  16464  2503prm  16465  4001lem1  16466  4001lem2  16467  4001prm  16470  quart1cl  25440  quart1lem  25441  quart1  25442  quartlem1  25443  log2tlbnd  25531  log2ublem3  25534  log2ub  25535  bposlem8  25875  lgsdir2lem1  25909  lgsdir2lem5  25913  2lgslem3a  25980  2lgslem3b  25981  2lgslem3c  25982  2lgslem3d  25983  2lgslem3a1  25984  2lgslem3b1  25985  2lgslem3c1  25986  2lgslem3d1  25987  2lgsoddprmlem1  25992  2lgsoddprmlem2  25993  2lgsoddprmlem3a  25994  2lgsoddprmlem3b  25995  2lgsoddprmlem3c  25996  2lgsoddprmlem3d  25997  ex-exp  28235  hgt750lem2  32033  420lcm8e840  39299  ex-decpmul  39484  resqrtvalex  40343  imsqrtvalex  40344  fmtno5lem4  44071  257prm  44076  fmtnoprmfac2lem1  44081  fmtno4prmfac  44087  fmtno4nprmfac193  44089  fmtno5faclem3  44096  m3prm  44107  139prmALT  44111  127prm  44114  m7prm  44115  2exp11  44116  5tcu2e40  44131  2exp340mod341  44249  8exp8mod9  44252  nfermltl8rev  44258  evengpop3  44314  tgoldbachlt  44332
 Copyright terms: Public domain W3C validator