Theorem 6cn 12303

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 12279	. 2 ⊢ 6 = (5 + 1)
2		5cn 12300	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11168	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11220	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2830	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108  1c1 11111   + caddc 11113  5c5 12270  6c6 12271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11168  ax-addcl 11170

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279

This theorem is referenced by:  7cn  12306  7m1e6  12344  6p2e8  12371  6p3e9  12372  halfpm6th  12433  6p4e10  12749  6t2e12  12781  6t3e18  12782  6t5e30  12784  5recm6rec  12821  bpoly2  16001  bpoly3  16002  bpoly4  16003  efi4p  16080  ef01bndlem  16127  cos01bnd  16129  3lcm2e6woprm  16552  6lcm4e12  16553  2exp8  17022  2exp11  17023  2exp16  17024  19prm  17051  83prm  17056  163prm  17058  317prm  17059  631prm  17060  1259lem1  17064  1259lem2  17065  1259lem3  17066  1259lem4  17067  1259lem5  17068  2503lem1  17070  2503lem2  17071  2503lem3  17072  2503prm  17073  4001lem1  17074  4001lem2  17075  4001lem4  17077  4001prm  17078  sincos6thpi  26025  sincos3rdpi  26026  1cubrlem  26346  log2ublem3  26453  log2ub  26454  basellem5  26589  basellem8  26592  ppiub  26707  bclbnd  26783  bposlem8  26794  bposlem9  26795  2lgslem3d  26902  2lgsoddprmlem3d  26916  ex-exp  29703  ex-bc  29705  ex-gcd  29710  ex-lcm  29711  hgt750lemd  33660  hgt750lem2  33664  problem5  34654  60gcd6e6  40869  60lcm7e420  40875  3exp7  40918  3lexlogpow5ineq1  40919  3lexlogpow5ineq5  40925  aks4d1p1p5  40940  aks4d1p1  40941  lhe4.4ex1a  43088  wallispi2lem2  44788  fmtno5lem1  46221  fmtno5lem4  46224  fmtno5  46225  fmtno4prmfac  46240  fmtno5faclem2  46248  fmtno5faclem3  46249  fmtno5fac  46250  flsqrt5  46262  139prmALT  46264  127prm  46267  mod42tp1mod8  46270  2t6m3t4e0  47024  zlmodzxzequa  47177  zlmodzxzequap  47180