Theorem 6cn 11720

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 11696	. 2 ⊢ 6 = (5 + 1)
2		5cn 11717	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 10587	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10639	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2907	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7148  ℂcc 10527  1c1 10530   + caddc 10532  5c5 11687  6c6 11688

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 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-ext 2791  ax-1cn 10587  ax-addcl 10589

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-cleq 2812  df-clel 2891  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696

This theorem is referenced by:  7cn  11723  7m1e6  11761  6p2e8  11788  6p3e9  11789  halfpm6th  11850  6p4e10  12162  6t2e12  12194  6t3e18  12195  6t5e30  12197  5recm6rec  12234  bpoly2  15403  bpoly3  15404  bpoly4  15405  efi4p  15482  ef01bndlem  15529  cos01bnd  15531  3lcm2e6woprm  15951  6lcm4e12  15952  2exp8  16415  2exp16  16416  19prm  16443  83prm  16448  163prm  16450  317prm  16451  631prm  16452  1259lem1  16456  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  2503lem1  16462  2503lem2  16463  2503lem3  16464  2503prm  16465  4001lem1  16466  4001lem2  16467  4001lem4  16469  4001prm  16470  sincos6thpi  25093  sincos3rdpi  25094  1cubrlem  25411  log2ublem3  25518  log2ub  25519  basellem5  25654  basellem8  25657  ppiub  25772  bclbnd  25848  bposlem8  25859  bposlem9  25860  2lgslem3d  25967  2lgsoddprmlem3d  25981  ex-exp  28221  ex-bc  28223  ex-gcd  28228  ex-lcm  28229  hgt750lemd  31912  hgt750lem2  31916  problem5  32905  lhe4.4ex1a  40651  wallispi2lem2  42347  fmtno5lem1  43705  fmtno5lem4  43708  fmtno5  43709  fmtno4prmfac  43724  fmtno5faclem2  43732  fmtno5faclem3  43733  fmtno5fac  43734  flsqrt5  43747  139prmALT  43749  127prm  43753  2exp11  43755  mod42tp1mod8  43757  2t6m3t4e0  44386  zlmodzxzequa  44541  zlmodzxzequap  44544