Theorem 6cn 12329

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 12305	. 2 ⊢ 6 = (5 + 1)
2		5cn 12326	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11185	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11239	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2830	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125  1c1 11128   + caddc 11130  5c5 12296  6c6 12297

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185  ax-addcl 11187

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809  df-2 12301  df-3 12302  df-4 12303  df-5 12304  df-6 12305

This theorem is referenced by:  7cn  12332  7m1e6  12370  6p2e8  12397  6p3e9  12398  halfpm6th  12461  6p4e10  12778  6t2e12  12810  6t3e18  12811  6t5e30  12813  5recm6rec  12849  bpoly2  16071  bpoly3  16072  bpoly4  16073  efi4p  16153  ef01bndlem  16200  cos01bnd  16202  3lcm2e6woprm  16632  6lcm4e12  16633  2exp8  17106  2exp11  17107  2exp16  17108  19prm  17135  83prm  17140  163prm  17142  317prm  17143  631prm  17144  1259lem1  17148  1259lem2  17149  1259lem3  17150  1259lem4  17151  1259lem5  17152  2503lem1  17154  2503lem2  17155  2503lem3  17156  2503prm  17157  4001lem1  17158  4001lem2  17159  4001lem4  17161  4001prm  17162  sincos6thpi  26475  sincos3rdpi  26476  1cubrlem  26801  log2ublem3  26908  log2ub  26909  basellem5  27045  basellem8  27048  ppiub  27165  bclbnd  27241  bposlem8  27252  bposlem9  27253  2lgslem3d  27360  2lgsoddprmlem3d  27374  ex-exp  30377  ex-bc  30379  ex-gcd  30384  ex-lcm  30385  hgt750lemd  34626  hgt750lem2  34630  problem5  35637  60gcd6e6  41963  60lcm7e420  41969  3exp7  42012  3lexlogpow5ineq1  42013  3lexlogpow5ineq5  42019  aks4d1p1p5  42034  aks4d1p1  42035  sq6  42291  lhe4.4ex1a  44301  wallispi2lem2  46049  fmtno5lem1  47515  fmtno5lem4  47518  fmtno5  47519  fmtno4prmfac  47534  fmtno5faclem2  47542  fmtno5faclem3  47543  fmtno5fac  47544  flsqrt5  47556  139prmALT  47558  127prm  47561  mod42tp1mod8  47564  2t6m3t4e0  48271  zlmodzxzequa  48420  zlmodzxzequap  48423