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

Theorem 5cn 10944
Description: The number 5 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
5cn 5 ∈ ℂ

Proof of Theorem 5cn
StepHypRef Expression
1 5re 10943 . 2 5 ∈ ℝ
21recni 9905 1 5 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  cc 9787  5c5 10917
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-i2m1 9857  ax-1ne0 9858  ax-rrecex 9861  ax-cnre 9862
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-br 4575  df-iota 5751  df-fv 5795  df-ov 6527  df-2 10923  df-3 10924  df-4 10925  df-5 10926
This theorem is referenced by:  6m1e5  10984  5p2e7  11009  5p3e8  11010  5p4e9  11011  5p5e10OLD  11012  5t2e10OLD  11026  5p5e10  11425  5t2e10  11463  5recm6rec  11515  bpoly4  14572  ef01bndlem  14696  dec5dvds  15549  dec5nprm  15551  2exp16  15578  prmlem1  15595  17prm  15605  139prm  15612  163prm  15613  317prm  15614  631prm  15615  prmo5  15617  prmo6  15618  1259lem1  15619  1259lem2  15620  1259lem3  15621  1259lem4  15622  2503lem1  15625  2503lem2  15626  2503lem3  15627  4001lem1  15629  4001lem2  15630  4001lem3  15631  4001lem4  15632  4001prm  15633  log2ublem3  24389  log2ub  24390  ppiublem2  24642  ppiub  24643  bclbnd  24719  bposlem4  24726  bposlem5  24727  bposlem6  24728  bposlem8  24730  bposlem9  24731  lgsdir2lem1  24764  2lgslem3c  24837  2lgsoddprmlem3d  24852  ex-fac  26463  fib6  29598  inductionexd  37273  fmtno5lem1  39805  fmtno5lem2  39806  257prm  39813  fmtno4prmfac193  39825  fmtno4nprmfac193  39826  flsqrt5  39849  139prmALT  39851  127prm  39855  2exp11  39857  5tcu2e40  39872  41prothprmlem2  39875  41prothprm  39876  gbpart8  39992  linevalexample  41977  5m4e1  42312
  Copyright terms: Public domain W3C validator