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 11118	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11170	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2828	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2106  (class class class)co 7362  ℂcc 11058  1c1 11061   + caddc 11063  5c5 12220  6c6 12221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-1cn 11118  ax-addcl 11120

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-clel 2809  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229

This theorem is referenced by:  7cn  12256  7m1e6  12294  6p2e8  12321  6p3e9  12322  halfpm6th  12383  6p4e10  12699  6t2e12  12731  6t3e18  12732  6t5e30  12734  5recm6rec  12771  bpoly2  15951  bpoly3  15952  bpoly4  15953  efi4p  16030  ef01bndlem  16077  cos01bnd  16079  3lcm2e6woprm  16502  6lcm4e12  16503  2exp8  16972  2exp11  16973  2exp16  16974  19prm  17001  83prm  17006  163prm  17008  317prm  17009  631prm  17010  1259lem1  17014  1259lem2  17015  1259lem3  17016  1259lem4  17017  1259lem5  17018  2503lem1  17020  2503lem2  17021  2503lem3  17022  2503prm  17023  4001lem1  17024  4001lem2  17025  4001lem4  17027  4001prm  17028  sincos6thpi  25909  sincos3rdpi  25910  1cubrlem  26228  log2ublem3  26335  log2ub  26336  basellem5  26471  basellem8  26474  ppiub  26589  bclbnd  26665  bposlem8  26676  bposlem9  26677  2lgslem3d  26784  2lgsoddprmlem3d  26798  ex-exp  29457  ex-bc  29459  ex-gcd  29464  ex-lcm  29465  hgt750lemd  33350  hgt750lem2  33354  problem5  34344  60gcd6e6  40534  60lcm7e420  40540  3exp7  40583  3lexlogpow5ineq1  40584  3lexlogpow5ineq5  40590  aks4d1p1p5  40605  aks4d1p1  40606  lhe4.4ex1a  42731  wallispi2lem2  44433  fmtno5lem1  45865  fmtno5lem4  45868  fmtno5  45869  fmtno4prmfac  45884  fmtno5faclem2  45892  fmtno5faclem3  45893  fmtno5fac  45894  flsqrt5  45906  139prmALT  45908  127prm  45911  mod42tp1mod8  45914  2t6m3t4e0  46544  zlmodzxzequa  46697  zlmodzxzequap  46700