Cosine via Complex Exponentials

StatusFully Proven

TypeTheorem

ModuleChebyshevCircles.Proofs.PowerSums

Statement

Theorem Cosine via Complex Exponentials

$\cos x = \mathrm{Re}\!\left(\dfrac{e^{ix} + e^{-ix}}{2}\right).$

theorem cos_as_exp (x : ℝ) :
    Real.cos x = ((Complex.exp (x * Complex.I) + Complex.exp (-(x * Complex.I))) / 2).re := by

Proof ▼


  rw [show (Complex.exp (↑x * Complex.I) + Complex.exp (-(↑x * Complex.I))) / 2 =
      Complex.cos (x : ℂ) by
    rw [Complex.cos]
    congr 2
    congr 1
    rw [neg_mul]]
  exact Complex.cos_ofReal_re x

Dependencies (uses)

None

Dependents (used by)

Power Sum as Binomial Cosine Sum

Neighborhood

Depth: 1 / 1

Legend

Not Ready

Work in Progress

Sorry (theorems only)

Proven/Defined

Fully Proven (theorems only)

Axiom

Mathlib Ready

Theorems/Lemmas

Definitions

Axioms