Theorem 6cn 12272

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 12248	. 2 ⊢ 6 = (5 + 1)
2		5cn 12269	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11151	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2832	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036  1c1 11039   + caddc 11041  5c5 12239  6c6 12240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248

This theorem is referenced by:  7cn  12275  7m1e6  12308  6p2e8  12335  6p3e9  12336  halfpm6th  12399  6p4e10  12716  6t2e12  12748  6t3e18  12749  6t5e30  12751  5recm6rec  12787  bpoly2  16022  bpoly3  16023  bpoly4  16024  efi4p  16104  ef01bndlem  16151  cos01bnd  16153  3lcm2e6woprm  16584  6lcm4e12  16585  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  26480  sincos3rdpi  26481  1cubrlem  26805  log2ublem3  26912  log2ub  26913  basellem5  27048  basellem8  27051  ppiub  27167  bclbnd  27243  bposlem8  27254  bposlem9  27255  2lgslem3d  27362  2lgsoddprmlem3d  27376  ex-exp  30520  ex-bc  30522  ex-gcd  30527  ex-lcm  30528  hgt750lemd  34792  hgt750lem2  34796  problem5  35851  60gcd6e6  42443  60lcm7e420  42449  3exp7  42492  3lexlogpow5ineq1  42493  3lexlogpow5ineq5  42499  aks4d1p1p5  42514  aks4d1p1  42515  sq6  42727  lhe4.4ex1a  44756  wallispi2lem2  46500  sin5tlem1  47321  sin5tlem4  47324  sin5tlem5  47325  fmtno5lem1  48016  fmtno5lem4  48019  fmtno5  48020  fmtno4prmfac  48035  fmtno5faclem2  48043  fmtno5faclem3  48044  fmtno5fac  48045  flsqrt5  48057  139prmALT  48059  127prm  48062  mod42tp1mod8  48065  2t6m3t4e0  48824  zlmodzxzequa  48972  zlmodzxzequap  48975