Theorem 6cn 12434

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 12409	. 2 ⊢ 6 = (5 + 1)
2		5cn 12431	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11258	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11315	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2857	1 ⊢ 6 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7420  ℂcc 11198  1c1 11201   + caddc 11203  5c5 12400  6c6 12401

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 2733  ax-1cn 11258  ax-addcl 11260

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836  df-2 12405  df-3 12406  df-4 12407  df-5 12408  df-6 12409

This theorem is used by:  7cn  12437  7m1e6  12474  6p2e8  12501  6p3e9  12502  8th4div3  12566  halfpm6th  12568  6p4e10  12891  6t2e12  12923  6t3e18  12924  6t5e30  12926  5recm6rec  12964  bpoly2  16223  bpoly3  16224  bpoly4  16225  efi4p  16305  ef01bndlem  16352  cos01bnd  16354  3lcm2e6woprm  16790  6lcm4e12  16791  2exp8  17266  2exp11  17267  2exp16  17268  19prm  17296  83prm  17301  163prm  17303  317prm  17304  631prm  17305  1259lem1  17309  1259lem2  17310  1259lem3  17311  1259lem4  17312  1259lem5  17313  2503lem1  17315  2503lem2  17316  2503lem3  17317  2503prm  17318  4001lem1  17319  4001lem2  17320  4001lem4  17322  4001prm  17323  sincos6thpi  26844  sincos3rdpi  26845  1cubrlem  27169  log2ublem3  27276  log2ub  27277  basellem5  27412  basellem8  27415  ppiub  27531  bclbnd  27607  bposlem8  27618  bposlem9  27619  2lgslem3d  27726  2lgsoddprmlem3d  27740  ex-exp  31051  ex-bc  31053  ex-gcd  31058  ex-lcm  31059  hgt750lemd  35277  hgt750lem2  35281  problem5  36434  60gcd6e6  43054  60lcm7e420  43060  3exp7  43103  3lexlogpow5ineq1  43104  3lexlogpow5ineq5  43110  aks4d1p1p5  43125  aks4d1p1  43126  25or6to4  43256  1p7e8  43314  sq6  43352  lhe4.4ex1a  45312  wallispi2lem2  47081  sin5tlem1  47918  sin5tlem4  47921  sin5tlem5  47922  fmtno5lem1  48637  fmtno5lem4  48640  fmtno5  48641  fmtno4prmfac  48656  fmtno5faclem2  48664  fmtno5faclem3  48665  fmtno5fac  48666  flsqrt5  48678  139prmALT  48680  127prm  48683  mod42tp1mod8  48686  2t6m3t4e0  49459  zlmodzxzequa  49607  zlmodzxzequap  49610