Theorem 6cn 12309

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 12284	. 2 ⊢ 6 = (5 + 1)
2		5cn 12306	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11131	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11188	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2858	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2142  (class class class)co 7396  ℂcc 11071  1c1 11074   + caddc 11076  5c5 12275  6c6 12276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11131  ax-addcl 11133

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-clel 2837  df-2 12280  df-3 12281  df-4 12282  df-5 12283  df-6 12284

This theorem is referenced by:  7cn  12312  7m1e6  12349  6p2e8  12376  6p3e9  12377  halfpm6th  12443  6p4e10  12765  6t2e12  12797  6t3e18  12798  6t5e30  12800  5recm6rec  12838  bpoly2  16087  bpoly3  16088  bpoly4  16089  efi4p  16169  ef01bndlem  16216  cos01bnd  16218  3lcm2e6woprm  16649  6lcm4e12  16650  2exp8  17124  2exp11  17125  2exp16  17126  19prm  17154  83prm  17159  163prm  17161  317prm  17162  631prm  17163  1259lem1  17167  1259lem2  17168  1259lem3  17169  1259lem4  17170  1259lem5  17171  2503lem1  17173  2503lem2  17174  2503lem3  17175  2503prm  17176  4001lem1  17177  4001lem2  17178  4001lem4  17180  4001prm  17181  sincos6thpi  26581  sincos3rdpi  26582  1cubrlem  26906  log2ublem3  27013  log2ub  27014  basellem5  27149  basellem8  27152  ppiub  27268  bclbnd  27344  bposlem8  27355  bposlem9  27356  2lgslem3d  27463  2lgsoddprmlem3d  27477  ex-exp  30652  ex-bc  30654  ex-gcd  30659  ex-lcm  30660  hgt750lemd  34942  hgt750lem2  34946  problem5  36019  60gcd6e6  42621  60lcm7e420  42627  3exp7  42670  3lexlogpow5ineq1  42671  3lexlogpow5ineq5  42677  aks4d1p1p5  42692  aks4d1p1  42693  sq6  42904  lhe4.4ex1a  44905  wallispi2lem2  46646  sin5tlem1  47467  sin5tlem4  47470  sin5tlem5  47471  fmtno5lem1  48162  fmtno5lem4  48165  fmtno5  48166  fmtno4prmfac  48181  fmtno5faclem2  48189  fmtno5faclem3  48190  fmtno5fac  48191  flsqrt5  48203  139prmALT  48205  127prm  48208  mod42tp1mod8  48211  2t6m3t4e0  48970  zlmodzxzequa  49118  zlmodzxzequap  49121