Theorem 6cn 12384

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 12360	. 2 ⊢ 6 = (5 + 1)
2		5cn 12381	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11242	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11296	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2840	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182  1c1 11185   + caddc 11187  5c5 12351  6c6 12352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-addcl 11244

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360

This theorem is referenced by:  7cn  12387  7m1e6  12425  6p2e8  12452  6p3e9  12453  halfpm6th  12514  6p4e10  12830  6t2e12  12862  6t3e18  12863  6t5e30  12865  5recm6rec  12902  bpoly2  16105  bpoly3  16106  bpoly4  16107  efi4p  16185  ef01bndlem  16232  cos01bnd  16234  3lcm2e6woprm  16662  6lcm4e12  16663  2exp8  17136  2exp11  17137  2exp16  17138  19prm  17165  83prm  17170  163prm  17172  317prm  17173  631prm  17174  1259lem1  17178  1259lem2  17179  1259lem3  17180  1259lem4  17181  1259lem5  17182  2503lem1  17184  2503lem2  17185  2503lem3  17186  2503prm  17187  4001lem1  17188  4001lem2  17189  4001lem4  17191  4001prm  17192  sincos6thpi  26576  sincos3rdpi  26577  1cubrlem  26902  log2ublem3  27009  log2ub  27010  basellem5  27146  basellem8  27149  ppiub  27266  bclbnd  27342  bposlem8  27353  bposlem9  27354  2lgslem3d  27461  2lgsoddprmlem3d  27475  ex-exp  30482  ex-bc  30484  ex-gcd  30489  ex-lcm  30490  hgt750lemd  34625  hgt750lem2  34629  problem5  35637  60gcd6e6  41961  60lcm7e420  41967  3exp7  42010  3lexlogpow5ineq1  42011  3lexlogpow5ineq5  42017  aks4d1p1p5  42032  aks4d1p1  42033  sq6  42283  lhe4.4ex1a  44298  wallispi2lem2  45993  fmtno5lem1  47427  fmtno5lem4  47430  fmtno5  47431  fmtno4prmfac  47446  fmtno5faclem2  47454  fmtno5faclem3  47455  fmtno5fac  47456  flsqrt5  47468  139prmALT  47470  127prm  47473  mod42tp1mod8  47476  2t6m3t4e0  48073  zlmodzxzequa  48225  zlmodzxzequap  48228