lean_workbook_plus_21953

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Then

\sqrt{a(a+8)}=\frac{15}{2}

\implies 4a^2+32a=225

\implies (2a+8)^2=289

\implies 2a+8=17

\implies a=\frac{9}{2}

Thus, the average of all the terms of the sequence is $A=\boxed{\frac{17}{2}}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_21953  (a : ℝ)
  (h₀ : 0 < a)
  (h₁ : Real.sqrt (a * (a + 8)) = 15 / 2) :
  (a + (a + 8)) / 2 = 17 / 2   :=  by sorry

Source