Theorem 6cn 12327

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 12303	. 2 ⊢ 6 = (5 + 1)
2		5cn 12324	. . 3 ⊢ 5 ∈ ℂ
3		ax-1cn 11190	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11244	. 2 ⊢ (5 + 1) ∈ ℂ
5	1, 4	eqeltri 2825	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2099  (class class class)co 7414  ℂcc 11130  1c1 11133   + caddc 11135  5c5 12294  6c6 12295

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 2699  ax-1cn 11190  ax-addcl 11192

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2720  df-clel 2806  df-2 12299  df-3 12300  df-4 12301  df-5 12302  df-6 12303

This theorem is referenced by:  7cn  12330  7m1e6  12368  6p2e8  12395  6p3e9  12396  halfpm6th  12457  6p4e10  12773  6t2e12  12805  6t3e18  12806  6t5e30  12808  5recm6rec  12845  bpoly2  16027  bpoly3  16028  bpoly4  16029  efi4p  16107  ef01bndlem  16154  cos01bnd  16156  3lcm2e6woprm  16579  6lcm4e12  16580  2exp8  17051  2exp11  17052  2exp16  17053  19prm  17080  83prm  17085  163prm  17087  317prm  17088  631prm  17089  1259lem1  17093  1259lem2  17094  1259lem3  17095  1259lem4  17096  1259lem5  17097  2503lem1  17099  2503lem2  17100  2503lem3  17101  2503prm  17102  4001lem1  17103  4001lem2  17104  4001lem4  17106  4001prm  17107  sincos6thpi  26443  sincos3rdpi  26444  1cubrlem  26766  log2ublem3  26873  log2ub  26874  basellem5  27010  basellem8  27013  ppiub  27130  bclbnd  27206  bposlem8  27217  bposlem9  27218  2lgslem3d  27325  2lgsoddprmlem3d  27339  ex-exp  30253  ex-bc  30255  ex-gcd  30260  ex-lcm  30261  hgt750lemd  34274  hgt750lem2  34278  problem5  35267  60gcd6e6  41469  60lcm7e420  41475  3exp7  41518  3lexlogpow5ineq1  41519  3lexlogpow5ineq5  41525  aks4d1p1p5  41540  aks4d1p1  41541  lhe4.4ex1a  43760  wallispi2lem2  45454  fmtno5lem1  46887  fmtno5lem4  46890  fmtno5  46891  fmtno4prmfac  46906  fmtno5faclem2  46914  fmtno5faclem3  46915  fmtno5fac  46916  flsqrt5  46928  139prmALT  46930  127prm  46933  mod42tp1mod8  46936  2t6m3t4e0  47406  zlmodzxzequa  47558  zlmodzxzequap  47561

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »