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

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

Proof of Theorem 6cn
StepHypRef Expression
1 df-6 11696 . 2 6 = (5 + 1)
2 5cn 11717 . . 3 5 ∈ ℂ
3 ax-1cn 10588 . . 3 1 ∈ ℂ
42, 3addcli 10640 . 2 (5 + 1) ∈ ℂ
51, 4eqeltri 2889 1 6 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2112  (class class class)co 7139  cc 10528  1c1 10531   + caddc 10533  5c5 11687  6c6 11688
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 2114  ax-9 2122  ax-ext 2773  ax-1cn 10588  ax-addcl 10590
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794  df-clel 2873  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696
This theorem is referenced by:  7cn  11723  7m1e6  11761  6p2e8  11788  6p3e9  11789  halfpm6th  11850  6p4e10  12162  6t2e12  12194  6t3e18  12195  6t5e30  12197  5recm6rec  12234  bpoly2  15406  bpoly3  15407  bpoly4  15408  efi4p  15485  ef01bndlem  15532  cos01bnd  15534  3lcm2e6woprm  15952  6lcm4e12  15953  2exp8  16418  2exp16  16419  19prm  16446  83prm  16451  163prm  16453  317prm  16454  631prm  16455  1259lem1  16459  1259lem2  16460  1259lem3  16461  1259lem4  16462  1259lem5  16463  2503lem1  16465  2503lem2  16466  2503lem3  16467  2503prm  16468  4001lem1  16469  4001lem2  16470  4001lem4  16472  4001prm  16473  sincos6thpi  25111  sincos3rdpi  25112  1cubrlem  25430  log2ublem3  25537  log2ub  25538  basellem5  25673  basellem8  25676  ppiub  25791  bclbnd  25867  bposlem8  25878  bposlem9  25879  2lgslem3d  25986  2lgsoddprmlem3d  26000  ex-exp  28238  ex-bc  28240  ex-gcd  28245  ex-lcm  28246  hgt750lemd  32027  hgt750lem2  32031  problem5  33020  60gcd6e6  39285  60lcm7e420  39291  lhe4.4ex1a  41020  wallispi2lem2  42701  fmtno5lem1  44057  fmtno5lem4  44060  fmtno5  44061  fmtno4prmfac  44076  fmtno5faclem2  44084  fmtno5faclem3  44085  fmtno5fac  44086  flsqrt5  44098  139prmALT  44100  127prm  44103  2exp11  44105  mod42tp1mod8  44107  2t6m3t4e0  44737  zlmodzxzequa  44892  zlmodzxzequap  44895
  Copyright terms: Public domain W3C validator