pith. machine review for the scientific record. sign in
lemma proved tactic proof

PhiPow_sub

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  56lemma PhiPow_sub (x y : ℝ) : PhiPow (x - y) = PhiPow x / PhiPow y := by

proof body

Tactic-mode proof.

  57  unfold PhiPow
  58  have hx : Real.log (Constants.phi) * (x - y)
  59        = Real.log (Constants.phi) * x + Real.log (Constants.phi) * (-y) := by
  60    ring
  61  calc
  62    Real.exp (Real.log (Constants.phi) * (x - y))
  63        = Real.exp (Real.log (Constants.phi) * x + Real.log (Constants.phi) * (-y)) := by
  64              simp [hx]
  65    _   = Real.exp (Real.log (Constants.phi) * x)
  66            * Real.exp (Real.log (Constants.phi) * (-y)) := by
  67              simp [Real.exp_add]
  68    _   = Real.exp (Real.log (Constants.phi) * x)
  69            * (Real.exp (Real.log (Constants.phi) * y))⁻¹ := by
  70              simp [Real.exp_neg]
  71    _   = Real.exp (Real.log (Constants.phi) * x)
  72            / Real.exp (Real.log (Constants.phi) * y) := by
  73              simp [div_eq_mul_inv]
  74

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.