lean_workbook_plus_50138

Proved

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

Let $x,y,z$ be real numbers,such that $-1\leq x,y,z\leq1$ and $x+y+z+xyz=0$ . Replace $x = \frac{b-c}{b+c},\quad y = \frac{c-a}{c+a},\quad z = \frac{a-b}{a+b}, \quad \forall a,\,b,\,c \in \mathbb{R}^+.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50138 (x y z a b c : ℝ) (hab : 0 < a ∧ 0 < b ∧ 0 < c) (h : x = (b - c) / (b + c) ∧ y = (c - a) / (c + a) ∧ z = (a - b) / (a + b)) : -1 ≤ x ∧ x ≤ 1 ∧ -1 ≤ y ∧ y ≤ 1 ∧ -1 ≤ z ∧ z ≤ 1 ∧ x + y + z + x * y * z = 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph