Theorem 6cn 12359

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 12334	. 2 ⊢ 6 = (5 + 1)
2		5cn 12356	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11185	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11242	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2856	1 ⊢ 6 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7414  ℂcc 11125  1c1 11128   + caddc 11130  5c5 12325  6c6 12326

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 2147  ax-9 2155  ax-ext 2732  ax-1cn 11185  ax-addcl 11187

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334

This theorem is used by:  7cn  12362  7m1e6  12399  6p2e8  12426  6p3e9  12427  8th4div3  12491  halfpm6th  12493  6p4e10  12816  6t2e12  12848  6t3e18  12849  6t5e30  12851  5recm6rec  12889  bpoly2  16146  bpoly3  16147  bpoly4  16148  efi4p  16228  ef01bndlem  16275  cos01bnd  16277  3lcm2e6woprm  16708  6lcm4e12  16709  2exp8  17183  2exp11  17184  2exp16  17185  19prm  17213  83prm  17218  163prm  17220  317prm  17221  631prm  17222  1259lem1  17226  1259lem2  17227  1259lem3  17228  1259lem4  17229  1259lem5  17230  2503lem1  17232  2503lem2  17233  2503lem3  17234  2503prm  17235  4001lem1  17236  4001lem2  17237  4001lem4  17239  4001prm  17240  sincos6thpi  26756  sincos3rdpi  26757  1cubrlem  27081  log2ublem3  27188  log2ub  27189  basellem5  27324  basellem8  27327  ppiub  27443  bclbnd  27519  bposlem8  27530  bposlem9  27531  2lgslem3d  27638  2lgsoddprmlem3d  27652  ex-exp  30933  ex-bc  30935  ex-gcd  30940  ex-lcm  30941  hgt750lemd  35159  hgt750lem2  35163  problem5  36251  60gcd6e6  42873  60lcm7e420  42879  3exp7  42922  3lexlogpow5ineq1  42923  3lexlogpow5ineq5  42929  aks4d1p1p5  42944  aks4d1p1  42945  25or6to4  43075  1p7e8  43133  sq6  43173  lhe4.4ex1a  45156  wallispi2lem2  46903  sin5tlem1  47740  sin5tlem4  47743  sin5tlem5  47744  fmtno5lem1  48459  fmtno5lem4  48462  fmtno5  48463  fmtno4prmfac  48478  fmtno5faclem2  48486  fmtno5faclem3  48487  fmtno5fac  48488  flsqrt5  48500  139prmALT  48502  127prm  48505  mod42tp1mod8  48508  2t6m3t4e0  49281  zlmodzxzequa  49429  zlmodzxzequap  49432