Theorem 6cn 12354

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 12330	. 2 ⊢ 6 = (5 + 1)
2		5cn 12351	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11210	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11264	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2834	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150  1c1 11153   + caddc 11155  5c5 12321  6c6 12322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-addcl 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330

This theorem is referenced by:  7cn  12357  7m1e6  12395  6p2e8  12422  6p3e9  12423  halfpm6th  12484  6p4e10  12802  6t2e12  12834  6t3e18  12835  6t5e30  12837  5recm6rec  12874  bpoly2  16089  bpoly3  16090  bpoly4  16091  efi4p  16169  ef01bndlem  16216  cos01bnd  16218  3lcm2e6woprm  16648  6lcm4e12  16649  2exp8  17122  2exp11  17123  2exp16  17124  19prm  17151  83prm  17156  163prm  17158  317prm  17159  631prm  17160  1259lem1  17164  1259lem2  17165  1259lem3  17166  1259lem4  17167  1259lem5  17168  2503lem1  17170  2503lem2  17171  2503lem3  17172  2503prm  17173  4001lem1  17174  4001lem2  17175  4001lem4  17177  4001prm  17178  sincos6thpi  26572  sincos3rdpi  26573  1cubrlem  26898  log2ublem3  27005  log2ub  27006  basellem5  27142  basellem8  27145  ppiub  27262  bclbnd  27338  bposlem8  27349  bposlem9  27350  2lgslem3d  27457  2lgsoddprmlem3d  27471  ex-exp  30478  ex-bc  30480  ex-gcd  30485  ex-lcm  30486  hgt750lemd  34641  hgt750lem2  34645  problem5  35653  60gcd6e6  41985  60lcm7e420  41991  3exp7  42034  3lexlogpow5ineq1  42035  3lexlogpow5ineq5  42041  aks4d1p1p5  42056  aks4d1p1  42057  sq6  42307  lhe4.4ex1a  44324  wallispi2lem2  46027  fmtno5lem1  47477  fmtno5lem4  47480  fmtno5  47481  fmtno4prmfac  47496  fmtno5faclem2  47504  fmtno5faclem3  47505  fmtno5fac  47506  flsqrt5  47518  139prmALT  47520  127prm  47523  mod42tp1mod8  47526  2t6m3t4e0  48192  zlmodzxzequa  48341  zlmodzxzequap  48344