Theorem 6cn 12277

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 12253	. 2 ⊢ 6 = (5 + 1)
2		5cn 12274	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11126	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11180	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066  1c1 11069   + caddc 11071  5c5 12244  6c6 12245

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-addcl 11128

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12249  df-3 12250  df-4 12251  df-5 12252  df-6 12253

This theorem is referenced by:  7cn  12280  7m1e6  12313  6p2e8  12340  6p3e9  12341  halfpm6th  12404  6p4e10  12721  6t2e12  12753  6t3e18  12754  6t5e30  12756  5recm6rec  12792  bpoly2  16023  bpoly3  16024  bpoly4  16025  efi4p  16105  ef01bndlem  16152  cos01bnd  16154  3lcm2e6woprm  16585  6lcm4e12  16586  2exp8  17059  2exp11  17060  2exp16  17061  19prm  17088  83prm  17093  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem4  17114  4001prm  17115  sincos6thpi  26425  sincos3rdpi  26426  1cubrlem  26751  log2ublem3  26858  log2ub  26859  basellem5  26995  basellem8  26998  ppiub  27115  bclbnd  27191  bposlem8  27202  bposlem9  27203  2lgslem3d  27310  2lgsoddprmlem3d  27324  ex-exp  30379  ex-bc  30381  ex-gcd  30386  ex-lcm  30387  hgt750lemd  34639  hgt750lem2  34643  problem5  35656  60gcd6e6  41992  60lcm7e420  41998  3exp7  42041  3lexlogpow5ineq1  42042  3lexlogpow5ineq5  42048  aks4d1p1p5  42063  aks4d1p1  42064  sq6  42283  lhe4.4ex1a  44318  wallispi2lem2  46070  fmtno5lem1  47554  fmtno5lem4  47557  fmtno5  47558  fmtno4prmfac  47573  fmtno5faclem2  47581  fmtno5faclem3  47582  fmtno5fac  47583  flsqrt5  47595  139prmALT  47597  127prm  47600  mod42tp1mod8  47603  2t6m3t4e0  48336  zlmodzxzequa  48485  zlmodzxzequap  48488