Theorem 6cn 12253

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 12229	. 2 ⊢ 6 = (5 + 1)
2		5cn 12250	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11102	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11156	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042  1c1 11045   + caddc 11047  5c5 12220  6c6 12221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11102  ax-addcl 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229

This theorem is referenced by:  7cn  12256  7m1e6  12289  6p2e8  12316  6p3e9  12317  halfpm6th  12380  6p4e10  12697  6t2e12  12729  6t3e18  12730  6t5e30  12732  5recm6rec  12768  bpoly2  15999  bpoly3  16000  bpoly4  16001  efi4p  16081  ef01bndlem  16128  cos01bnd  16130  3lcm2e6woprm  16561  6lcm4e12  16562  2exp8  17035  2exp11  17036  2exp16  17037  19prm  17064  83prm  17069  163prm  17071  317prm  17072  631prm  17073  1259lem1  17077  1259lem2  17078  1259lem3  17079  1259lem4  17080  1259lem5  17081  2503lem1  17083  2503lem2  17084  2503lem3  17085  2503prm  17086  4001lem1  17087  4001lem2  17088  4001lem4  17090  4001prm  17091  sincos6thpi  26458  sincos3rdpi  26459  1cubrlem  26784  log2ublem3  26891  log2ub  26892  basellem5  27028  basellem8  27031  ppiub  27148  bclbnd  27224  bposlem8  27235  bposlem9  27236  2lgslem3d  27343  2lgsoddprmlem3d  27357  ex-exp  30429  ex-bc  30431  ex-gcd  30436  ex-lcm  30437  hgt750lemd  34632  hgt750lem2  34636  problem5  35649  60gcd6e6  41985  60lcm7e420  41991  3exp7  42034  3lexlogpow5ineq1  42035  3lexlogpow5ineq5  42041  aks4d1p1p5  42056  aks4d1p1  42057  sq6  42276  lhe4.4ex1a  44311  wallispi2lem2  46063  fmtno5lem1  47547  fmtno5lem4  47550  fmtno5  47551  fmtno4prmfac  47566  fmtno5faclem2  47574  fmtno5faclem3  47575  fmtno5fac  47576  flsqrt5  47588  139prmALT  47590  127prm  47593  mod42tp1mod8  47596  2t6m3t4e0  48329  zlmodzxzequa  48478  zlmodzxzequap  48481