by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Note that (a−1)(b−1)≥0 since −1≤a≤1 and −1≤b≤1 (so that a−1≤0 and b−1≤0 ). Then ab+1≥a+b . But also (a+1)(b+1)≥0 by a similar argument, so ab+1≥−(a+b) . Then ab+1≥∣a+b∣ . But ∣ab+1∣≥ab+1 , so we get ∣ab+1∣≥∣a+b∣ . Note that equality holds if and only if a=b=1 or a=b=−1 .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_70700 (a b : ℝ) (hab : a ∈ Set.Icc (-1) 1 ∧ b ∈ Set.Icc (-1) 1) :
|a * b + 1| ≥ |a + b| := by sorry