Theorem 6cn 12444

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 12419	. 2 ⊢ 6 = (5 + 1)
2		5cn 12441	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11268	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11325	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2859	1 ⊢ 6 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7427  ℂcc 11208  1c1 11211   + caddc 11213  5c5 12410  6c6 12411

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-1cn 11268  ax-addcl 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-clel 2838  df-2 12415  df-3 12416  df-4 12417  df-5 12418  df-6 12419

This theorem is used by:  7cn  12447  7m1e6  12484  6p2e8  12511  6p3e9  12512  8th4div3  12576  halfpm6th  12578  6p4e10  12901  6t2e12  12933  6t3e18  12934  6t5e30  12936  5recm6rec  12974  bpoly2  16235  bpoly3  16236  bpoly4  16237  efi4p  16317  ef01bndlem  16364  cos01bnd  16366  3lcm2e6woprm  16802  6lcm4e12  16803  2exp8  17278  2exp11  17279  2exp16  17280  19prm  17308  83prm  17313  163prm  17315  317prm  17316  631prm  17317  1259lem1  17321  1259lem2  17322  1259lem3  17323  1259lem4  17324  1259lem5  17325  2503lem1  17327  2503lem2  17328  2503lem3  17329  2503prm  17330  4001lem1  17331  4001lem2  17332  4001lem4  17334  4001prm  17335  sincos6thpi  26856  sincos3rdpi  26857  1cubrlem  27181  log2ublem3  27288  log2ub  27289  basellem5  27424  basellem8  27427  ppiub  27543  bclbnd  27619  bposlem8  27630  bposlem9  27631  2lgslem3d  27738  2lgsoddprmlem3d  27752  ex-exp  31063  ex-bc  31065  ex-gcd  31070  ex-lcm  31071  hgt750lemd  35330  hgt750lem2  35334  problem5  36555  60gcd6e6  43194  60lcm7e420  43200  3exp7  43243  3lexlogpow5ineq1  43244  3lexlogpow5ineq5  43250  aks4d1p1p5  43265  aks4d1p1  43266  25or6to4  43396  1p7e8  43454  sq6  43492  lhe4.4ex1a  45453  wallispi2lem2  47221  sin5tlem1  48058  sin5tlem4  48061  sin5tlem5  48062  fmtno5lem1  48777  fmtno5lem4  48780  fmtno5  48781  fmtno4prmfac  48796  fmtno5faclem2  48804  fmtno5faclem3  48805  fmtno5fac  48806  flsqrt5  48818  139prmALT  48820  127prm  48823  mod42tp1mod8  48826  2t6m3t4e0  49599  zlmodzxzequa  49747  zlmodzxzequap  49750