Theorem 6cn 12234

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 12210	. 2 ⊢ 6 = (5 + 1)
2		5cn 12231	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11082	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11136	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2830	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2113  (class class class)co 7356  ℂcc 11022  1c1 11025   + caddc 11027  5c5 12201  6c6 12202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-1cn 11082  ax-addcl 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-clel 2809  df-2 12206  df-3 12207  df-4 12208  df-5 12209  df-6 12210

This theorem is referenced by:  7cn  12237  7m1e6  12270  6p2e8  12297  6p3e9  12298  halfpm6th  12361  6p4e10  12677  6t2e12  12709  6t3e18  12710  6t5e30  12712  5recm6rec  12748  bpoly2  15978  bpoly3  15979  bpoly4  15980  efi4p  16060  ef01bndlem  16107  cos01bnd  16109  3lcm2e6woprm  16540  6lcm4e12  16541  2exp8  17014  2exp11  17015  2exp16  17016  19prm  17043  83prm  17048  163prm  17050  317prm  17051  631prm  17052  1259lem1  17056  1259lem2  17057  1259lem3  17058  1259lem4  17059  1259lem5  17060  2503lem1  17062  2503lem2  17063  2503lem3  17064  2503prm  17065  4001lem1  17066  4001lem2  17067  4001lem4  17069  4001prm  17070  sincos6thpi  26479  sincos3rdpi  26480  1cubrlem  26805  log2ublem3  26912  log2ub  26913  basellem5  27049  basellem8  27052  ppiub  27169  bclbnd  27245  bposlem8  27256  bposlem9  27257  2lgslem3d  27364  2lgsoddprmlem3d  27378  ex-exp  30474  ex-bc  30476  ex-gcd  30481  ex-lcm  30482  hgt750lemd  34754  hgt750lem2  34758  problem5  35812  60gcd6e6  42197  60lcm7e420  42203  3exp7  42246  3lexlogpow5ineq1  42247  3lexlogpow5ineq5  42253  aks4d1p1p5  42268  aks4d1p1  42269  sq6  42492  lhe4.4ex1a  44512  wallispi2lem2  46258  fmtno5lem1  47741  fmtno5lem4  47744  fmtno5  47745  fmtno4prmfac  47760  fmtno5faclem2  47768  fmtno5faclem3  47769  fmtno5fac  47770  flsqrt5  47782  139prmALT  47784  127prm  47787  mod42tp1mod8  47790  2t6m3t4e0  48536  zlmodzxzequa  48684  zlmodzxzequap  48687