Theorem 6cn 11731

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 11707	. 2 ⊢ 6 = (5 + 1)
2		5cn 11728	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 10597	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10649	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2911	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7158  ℂcc 10537  1c1 10540   + caddc 10542  5c5 11698  6c6 11699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795  ax-1cn 10597  ax-addcl 10599

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895  df-2 11703  df-3 11704  df-4 11705  df-5 11706  df-6 11707

This theorem is referenced by:  7cn  11734  7m1e6  11772  6p2e8  11799  6p3e9  11800  halfpm6th  11861  6p4e10  12173  6t2e12  12205  6t3e18  12206  6t5e30  12208  5recm6rec  12245  bpoly2  15413  bpoly3  15414  bpoly4  15415  efi4p  15492  ef01bndlem  15539  cos01bnd  15541  3lcm2e6woprm  15961  6lcm4e12  15962  2exp8  16425  2exp16  16426  19prm  16453  83prm  16458  163prm  16460  317prm  16461  631prm  16462  1259lem1  16466  1259lem2  16467  1259lem3  16468  1259lem4  16469  1259lem5  16470  2503lem1  16472  2503lem2  16473  2503lem3  16474  2503prm  16475  4001lem1  16476  4001lem2  16477  4001lem4  16479  4001prm  16480  sincos6thpi  25103  sincos3rdpi  25104  1cubrlem  25421  log2ublem3  25528  log2ub  25529  basellem5  25664  basellem8  25667  ppiub  25782  bclbnd  25858  bposlem8  25869  bposlem9  25870  2lgslem3d  25977  2lgsoddprmlem3d  25991  ex-exp  28231  ex-bc  28233  ex-gcd  28238  ex-lcm  28239  hgt750lemd  31921  hgt750lem2  31925  problem5  32914  lhe4.4ex1a  40668  wallispi2lem2  42364  fmtno5lem1  43722  fmtno5lem4  43725  fmtno5  43726  fmtno4prmfac  43741  fmtno5faclem2  43749  fmtno5faclem3  43750  fmtno5fac  43751  flsqrt5  43764  139prmALT  43766  127prm  43770  2exp11  43772  mod42tp1mod8  43774  2t6m3t4e0  44403  zlmodzxzequa  44558  zlmodzxzequap  44561