LemmaStatement: AI-adaptedProof: AI-adaptedprecheck 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} \geq 1 + n x$

Statement

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

$(1 + x)^{n} \geq 1 + n x,$

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

Facts & Assumptions

Given: An ordered field $R$ , an element $x \geq - 1$ of it, and a natural number $n$ , with $ι (n) \in 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 \geq 0$ , $u \geq v$ implies $u c \geq v c$ . Sign rules for products and monotonicity of multiplication gives only the strict rule $u > v ⟺ u c > v c$ 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 \neq 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} \geq 0$ for every $x$ .

[L5]

Canonical naturals: $ι (0) = 0$ , $ι (n + 1) = ι (n) + 1$ , and $ι (n) > 0$ for $n \geq 1$ , so $ι (n) \geq 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 N$ and assume $(1 + x)^{n} \geq 1 + n x$ .

1.3

Since $x \geq - 1$ we have $1 + x \geq 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} \geq 0$ , since $x^{2} \geq 0$ and $ι (n) \geq 0$ , so scaling the inequality $x^{2} \geq 0$ by the nonnegative factor $ι (n)$ gives $ι (n) x^{2} \geq ι (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 \geq 2$ and $x \neq 0$ with $x \geq - 1$ , then $(1 + x)^{n} > 1 + n x$ , 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 + 2 x + x^{2} > 1 + 2 x$ because $x^{2} > 0$ ; and assuming $(1 + x)^{m} > 1 + m x$ for some $m \geq 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 + m x) (1 + x) = 1 + (m + 1) x + m x^{2} \geq 1 + (m + 1) x$ , so the strict inequality passes to $m + 1$ in either case.

L1L2L3L4L5

2.1

Multiplying the hypothesis by $1 + x \geq 0$ and expanding: $(1 + x)^{n + 1} = (1 + x)^{n} (1 + x) \geq (1 + n x) (1 + x) = 1 + (n + 1) x + n x^{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 \leq 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} \geq 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} \geq 1 + n x$ holds for every $n \in N$ and every $x \geq - 1$ , and by steps 2.2 and 1.5 equality holds exactly when $n \leq 1$ or $x = 0$ .

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

Depends on

Used by

Dependency tree · two levels

25 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on 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≥1+nx