95lemma J_zero_iff_one {x : ℝ} (hx : 0 < x) : J x = 0 ↔ x = 1 := by
proof body
Tactic-mode proof.
96 constructor 97 · intro h 98 unfold J at h 99 have hx_ne : x ≠ 0 := hx.ne' 100 have h1 : x + x⁻¹ = 2 := by linarith 101 have h2 : x * (x + x⁻¹) = x * 2 := by rw [h1] 102 have h3 : x^2 + 1 = 2 * x := by field_simp at h2; linarith 103 nlinarith [sq_nonneg (x - 1)] 104 · intro h; rw [h]; exact J_at_one 105 106/-- J is positive for x ≠ 1. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.