Theorem 6cn 12266

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 12242	. 2 ⊢ 6 = (5 + 1)
2		5cn 12263	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11090	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11145	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2833	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7361  ℂcc 11030  1c1 11033   + caddc 11035  5c5 12233  6c6 12234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11090  ax-addcl 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-2 12238  df-3 12239  df-4 12240  df-5 12241  df-6 12242

This theorem is referenced by:  7cn  12269  7m1e6  12302  6p2e8  12329  6p3e9  12330  halfpm6th  12393  6p4e10  12710  6t2e12  12742  6t3e18  12743  6t5e30  12745  5recm6rec  12781  bpoly2  16016  bpoly3  16017  bpoly4  16018  efi4p  16098  ef01bndlem  16145  cos01bnd  16147  3lcm2e6woprm  16578  6lcm4e12  16579  2exp8  17053  2exp11  17054  2exp16  17055  19prm  17082  83prm  17087  163prm  17089  317prm  17090  631prm  17091  1259lem1  17095  1259lem2  17096  1259lem3  17097  1259lem4  17098  1259lem5  17099  2503lem1  17101  2503lem2  17102  2503lem3  17103  2503prm  17104  4001lem1  17105  4001lem2  17106  4001lem4  17108  4001prm  17109  sincos6thpi  26496  sincos3rdpi  26497  1cubrlem  26821  log2ublem3  26928  log2ub  26929  basellem5  27065  basellem8  27068  ppiub  27184  bclbnd  27260  bposlem8  27271  bposlem9  27272  2lgslem3d  27379  2lgsoddprmlem3d  27393  ex-exp  30538  ex-bc  30540  ex-gcd  30545  ex-lcm  30546  hgt750lemd  34811  hgt750lem2  34815  problem5  35870  60gcd6e6  42460  60lcm7e420  42466  3exp7  42509  3lexlogpow5ineq1  42510  3lexlogpow5ineq5  42516  aks4d1p1p5  42531  aks4d1p1  42532  sq6  42744  lhe4.4ex1a  44777  wallispi2lem2  46521  sin5tlem1  47340  sin5tlem4  47343  sin5tlem5  47344  fmtno5lem1  48031  fmtno5lem4  48034  fmtno5  48035  fmtno4prmfac  48050  fmtno5faclem2  48058  fmtno5faclem3  48059  fmtno5fac  48060  flsqrt5  48072  139prmALT  48074  127prm  48077  mod42tp1mod8  48080  2t6m3t4e0  48839  zlmodzxzequa  48987  zlmodzxzequap  48990