Theorem 6cn 12216

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 12192	. 2 ⊢ 6 = (5 + 1)
2		5cn 12213	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11064	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11118	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2827	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004  1c1 11007   + caddc 11009  5c5 12183  6c6 12184

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 2113  ax-9 2121  ax-ext 2703  ax-1cn 11064  ax-addcl 11066

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-2 12188  df-3 12189  df-4 12190  df-5 12191  df-6 12192

This theorem is referenced by:  7cn  12219  7m1e6  12252  6p2e8  12279  6p3e9  12280  halfpm6th  12343  6p4e10  12660  6t2e12  12692  6t3e18  12693  6t5e30  12695  5recm6rec  12731  bpoly2  15964  bpoly3  15965  bpoly4  15966  efi4p  16046  ef01bndlem  16093  cos01bnd  16095  3lcm2e6woprm  16526  6lcm4e12  16527  2exp8  17000  2exp11  17001  2exp16  17002  19prm  17029  83prm  17034  163prm  17036  317prm  17037  631prm  17038  1259lem1  17042  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem4  17055  4001prm  17056  sincos6thpi  26452  sincos3rdpi  26453  1cubrlem  26778  log2ublem3  26885  log2ub  26886  basellem5  27022  basellem8  27025  ppiub  27142  bclbnd  27218  bposlem8  27229  bposlem9  27230  2lgslem3d  27337  2lgsoddprmlem3d  27351  ex-exp  30430  ex-bc  30432  ex-gcd  30437  ex-lcm  30438  hgt750lemd  34661  hgt750lem2  34665  problem5  35713  60gcd6e6  42107  60lcm7e420  42113  3exp7  42156  3lexlogpow5ineq1  42157  3lexlogpow5ineq5  42163  aks4d1p1p5  42178  aks4d1p1  42179  sq6  42398  lhe4.4ex1a  44432  wallispi2lem2  46180  fmtno5lem1  47663  fmtno5lem4  47666  fmtno5  47667  fmtno4prmfac  47682  fmtno5faclem2  47690  fmtno5faclem3  47691  fmtno5fac  47692  flsqrt5  47704  139prmALT  47706  127prm  47709  mod42tp1mod8  47712  2t6m3t4e0  48458  zlmodzxzequa  48607  zlmodzxzequap  48610