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

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

Proof of Theorem 6cn
StepHypRef Expression
1 6re 11053 . 2 6 ∈ ℝ
21recni 10004 1 6 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  cc 9886  6c6 11026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-i2m1 9956  ax-1ne0 9957  ax-rrecex 9960  ax-cnre 9961
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5815  df-fv 5860  df-ov 6613  df-2 11031  df-3 11032  df-4 11033  df-5 11034  df-6 11035
This theorem is referenced by:  7m1e6  11093  6p2e8  11121  6p3e9  11122  6p4e10OLD  11123  halfpm6th  11205  6p4e10  11550  6t2e12  11593  6t3e18  11594  6t5e30  11596  5recm6rec  11638  bpoly2  14724  bpoly3  14725  bpoly4  14726  efi4p  14803  ef01bndlem  14850  cos01bnd  14852  3lcm2e6woprm  15263  6lcm4e12  15264  2exp8  15731  2exp16  15732  19prm  15760  83prm  15765  163prm  15767  317prm  15768  631prm  15769  prmo6  15772  1259lem1  15773  1259lem2  15774  1259lem3  15775  1259lem4  15776  1259lem5  15777  2503lem1  15779  2503lem2  15780  2503lem3  15781  2503prm  15782  4001lem1  15783  4001lem2  15784  4001lem4  15786  4001prm  15787  sincos6thpi  24188  sincos3rdpi  24189  1cubrlem  24485  log2ublem3  24592  log2ub  24593  basellem5  24728  basellem8  24731  ppiub  24846  bclbnd  24922  bposlem8  24933  bposlem9  24934  2lgslem3d  25041  2lgsoddprmlem3d  25055  ex-exp  27178  ex-bc  27180  ex-gcd  27185  ex-lcm  27186  problem5  31306  lhe4.4ex1a  38045  wallispi2lem2  39622  fmtno5lem1  40790  fmtno5lem4  40793  fmtno5  40794  fmtno4prmfac  40809  fmtno5faclem2  40817  fmtno5faclem3  40818  fmtno5fac  40819  flsqrt5  40834  139prmALT  40836  127prm  40840  2exp11  40842  mod42tp1mod8  40844  2t6m3t4e0  41440  zlmodzxzequa  41599  zlmodzxzequap  41602
  Copyright terms: Public domain W3C validator