Theorem 6cn 12278

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 12254	. 2 ⊢ 6 = (5 + 1)
2		5cn 12275	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11132	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11186	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2825	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7389  ℂcc 11072  1c1 11075   + caddc 11077  5c5 12245  6c6 12246

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 2702  ax-1cn 11132  ax-addcl 11134

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804  df-2 12250  df-3 12251  df-4 12252  df-5 12253  df-6 12254

This theorem is referenced by:  7cn  12281  7m1e6  12319  6p2e8  12346  6p3e9  12347  halfpm6th  12410  6p4e10  12727  6t2e12  12759  6t3e18  12760  6t5e30  12762  5recm6rec  12798  bpoly2  16029  bpoly3  16030  bpoly4  16031  efi4p  16111  ef01bndlem  16158  cos01bnd  16160  3lcm2e6woprm  16591  6lcm4e12  16592  2exp8  17065  2exp11  17066  2exp16  17067  19prm  17094  83prm  17099  163prm  17101  317prm  17102  631prm  17103  1259lem1  17107  1259lem2  17108  1259lem3  17109  1259lem4  17110  1259lem5  17111  2503lem1  17113  2503lem2  17114  2503lem3  17115  2503prm  17116  4001lem1  17117  4001lem2  17118  4001lem4  17120  4001prm  17121  sincos6thpi  26431  sincos3rdpi  26432  1cubrlem  26757  log2ublem3  26864  log2ub  26865  basellem5  27001  basellem8  27004  ppiub  27121  bclbnd  27197  bposlem8  27208  bposlem9  27209  2lgslem3d  27316  2lgsoddprmlem3d  27330  ex-exp  30385  ex-bc  30387  ex-gcd  30392  ex-lcm  30393  hgt750lemd  34645  hgt750lem2  34649  problem5  35656  60gcd6e6  41987  60lcm7e420  41993  3exp7  42036  3lexlogpow5ineq1  42037  3lexlogpow5ineq5  42043  aks4d1p1p5  42058  aks4d1p1  42059  sq6  42278  lhe4.4ex1a  44311  wallispi2lem2  46063  fmtno5lem1  47544  fmtno5lem4  47547  fmtno5  47548  fmtno4prmfac  47563  fmtno5faclem2  47571  fmtno5faclem3  47572  fmtno5fac  47573  flsqrt5  47585  139prmALT  47587  127prm  47590  mod42tp1mod8  47593  2t6m3t4e0  48326  zlmodzxzequa  48475  zlmodzxzequap  48478