Theorem 6cn 12357

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

Step	Hyp	Ref	Expression
1		df-6 12333	. 2 ⊢ 6 = (5 + 1)
2		5cn 12354	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11213	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11267	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2837	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153  1c1 11156   + caddc 11158  5c5 12324  6c6 12325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-addcl 11215

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333

This theorem is referenced by:  7cn  12360  7m1e6  12398  6p2e8  12425  6p3e9  12426  halfpm6th  12487  6p4e10  12805  6t2e12  12837  6t3e18  12838  6t5e30  12840  5recm6rec  12877  bpoly2  16093  bpoly3  16094  bpoly4  16095  efi4p  16173  ef01bndlem  16220  cos01bnd  16222  3lcm2e6woprm  16652  6lcm4e12  16653  2exp8  17126  2exp11  17127  2exp16  17128  19prm  17155  83prm  17160  163prm  17162  317prm  17163  631prm  17164  1259lem1  17168  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  2503lem1  17174  2503lem2  17175  2503lem3  17176  2503prm  17177  4001lem1  17178  4001lem2  17179  4001lem4  17181  4001prm  17182  sincos6thpi  26558  sincos3rdpi  26559  1cubrlem  26884  log2ublem3  26991  log2ub  26992  basellem5  27128  basellem8  27131  ppiub  27248  bclbnd  27324  bposlem8  27335  bposlem9  27336  2lgslem3d  27443  2lgsoddprmlem3d  27457  ex-exp  30469  ex-bc  30471  ex-gcd  30476  ex-lcm  30477  hgt750lemd  34663  hgt750lem2  34667  problem5  35674  60gcd6e6  42005  60lcm7e420  42011  3exp7  42054  3lexlogpow5ineq1  42055  3lexlogpow5ineq5  42061  aks4d1p1p5  42076  aks4d1p1  42077  sq6  42329  lhe4.4ex1a  44348  wallispi2lem2  46087  fmtno5lem1  47540  fmtno5lem4  47543  fmtno5  47544  fmtno4prmfac  47559  fmtno5faclem2  47567  fmtno5faclem3  47568  fmtno5fac  47569  flsqrt5  47581  139prmALT  47583  127prm  47586  mod42tp1mod8  47589  2t6m3t4e0  48264  zlmodzxzequa  48413  zlmodzxzequap  48416