Theorem 6cn 12327

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 12302	. 2 ⊢ 6 = (5 + 1)
2		5cn 12324	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11153	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11210	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2859	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093  1c1 11096   + caddc 11098  5c5 12293  6c6 12294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-addcl 11155

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838  df-2 12298  df-3 12299  df-4 12300  df-5 12301  df-6 12302

This theorem is referenced by:  7cn  12330  7m1e6  12367  6p2e8  12394  6p3e9  12395  8th4div3  12459  halfpm6th  12461  6p4e10  12783  6t2e12  12815  6t3e18  12816  6t5e30  12818  5recm6rec  12856  bpoly2  16106  bpoly3  16107  bpoly4  16108  efi4p  16188  ef01bndlem  16235  cos01bnd  16237  3lcm2e6woprm  16668  6lcm4e12  16669  2exp8  17143  2exp11  17144  2exp16  17145  19prm  17173  83prm  17178  163prm  17180  317prm  17181  631prm  17182  1259lem1  17186  1259lem2  17187  1259lem3  17188  1259lem4  17189  1259lem5  17190  2503lem1  17192  2503lem2  17193  2503lem3  17194  2503prm  17195  4001lem1  17196  4001lem2  17197  4001lem4  17199  4001prm  17200  sincos6thpi  26681  sincos3rdpi  26682  1cubrlem  27006  log2ublem3  27113  log2ub  27114  basellem5  27249  basellem8  27252  ppiub  27368  bclbnd  27444  bposlem8  27455  bposlem9  27456  2lgslem3d  27563  2lgsoddprmlem3d  27577  ex-exp  30801  ex-bc  30803  ex-gcd  30808  ex-lcm  30809  hgt750lemd  35035  hgt750lem2  35039  problem5  36161  60gcd6e6  42791  60lcm7e420  42797  3exp7  42840  3lexlogpow5ineq1  42841  3lexlogpow5ineq5  42847  aks4d1p1p5  42862  aks4d1p1  42863  25or6to4  42993  sq6  43076  lhe4.4ex1a  45059  wallispi2lem2  46806  sin5tlem1  47630  sin5tlem4  47633  sin5tlem5  47634  fmtno5lem1  48325  fmtno5lem4  48328  fmtno5  48329  fmtno4prmfac  48344  fmtno5faclem2  48352  fmtno5faclem3  48353  fmtno5fac  48354  flsqrt5  48366  139prmALT  48368  127prm  48371  mod42tp1mod8  48374  2t6m3t4e0  49148  zlmodzxzequa  49296  zlmodzxzequap  49299