MPE Home 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 10583 . . 3 1 ∈ ℂ
42, 3addcli 10635 . 2 (7 + 1) ∈ ℂ
51, 4eqeltri 2906 1 8 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  (class class class)co 7145  cc 10523  1c1 10526   + caddc 10528  7c7 11685  8c8 11686
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790  ax-1cn 10583  ax-addcl 10585
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890  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  15529  2exp16  16412  139prm  16445  163prm  16446  317prm  16447  631prm  16448  1259lem2  16453  1259lem3  16454  1259lem4  16455  1259lem5  16456  2503lem2  16459  2503lem3  16460  2503prm  16461  4001lem1  16462  4001lem2  16463  4001prm  16466  quart1cl  25359  quart1lem  25360  quart1  25361  quartlem1  25362  log2tlbnd  25450  log2ublem3  25453  log2ub  25454  bposlem8  25794  lgsdir2lem1  25828  lgsdir2lem5  25832  2lgslem3a  25899  2lgslem3b  25900  2lgslem3c  25901  2lgslem3d  25902  2lgslem3a1  25903  2lgslem3b1  25904  2lgslem3c1  25905  2lgslem3d1  25906  2lgsoddprmlem1  25911  2lgsoddprmlem2  25912  2lgsoddprmlem3a  25913  2lgsoddprmlem3b  25914  2lgsoddprmlem3c  25915  2lgsoddprmlem3d  25916  ex-exp  28156  hgt750lem2  31822  ex-decpmul  39056  fmtno5lem4  43595  257prm  43600  fmtnoprmfac2lem1  43605  fmtno4prmfac  43611  fmtno4nprmfac193  43613  fmtno5faclem3  43620  m3prm  43631  139prmALT  43636  127prm  43640  m7prm  43641  2exp11  43642  5tcu2e40  43657  2exp340mod341  43775  8exp8mod9  43778  nfermltl8rev  43784  evengpop3  43840  tgoldbachlt  43858
  Copyright terms: Public domain W3C validator