Theorem 6cn 12073

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 12049	. 2 ⊢ 6 = (5 + 1)
2		5cn 12070	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 10938	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10990	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2836	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2107  (class class class)co 7284  ℂcc 10878  1c1 10881   + caddc 10883  5c5 12040  6c6 12041

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 2710  ax-1cn 10938  ax-addcl 10940

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817  df-2 12045  df-3 12046  df-4 12047  df-5 12048  df-6 12049

This theorem is referenced by:  7cn  12076  7m1e6  12114  6p2e8  12141  6p3e9  12142  halfpm6th  12203  6p4e10  12518  6t2e12  12550  6t3e18  12551  6t5e30  12553  5recm6rec  12590  bpoly2  15776  bpoly3  15777  bpoly4  15778  efi4p  15855  ef01bndlem  15902  cos01bnd  15904  3lcm2e6woprm  16329  6lcm4e12  16330  2exp8  16799  2exp11  16800  2exp16  16801  19prm  16828  83prm  16833  163prm  16835  317prm  16836  631prm  16837  1259lem1  16841  1259lem2  16842  1259lem3  16843  1259lem4  16844  1259lem5  16845  2503lem1  16847  2503lem2  16848  2503lem3  16849  2503prm  16850  4001lem1  16851  4001lem2  16852  4001lem4  16854  4001prm  16855  sincos6thpi  25681  sincos3rdpi  25682  1cubrlem  26000  log2ublem3  26107  log2ub  26108  basellem5  26243  basellem8  26246  ppiub  26361  bclbnd  26437  bposlem8  26448  bposlem9  26449  2lgslem3d  26556  2lgsoddprmlem3d  26570  ex-exp  28823  ex-bc  28825  ex-gcd  28830  ex-lcm  28831  hgt750lemd  32637  hgt750lem2  32641  problem5  33636  60gcd6e6  40019  60lcm7e420  40025  3exp7  40068  3lexlogpow5ineq1  40069  3lexlogpow5ineq5  40075  aks4d1p1p5  40090  aks4d1p1  40091  lhe4.4ex1a  41954  wallispi2lem2  43620  fmtno5lem1  45016  fmtno5lem4  45019  fmtno5  45020  fmtno4prmfac  45035  fmtno5faclem2  45043  fmtno5faclem3  45044  fmtno5fac  45045  flsqrt5  45057  139prmALT  45059  127prm  45062  mod42tp1mod8  45065  2t6m3t4e0  45695  zlmodzxzequa  45848  zlmodzxzequap  45851