Theorem 6cn 11886

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 11862	. 2 ⊢ 6 = (5 + 1)
2		5cn 11883	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 10752	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10804	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2827	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2112  (class class class)co 7191  ℂcc 10692  1c1 10695   + caddc 10697  5c5 11853  6c6 11854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-1cn 10752  ax-addcl 10754

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-clel 2809  df-2 11858  df-3 11859  df-4 11860  df-5 11861  df-6 11862

This theorem is referenced by:  7cn  11889  7m1e6  11927  6p2e8  11954  6p3e9  11955  halfpm6th  12016  6p4e10  12330  6t2e12  12362  6t3e18  12363  6t5e30  12365  5recm6rec  12402  bpoly2  15582  bpoly3  15583  bpoly4  15584  efi4p  15661  ef01bndlem  15708  cos01bnd  15710  3lcm2e6woprm  16135  6lcm4e12  16136  2exp8  16605  2exp11  16606  2exp16  16607  19prm  16634  83prm  16639  163prm  16641  317prm  16642  631prm  16643  1259lem1  16647  1259lem2  16648  1259lem3  16649  1259lem4  16650  1259lem5  16651  2503lem1  16653  2503lem2  16654  2503lem3  16655  2503prm  16656  4001lem1  16657  4001lem2  16658  4001lem4  16660  4001prm  16661  sincos6thpi  25359  sincos3rdpi  25360  1cubrlem  25678  log2ublem3  25785  log2ub  25786  basellem5  25921  basellem8  25924  ppiub  26039  bclbnd  26115  bposlem8  26126  bposlem9  26127  2lgslem3d  26234  2lgsoddprmlem3d  26248  ex-exp  28487  ex-bc  28489  ex-gcd  28494  ex-lcm  28495  hgt750lemd  32294  hgt750lem2  32298  problem5  33294  60gcd6e6  39695  60lcm7e420  39701  3exp7  39744  3lexlogpow5ineq1  39745  3lexlogpow5ineq5  39751  aks4d1p1p5  39765  aks4d1p1  39766  lhe4.4ex1a  41561  wallispi2lem2  43231  fmtno5lem1  44621  fmtno5lem4  44624  fmtno5  44625  fmtno4prmfac  44640  fmtno5faclem2  44648  fmtno5faclem3  44649  fmtno5fac  44650  flsqrt5  44662  139prmALT  44664  127prm  44667  mod42tp1mod8  44670  2t6m3t4e0  45300  zlmodzxzequa  45453  zlmodzxzequap  45456