Theorem 6cn 11994

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 11970	. 2 ⊢ 6 = (5 + 1)
2		5cn 11991	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 10860	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10912	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2835	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800  1c1 10803   + caddc 10805  5c5 11961  6c6 11962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-addcl 10862

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817  df-2 11966  df-3 11967  df-4 11968  df-5 11969  df-6 11970

This theorem is referenced by:  7cn  11997  7m1e6  12035  6p2e8  12062  6p3e9  12063  halfpm6th  12124  6p4e10  12438  6t2e12  12470  6t3e18  12471  6t5e30  12473  5recm6rec  12510  bpoly2  15695  bpoly3  15696  bpoly4  15697  efi4p  15774  ef01bndlem  15821  cos01bnd  15823  3lcm2e6woprm  16248  6lcm4e12  16249  2exp8  16718  2exp11  16719  2exp16  16720  19prm  16747  83prm  16752  163prm  16754  317prm  16755  631prm  16756  1259lem1  16760  1259lem2  16761  1259lem3  16762  1259lem4  16763  1259lem5  16764  2503lem1  16766  2503lem2  16767  2503lem3  16768  2503prm  16769  4001lem1  16770  4001lem2  16771  4001lem4  16773  4001prm  16774  sincos6thpi  25577  sincos3rdpi  25578  1cubrlem  25896  log2ublem3  26003  log2ub  26004  basellem5  26139  basellem8  26142  ppiub  26257  bclbnd  26333  bposlem8  26344  bposlem9  26345  2lgslem3d  26452  2lgsoddprmlem3d  26466  ex-exp  28715  ex-bc  28717  ex-gcd  28722  ex-lcm  28723  hgt750lemd  32528  hgt750lem2  32532  problem5  33527  60gcd6e6  39940  60lcm7e420  39946  3exp7  39989  3lexlogpow5ineq1  39990  3lexlogpow5ineq5  39996  aks4d1p1p5  40011  aks4d1p1  40012  lhe4.4ex1a  41836  wallispi2lem2  43503  fmtno5lem1  44893  fmtno5lem4  44896  fmtno5  44897  fmtno4prmfac  44912  fmtno5faclem2  44920  fmtno5faclem3  44921  fmtno5fac  44922  flsqrt5  44934  139prmALT  44936  127prm  44939  mod42tp1mod8  44942  2t6m3t4e0  45572  zlmodzxzequa  45725  zlmodzxzequap  45728