lean_workbook_plus_54514

Proved

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

Prove Bernoulli's Inequality: $(1+x)^{n}>1+nx$ for $x>-1$ , $x \neq 0$ , and $n$ a positive integer greater than 1.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_54514 (x : ℝ) (n : ℕ) (hn : 1 < n) (hx : -1 < x) (hx' : x ≠ 0) : (1 + x) ^ n > 1 + n * x   :=  by sorry

Source