Theorem 6cn 12219

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 12195	. 2 ⊢ 6 = (5 + 1)
2		5cn 12216	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11067	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11121	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007  1c1 11010   + caddc 11012  5c5 12186  6c6 12187

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 2701  ax-1cn 11067  ax-addcl 11069

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12191  df-3 12192  df-4 12193  df-5 12194  df-6 12195

This theorem is referenced by:  7cn  12222  7m1e6  12255  6p2e8  12282  6p3e9  12283  halfpm6th  12346  6p4e10  12663  6t2e12  12695  6t3e18  12696  6t5e30  12698  5recm6rec  12734  bpoly2  15964  bpoly3  15965  bpoly4  15966  efi4p  16046  ef01bndlem  16093  cos01bnd  16095  3lcm2e6woprm  16526  6lcm4e12  16527  2exp8  17000  2exp11  17001  2exp16  17002  19prm  17029  83prm  17034  163prm  17036  317prm  17037  631prm  17038  1259lem1  17042  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem4  17055  4001prm  17056  sincos6thpi  26423  sincos3rdpi  26424  1cubrlem  26749  log2ublem3  26856  log2ub  26857  basellem5  26993  basellem8  26996  ppiub  27113  bclbnd  27189  bposlem8  27200  bposlem9  27201  2lgslem3d  27308  2lgsoddprmlem3d  27322  ex-exp  30394  ex-bc  30396  ex-gcd  30401  ex-lcm  30402  hgt750lemd  34616  hgt750lem2  34620  problem5  35646  60gcd6e6  41981  60lcm7e420  41987  3exp7  42030  3lexlogpow5ineq1  42031  3lexlogpow5ineq5  42037  aks4d1p1p5  42052  aks4d1p1  42053  sq6  42272  lhe4.4ex1a  44306  wallispi2lem2  46057  fmtno5lem1  47541  fmtno5lem4  47544  fmtno5  47545  fmtno4prmfac  47560  fmtno5faclem2  47568  fmtno5faclem3  47569  fmtno5fac  47570  flsqrt5  47582  139prmALT  47584  127prm  47587  mod42tp1mod8  47590  2t6m3t4e0  48336  zlmodzxzequa  48485  zlmodzxzequap  48488