Theorem 6cn 12236

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 12212	. 2 ⊢ 6 = (5 + 1)
2		5cn 12233	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11084	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11138	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2832	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024  1c1 11027   + caddc 11029  5c5 12203  6c6 12204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-addcl 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811  df-2 12208  df-3 12209  df-4 12210  df-5 12211  df-6 12212

This theorem is referenced by:  7cn  12239  7m1e6  12272  6p2e8  12299  6p3e9  12300  halfpm6th  12363  6p4e10  12679  6t2e12  12711  6t3e18  12712  6t5e30  12714  5recm6rec  12750  bpoly2  15980  bpoly3  15981  bpoly4  15982  efi4p  16062  ef01bndlem  16109  cos01bnd  16111  3lcm2e6woprm  16542  6lcm4e12  16543  2exp8  17016  2exp11  17017  2exp16  17018  19prm  17045  83prm  17050  163prm  17052  317prm  17053  631prm  17054  1259lem1  17058  1259lem2  17059  1259lem3  17060  1259lem4  17061  1259lem5  17062  2503lem1  17064  2503lem2  17065  2503lem3  17066  2503prm  17067  4001lem1  17068  4001lem2  17069  4001lem4  17071  4001prm  17072  sincos6thpi  26481  sincos3rdpi  26482  1cubrlem  26807  log2ublem3  26914  log2ub  26915  basellem5  27051  basellem8  27054  ppiub  27171  bclbnd  27247  bposlem8  27258  bposlem9  27259  2lgslem3d  27366  2lgsoddprmlem3d  27380  ex-exp  30525  ex-bc  30527  ex-gcd  30532  ex-lcm  30533  hgt750lemd  34805  hgt750lem2  34809  problem5  35863  60gcd6e6  42268  60lcm7e420  42274  3exp7  42317  3lexlogpow5ineq1  42318  3lexlogpow5ineq5  42324  aks4d1p1p5  42339  aks4d1p1  42340  sq6  42560  lhe4.4ex1a  44580  wallispi2lem2  46326  fmtno5lem1  47809  fmtno5lem4  47812  fmtno5  47813  fmtno4prmfac  47828  fmtno5faclem2  47836  fmtno5faclem3  47837  fmtno5fac  47838  flsqrt5  47850  139prmALT  47852  127prm  47855  mod42tp1mod8  47858  2t6m3t4e0  48604  zlmodzxzequa  48752  zlmodzxzequap  48755