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

Theorem 6cn 12245
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 12221 . 2 6 = (5 + 1)
2 5cn 12242 . . 3 5 ∈ ℂ
3 ax-1cn 11110 . . 3 1 ∈ ℂ
42, 3addcli 11162 . 2 (5 + 1) ∈ ℂ
51, 4eqeltri 2834 1 6 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  (class class class)co 7358  cc 11050  1c1 11053   + caddc 11055  5c5 12212  6c6 12213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-1cn 11110  ax-addcl 11112
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-clel 2815  df-2 12217  df-3 12218  df-4 12219  df-5 12220  df-6 12221
This theorem is referenced by:  7cn  12248  7m1e6  12286  6p2e8  12313  6p3e9  12314  halfpm6th  12375  6p4e10  12691  6t2e12  12723  6t3e18  12724  6t5e30  12726  5recm6rec  12763  bpoly2  15941  bpoly3  15942  bpoly4  15943  efi4p  16020  ef01bndlem  16067  cos01bnd  16069  3lcm2e6woprm  16492  6lcm4e12  16493  2exp8  16962  2exp11  16963  2exp16  16964  19prm  16991  83prm  16996  163prm  16998  317prm  16999  631prm  17000  1259lem1  17004  1259lem2  17005  1259lem3  17006  1259lem4  17007  1259lem5  17008  2503lem1  17010  2503lem2  17011  2503lem3  17012  2503prm  17013  4001lem1  17014  4001lem2  17015  4001lem4  17017  4001prm  17018  sincos6thpi  25875  sincos3rdpi  25876  1cubrlem  26194  log2ublem3  26301  log2ub  26302  basellem5  26437  basellem8  26440  ppiub  26555  bclbnd  26631  bposlem8  26642  bposlem9  26643  2lgslem3d  26750  2lgsoddprmlem3d  26764  ex-exp  29397  ex-bc  29399  ex-gcd  29404  ex-lcm  29405  hgt750lemd  33264  hgt750lem2  33268  problem5  34260  60gcd6e6  40464  60lcm7e420  40470  3exp7  40513  3lexlogpow5ineq1  40514  3lexlogpow5ineq5  40520  aks4d1p1p5  40535  aks4d1p1  40536  lhe4.4ex1a  42616  wallispi2lem2  44320  fmtno5lem1  45752  fmtno5lem4  45755  fmtno5  45756  fmtno4prmfac  45771  fmtno5faclem2  45779  fmtno5faclem3  45780  fmtno5fac  45781  flsqrt5  45793  139prmALT  45795  127prm  45798  mod42tp1mod8  45801  2t6m3t4e0  46431  zlmodzxzequa  46584  zlmodzxzequap  46587
  Copyright terms: Public domain W3C validator