Theorem 6cn 12355

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 12331	. 2 ⊢ 6 = (5 + 1)
2		5cn 12352	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11216	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11270	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2822	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2099  (class class class)co 7424  ℂcc 11156  1c1 11159   + caddc 11161  5c5 12322  6c6 12323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-1cn 11216  ax-addcl 11218

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-clel 2803  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331

This theorem is referenced by:  7cn  12358  7m1e6  12396  6p2e8  12423  6p3e9  12424  halfpm6th  12485  6p4e10  12801  6t2e12  12833  6t3e18  12834  6t5e30  12836  5recm6rec  12873  bpoly2  16059  bpoly3  16060  bpoly4  16061  efi4p  16139  ef01bndlem  16186  cos01bnd  16188  3lcm2e6woprm  16616  6lcm4e12  16617  2exp8  17091  2exp11  17092  2exp16  17093  19prm  17120  83prm  17125  163prm  17127  317prm  17128  631prm  17129  1259lem1  17133  1259lem2  17134  1259lem3  17135  1259lem4  17136  1259lem5  17137  2503lem1  17139  2503lem2  17140  2503lem3  17141  2503prm  17142  4001lem1  17143  4001lem2  17144  4001lem4  17146  4001prm  17147  sincos6thpi  26543  sincos3rdpi  26544  1cubrlem  26869  log2ublem3  26976  log2ub  26977  basellem5  27113  basellem8  27116  ppiub  27233  bclbnd  27309  bposlem8  27320  bposlem9  27321  2lgslem3d  27428  2lgsoddprmlem3d  27442  ex-exp  30383  ex-bc  30385  ex-gcd  30390  ex-lcm  30391  hgt750lemd  34494  hgt750lem2  34498  problem5  35497  60gcd6e6  41703  60lcm7e420  41709  3exp7  41752  3lexlogpow5ineq1  41753  3lexlogpow5ineq5  41759  aks4d1p1p5  41774  aks4d1p1  41775  lhe4.4ex1a  44003  wallispi2lem2  45693  fmtno5lem1  47125  fmtno5lem4  47128  fmtno5  47129  fmtno4prmfac  47144  fmtno5faclem2  47152  fmtno5faclem3  47153  fmtno5fac  47154  flsqrt5  47166  139prmALT  47168  127prm  47171  mod42tp1mod8  47174  2t6m3t4e0  47727  zlmodzxzequa  47879  zlmodzxzequap  47882