Theorem 6cn 12332

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 12307	. 2 ⊢ 6 = (5 + 1)
2		5cn 12329	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11158	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11215	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2865	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2149  (class class class)co 7411  ℂcc 11098  1c1 11101   + caddc 11103  5c5 12298  6c6 12299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11158  ax-addcl 11160

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844  df-2 12303  df-3 12304  df-4 12305  df-5 12306  df-6 12307

This theorem is referenced by:  7cn  12335  7m1e6  12372  6p2e8  12399  6p3e9  12400  halfpm6th  12466  6p4e10  12788  6t2e12  12820  6t3e18  12821  6t5e30  12823  5recm6rec  12861  bpoly2  16111  bpoly3  16112  bpoly4  16113  efi4p  16193  ef01bndlem  16240  cos01bnd  16242  3lcm2e6woprm  16673  6lcm4e12  16674  2exp8  17148  2exp11  17149  2exp16  17150  19prm  17178  83prm  17183  163prm  17185  317prm  17186  631prm  17187  1259lem1  17191  1259lem2  17192  1259lem3  17193  1259lem4  17194  1259lem5  17195  2503lem1  17197  2503lem2  17198  2503lem3  17199  2503prm  17200  4001lem1  17201  4001lem2  17202  4001lem4  17204  4001prm  17205  sincos6thpi  26647  sincos3rdpi  26648  1cubrlem  26972  log2ublem3  27079  log2ub  27080  basellem5  27215  basellem8  27218  ppiub  27334  bclbnd  27410  bposlem8  27421  bposlem9  27422  2lgslem3d  27529  2lgsoddprmlem3d  27543  ex-exp  30742  ex-bc  30744  ex-gcd  30749  ex-lcm  30750  hgt750lemd  34980  hgt750lem2  34984  problem5  36094  60gcd6e6  42695  60lcm7e420  42701  3exp7  42744  3lexlogpow5ineq1  42745  3lexlogpow5ineq5  42751  aks4d1p1p5  42766  aks4d1p1  42767  25or6to4  42897  sq6  42980  lhe4.4ex1a  44965  wallispi2lem2  46712  sin5tlem1  47533  sin5tlem4  47536  sin5tlem5  47537  fmtno5lem1  48228  fmtno5lem4  48231  fmtno5  48232  fmtno4prmfac  48247  fmtno5faclem2  48255  fmtno5faclem3  48256  fmtno5fac  48257  flsqrt5  48269  139prmALT  48271  127prm  48274  mod42tp1mod8  48277  2t6m3t4e0  49047  zlmodzxzequa  49195  zlmodzxzequap  49198