Theorem 6cn 12263

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 12239	. 2 ⊢ 6 = (5 + 1)
2		5cn 12260	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11087	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11142	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2835	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2119  (class class class)co 7356  ℂcc 11027  1c1 11030   + caddc 11032  5c5 12230  6c6 12231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087  ax-addcl 11089

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239

This theorem is referenced by:  7cn  12266  7m1e6  12299  6p2e8  12326  6p3e9  12327  halfpm6th  12390  6p4e10  12707  6t2e12  12739  6t3e18  12740  6t5e30  12742  5recm6rec  12778  bpoly2  16013  bpoly3  16014  bpoly4  16015  efi4p  16095  ef01bndlem  16142  cos01bnd  16144  3lcm2e6woprm  16575  6lcm4e12  16576  2exp8  17050  2exp11  17051  2exp16  17052  19prm  17079  83prm  17084  163prm  17086  317prm  17087  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  2503lem1  17098  2503lem2  17099  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem4  17105  4001prm  17106  sincos6thpi  26498  sincos3rdpi  26499  1cubrlem  26823  log2ublem3  26930  log2ub  26931  basellem5  27066  basellem8  27069  ppiub  27185  bclbnd  27261  bposlem8  27272  bposlem9  27273  2lgslem3d  27380  2lgsoddprmlem3d  27394  ex-exp  30538  ex-bc  30540  ex-gcd  30545  ex-lcm  30546  hgt750lemd  34832  hgt750lem2  34836  problem5  35897  60gcd6e6  42489  60lcm7e420  42495  3exp7  42538  3lexlogpow5ineq1  42539  3lexlogpow5ineq5  42545  aks4d1p1p5  42560  aks4d1p1  42561  sq6  42772  lhe4.4ex1a  44773  wallispi2lem2  46515  sin5tlem1  47336  sin5tlem4  47339  sin5tlem5  47340  fmtno5lem1  48031  fmtno5lem4  48034  fmtno5  48035  fmtno4prmfac  48050  fmtno5faclem2  48058  fmtno5faclem3  48059  fmtno5fac  48060  flsqrt5  48072  139prmALT  48074  127prm  48077  mod42tp1mod8  48080  2t6m3t4e0  48839  zlmodzxzequa  48987  zlmodzxzequap  48990