Theorem 6cn 11582

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 11558	. 2 ⊢ 6 = (5 + 1)
2		5cn 11579	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 10448	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10500	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2881	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2083  (class class class)co 7023  ℂcc 10388  1c1 10391   + caddc 10393  5c5 11549  6c6 11550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-ext 2771  ax-1cn 10448  ax-addcl 10450

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-cleq 2790  df-clel 2865  df-2 11554  df-3 11555  df-4 11556  df-5 11557  df-6 11558

This theorem is referenced by:  7cn  11585  7m1e6  11623  6p2e8  11650  6p3e9  11651  halfpm6th  11712  6p4e10  12024  6t2e12  12056  6t3e18  12057  6t5e30  12059  5recm6rec  12096  bpoly2  15248  bpoly3  15249  bpoly4  15250  efi4p  15327  ef01bndlem  15374  cos01bnd  15376  3lcm2e6woprm  15792  6lcm4e12  15793  2exp8  16256  2exp16  16257  19prm  16284  83prm  16289  163prm  16291  317prm  16292  631prm  16293  1259lem1  16297  1259lem2  16298  1259lem3  16299  1259lem4  16300  1259lem5  16301  2503lem1  16303  2503lem2  16304  2503lem3  16305  2503prm  16306  4001lem1  16307  4001lem2  16308  4001lem4  16310  4001prm  16311  sincos6thpi  24788  sincos3rdpi  24789  1cubrlem  25104  log2ublem3  25212  log2ub  25213  basellem5  25348  basellem8  25351  ppiub  25466  bclbnd  25542  bposlem8  25553  bposlem9  25554  2lgslem3d  25661  2lgsoddprmlem3d  25675  ex-exp  27917  ex-bc  27919  ex-gcd  27924  ex-lcm  27925  hgt750lemd  31532  hgt750lem2  31536  problem5  32522  lhe4.4ex1a  40220  wallispi2lem2  41921  fmtno5lem1  43219  fmtno5lem4  43222  fmtno5  43223  fmtno4prmfac  43238  fmtno5faclem2  43246  fmtno5faclem3  43247  fmtno5fac  43248  flsqrt5  43261  139prmALT  43263  127prm  43267  2exp11  43269  mod42tp1mod8  43271  2t6m3t4e0  43896  zlmodzxzequa  44053  zlmodzxzequap  44056