Theorem 6cn 12284

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 12260	. 2 ⊢ 6 = (5 + 1)
2		5cn 12281	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11133	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11187	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2825	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073  1c1 11076   + caddc 11078  5c5 12251  6c6 12252

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 11133  ax-addcl 11135

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804  df-2 12256  df-3 12257  df-4 12258  df-5 12259  df-6 12260

This theorem is referenced by:  7cn  12287  7m1e6  12320  6p2e8  12347  6p3e9  12348  halfpm6th  12411  6p4e10  12728  6t2e12  12760  6t3e18  12761  6t5e30  12763  5recm6rec  12799  bpoly2  16030  bpoly3  16031  bpoly4  16032  efi4p  16112  ef01bndlem  16159  cos01bnd  16161  3lcm2e6woprm  16592  6lcm4e12  16593  2exp8  17066  2exp11  17067  2exp16  17068  19prm  17095  83prm  17100  163prm  17102  317prm  17103  631prm  17104  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  2503lem1  17114  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem4  17121  4001prm  17122  sincos6thpi  26432  sincos3rdpi  26433  1cubrlem  26758  log2ublem3  26865  log2ub  26866  basellem5  27002  basellem8  27005  ppiub  27122  bclbnd  27198  bposlem8  27209  bposlem9  27210  2lgslem3d  27317  2lgsoddprmlem3d  27331  ex-exp  30386  ex-bc  30388  ex-gcd  30393  ex-lcm  30394  hgt750lemd  34646  hgt750lem2  34650  problem5  35663  60gcd6e6  41999  60lcm7e420  42005  3exp7  42048  3lexlogpow5ineq1  42049  3lexlogpow5ineq5  42055  aks4d1p1p5  42070  aks4d1p1  42071  sq6  42290  lhe4.4ex1a  44325  wallispi2lem2  46077  fmtno5lem1  47558  fmtno5lem4  47561  fmtno5  47562  fmtno4prmfac  47577  fmtno5faclem2  47585  fmtno5faclem3  47586  fmtno5fac  47587  flsqrt5  47599  139prmALT  47601  127prm  47604  mod42tp1mod8  47607  2t6m3t4e0  48340  zlmodzxzequa  48489  zlmodzxzequap  48492