Theorem 6cn 12267

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 12243	. 2 ⊢ 6 = (5 + 1)
2		5cn 12264	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11092	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11147	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2837	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2121  (class class class)co 7359  ℂcc 11032  1c1 11035   + caddc 11037  5c5 12234  6c6 12235

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-1cn 11092  ax-addcl 11094

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-clel 2816  df-2 12239  df-3 12240  df-4 12241  df-5 12242  df-6 12243

This theorem is referenced by:  7cn  12270  7m1e6  12303  6p2e8  12330  6p3e9  12331  halfpm6th  12394  6p4e10  12711  6t2e12  12743  6t3e18  12744  6t5e30  12746  5recm6rec  12782  bpoly2  16017  bpoly3  16018  bpoly4  16019  efi4p  16099  ef01bndlem  16146  cos01bnd  16148  3lcm2e6woprm  16579  6lcm4e12  16580  2exp8  17054  2exp11  17055  2exp16  17056  19prm  17083  83prm  17088  163prm  17090  317prm  17091  631prm  17092  1259lem1  17096  1259lem2  17097  1259lem3  17098  1259lem4  17099  1259lem5  17100  2503lem1  17102  2503lem2  17103  2503lem3  17104  2503prm  17105  4001lem1  17106  4001lem2  17107  4001lem4  17109  4001prm  17110  sincos6thpi  26501  sincos3rdpi  26502  1cubrlem  26826  log2ublem3  26933  log2ub  26934  basellem5  27069  basellem8  27072  ppiub  27188  bclbnd  27264  bposlem8  27275  bposlem9  27276  2lgslem3d  27383  2lgsoddprmlem3d  27397  ex-exp  30540  ex-bc  30542  ex-gcd  30547  ex-lcm  30548  hgt750lemd  34842  hgt750lem2  34846  problem5  35910  60gcd6e6  42502  60lcm7e420  42508  3exp7  42551  3lexlogpow5ineq1  42552  3lexlogpow5ineq5  42558  aks4d1p1p5  42573  aks4d1p1  42574  sq6  42785  lhe4.4ex1a  44786  wallispi2lem2  46527  sin5tlem1  47348  sin5tlem4  47351  sin5tlem5  47352  fmtno5lem1  48043  fmtno5lem4  48046  fmtno5  48047  fmtno4prmfac  48062  fmtno5faclem2  48070  fmtno5faclem3  48071  fmtno5fac  48072  flsqrt5  48084  139prmALT  48086  127prm  48089  mod42tp1mod8  48092  2t6m3t4e0  48851  zlmodzxzequa  48999  zlmodzxzequap  49002