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

defect_zero_iff_one

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)

  58theorem defect_zero_iff_one {x : ℝ} (hx : 0 < x) : defect x = 0 ↔ x = 1 := by

proof body

Tactic-mode proof.

  59  simp only [defect, J]
  60  constructor
  61  · intro h
  62    have hx0 : x ≠ 0 := hx.ne'
  63    -- (x + 1/x)/2 - 1 = 0 implies (x + 1/x) = 2
  64    have h1 : x + x⁻¹ = 2 := by linarith
  65    -- Multiply by x: x² + 1 = 2x, so (x-1)² = 0
  66    have h2 : x * (x + x⁻¹) = x * 2 := by rw [h1]
  67    have h3 : x^2 + 1 = 2 * x := by field_simp at h2; linarith
  68    nlinarith [sq_nonneg (x - 1)]
  69  · intro h; simp [h]
  70
  71/-- **Law of Existence (Forward)**: Existence implies defect is zero. -/

used by (29)

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

depends on (10)

Lean names referenced from this declaration's body.