pith. machine review for the scientific record. sign in
theorem proved term proof

dalembert_identity

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)

 508theorem dalembert_identity {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
 509    Jcost (x * y) + Jcost (x / y) = 2 * Jcost x + 2 * Jcost y + 2 * Jcost x * Jcost y := by

proof body

Term-mode proof.

 510  have hx0 : x ≠ 0 := ne_of_gt hx
 511  have hy0 : y ≠ 0 := ne_of_gt hy
 512  have hxy : x * y ≠ 0 := mul_ne_zero hx0 hy0
 513  have hxdy : x / y ≠ 0 := div_ne_zero hx0 hy0
 514  simp only [Jcost_eq_sq hxy, Jcost_eq_sq hxdy, Jcost_eq_sq hx0, Jcost_eq_sq hy0]
 515  field_simp
 516  ring
 517
 518/-- From d'Alembert: J(xy) ≤ 2J(x) + 2J(y) + 2J(x)J(y) since J(x/y) ≥ 0 -/

used by (8)

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.