lean_workbook_plus_22982

Proved

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

$xyz+\frac{1}{xyz}-2=0\Rightarrow (xyz)^2-2(xyz)+1=0\Rightarrow xyz=\pm 1\Rightarrow \boxed{B}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_22982 (x y z : ℝ) (h : x * y * z + 1 / (x * y * z) - 2 = 0) : (x * y * z) ^ 2 - 2 * (x * y * z) + 1 = 0   :=  by sorry

Source