Theorem 6cn 12248

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 12224	. 2 ⊢ 6 = (5 + 1)
2		5cn 12245	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11150	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2833	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036  1c1 11039   + caddc 11041  5c5 12215  6c6 12216

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 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-2 12220  df-3 12221  df-4 12222  df-5 12223  df-6 12224

This theorem is referenced by:  7cn  12251  7m1e6  12284  6p2e8  12311  6p3e9  12312  halfpm6th  12375  6p4e10  12691  6t2e12  12723  6t3e18  12724  6t5e30  12726  5recm6rec  12762  bpoly2  15992  bpoly3  15993  bpoly4  15994  efi4p  16074  ef01bndlem  16121  cos01bnd  16123  3lcm2e6woprm  16554  6lcm4e12  16555  2exp8  17028  2exp11  17029  2exp16  17030  19prm  17057  83prm  17062  163prm  17064  317prm  17065  631prm  17066  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  2503lem1  17076  2503lem2  17077  2503lem3  17078  2503prm  17079  4001lem1  17080  4001lem2  17081  4001lem4  17083  4001prm  17084  sincos6thpi  26496  sincos3rdpi  26497  1cubrlem  26822  log2ublem3  26929  log2ub  26930  basellem5  27066  basellem8  27069  ppiub  27186  bclbnd  27262  bposlem8  27273  bposlem9  27274  2lgslem3d  27381  2lgsoddprmlem3d  27395  ex-exp  30541  ex-bc  30543  ex-gcd  30548  ex-lcm  30549  hgt750lemd  34830  hgt750lem2  34834  problem5  35889  60gcd6e6  42378  60lcm7e420  42384  3exp7  42427  3lexlogpow5ineq1  42428  3lexlogpow5ineq5  42434  aks4d1p1p5  42449  aks4d1p1  42450  sq6  42669  lhe4.4ex1a  44689  wallispi2lem2  46434  fmtno5lem1  47917  fmtno5lem4  47920  fmtno5  47921  fmtno4prmfac  47936  fmtno5faclem2  47944  fmtno5faclem3  47945  fmtno5fac  47946  flsqrt5  47958  139prmALT  47960  127prm  47963  mod42tp1mod8  47966  2t6m3t4e0  48712  zlmodzxzequa  48860  zlmodzxzequap  48863