LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Bernoulli's inequality $(1+x)^n \ge 1 + nx$

Statement

Let $\mathbb{R}$ be an ordered field (Ordered field), let $x \in \mathbb{R}$ with $x \ge -1$ , and let $n \in \mathbb{N}$ , with powers as in Integer powers $a^m$ and with $n$ also denoting the canonical natural $\iota(n) \in \mathbb{R}$ (Canonical naturals are positive and strictly increasing, The unique embedding of ℚ into an ordered field). Then

$(1+x)^n \ge 1 + nx,$

and equality holds if and only if $n \le 1$ or $x = 0$ .

Facts & Assumptions

Given: An ordered field $\mathbb{R}$ , an element $x \ge -1$ of it, and a natural number $n$ , with $\iota(n) \in \mathbb{R}$ written $n$ .

[L1]

Definition of powers (Integer powers $a^m$ ): $a^0 = 1$ and $a^{n+1} = a^n a$ .

[L2]

Induction principle (The principle of mathematical induction).

[L3]

Order and scaling: for $c \ge 0$ , $u \ge v$ implies $uc \ge vc$ . Sign rules for products and monotonicity of multiplication gives only the strict rule $u > v \iff uc > vc$ for $c > 0$ , so this is that rule together with the case $u = v$ , and with the case $c = 0$ , where both sides are $0$ (Multiplication by zero: $0 \cdot a = 0$ ). Likewise adding a constant preserves the order, where Order is preserved by adding a constant and by adding inequalities again states only the strict form and the nonstrict one adds the case of equality; trichotomy is what settles those cases (Ordered field).

[L4]

Squares are nonnegative: $x^2 > 0$ for $x \ne 0$ (Squares of nonzero elements are positive), and $0^2 = 0 \cdot 0 = 0$ because a product with a zero factor vanishes (Multiplication by zero: $0 \cdot a = 0$ ), which is also what makes $0 \cdot x = 0$ below; so $x^2 \ge 0$ for every $x$ .

[L5]

Canonical naturals: $\iota(0) = 0$ , $\iota(n+1) = \iota(n) + 1$ , and $\iota(n) > 0$ for $n \ge 1$ , so $\iota(n) \ge 0$ for every $n$ (Canonical naturals are positive and strictly increasing, The unique embedding of ℚ into an ordered field).

Proof

technique · induction

1.1

Base case $n = 0$ : $(1+x)^0 = 1$ and $1 + 0 \cdot x = 1$ , so the inequality holds with equality.

baseL1L4L5

1.2

Inductive hypothesis: fix $n \in \mathbb{N}$ and assume $(1+x)^n \ge 1 + nx$ .

1.3

Since $x \ge -1$ we have $1 + x \ge 0$ , and this is exactly what licenses multiplying the inductive inequality by $1 + x$ without reversing it.

givenL3

1.4

The discarded term is nonnegative: $n x^2 \ge 0$ , since $x^2 \ge 0$ and $\iota(n) \ge 0$ , so scaling the inequality $x^2 \ge 0$ by the nonnegative factor $\iota(n)$ gives $\iota(n) x^2 \ge \iota(n) \cdot 0 = 0$ ; the scaling rule, and not the nonnegativity of the two factors on its own, is what licenses this.

L3L4L5

1.5

Equality analysis, the strict direction: if $n \ge 2$ and $x \ne 0$ with $x \ge -1$ , then $(1+x)^n > 1 + nx$ , by a second induction, on $j$ , over the statement $(1+x)^{j+2} > 1 + (j+2)x$ ; for $j = 0$ we have $(1+x)^2 = 1 + 2x + x^2 > 1 + 2x$ because $x^2 > 0$ ; and assuming $(1+x)^{m} > 1 + mx$ for some $m \ge 2$ , there are two possibilities: if $x = -1$ then $(1+x)^{m+1} = 0$ while $1 + (m+1)x = 1 - (m+1) = -m < 0$ , and if $x > -1$ then $1 + x > 0$ and $(1+x)^{m+1} = (1+x)^{m}(1+x) > (1 + mx)(1 + x) = 1 + (m+1)x + mx^2 \ge 1 + (m+1)x$ , so the strict inequality passes to $m+1$ in either case.

L1L2L3L4L5

2.1

Multiplying the hypothesis by $1 + x \ge 0$ and expanding: $(1+x)^{n+1} = (1+x)^n (1+x) \ge (1 + nx)(1 + x) = 1 + (n+1)x + nx^2$ .

step 1.2step 1.3L1L3L5

2.2

Equality analysis, the easy direction: at $n = 0$ both sides are $1$ , and at $n = 1$ both sides are $1 + x$ , so equality holds whenever $n \le 1$ ; and if $x = 0$ both sides are $1$ for every $n$ , since $(1+0)^n = 1^n = 1$ .

step 1.1L1L5

3.1

Hence $(1+x)^{n+1} \ge 1 + (n+1)x$ , which is the claim at $n+1$ .

step 2.1step 1.4L3

4.1

By the induction principle the inequality $(1+x)^n \ge 1 + nx$ holds for every $n \in \mathbb{N}$ and every $x \ge -1$ , and by steps 2.2 and 1.5 equality holds exactly when $n \le 1$ or $x = 0$ .

step 1.1step 3.1step 2.2step 1.5L2discharge-induction∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 50 results over 16 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. Lebl, Basic Analysis I (standard reference, not scraped)
Radicals and rational exponents (Emory University) (standard reference, not scraped)
Bernoulli's inequality (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
M. Spivak, Calculus, 4th ed., Ch. 2 (standard reference, not scraped)

Bernoulli's inequality (1+x)n≥1+nx(1+x)^n \ge 1 + nx(1+x)n≥1+nx