Theorem 6cn 12349

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 12324	. 2 ⊢ 6 = (5 + 1)
2		5cn 12346	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11175	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11232	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2861	1 ⊢ 6 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7419  ℂcc 11115  1c1 11118   + caddc 11120  5c5 12315  6c6 12316

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-1cn 11175  ax-addcl 11177

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840  df-2 12320  df-3 12321  df-4 12322  df-5 12323  df-6 12324

This theorem is used by:  7cn  12352  7m1e6  12389  6p2e8  12416  6p3e9  12417  8th4div3  12481  halfpm6th  12483  6p4e10  12806  6t2e12  12838  6t3e18  12839  6t5e30  12841  5recm6rec  12879  bpoly2  16135  bpoly3  16136  bpoly4  16137  efi4p  16217  ef01bndlem  16264  cos01bnd  16266  3lcm2e6woprm  16697  6lcm4e12  16698  2exp8  17172  2exp11  17173  2exp16  17174  19prm  17202  83prm  17207  163prm  17209  317prm  17210  631prm  17211  1259lem1  17215  1259lem2  17216  1259lem3  17217  1259lem4  17218  1259lem5  17219  2503lem1  17221  2503lem2  17222  2503lem3  17223  2503prm  17224  4001lem1  17225  4001lem2  17226  4001lem4  17228  4001prm  17229  sincos6thpi  26734  sincos3rdpi  26735  1cubrlem  27059  log2ublem3  27166  log2ub  27167  basellem5  27302  basellem8  27305  ppiub  27421  bclbnd  27497  bposlem8  27508  bposlem9  27509  2lgslem3d  27616  2lgsoddprmlem3d  27630  ex-exp  30874  ex-bc  30876  ex-gcd  30881  ex-lcm  30882  hgt750lemd  35102  hgt750lem2  35106  problem5  36200  60gcd6e6  42831  60lcm7e420  42837  3exp7  42880  3lexlogpow5ineq1  42881  3lexlogpow5ineq5  42887  aks4d1p1p5  42902  aks4d1p1  42903  25or6to4  43033  sq6  43116  lhe4.4ex1a  45099  wallispi2lem2  46846  sin5tlem1  47670  sin5tlem4  47673  sin5tlem5  47674  fmtno5lem1  48365  fmtno5lem4  48368  fmtno5  48369  fmtno4prmfac  48384  fmtno5faclem2  48392  fmtno5faclem3  48393  fmtno5fac  48394  flsqrt5  48406  139prmALT  48408  127prm  48411  mod42tp1mod8  48414  2t6m3t4e0  49187  zlmodzxzequa  49335  zlmodzxzequap  49338