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 field image $n \cdot 1_{R}$ of the natural number n (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 field coefficients denoting the canonical image $n \cdot 1_{R}$ ; the exponent remains natural.

[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 in the field: $0 \cdot 1_{R} = 0_{R}$ , $(n + 1) \cdot 1_{R} = n \cdot 1_{R} + 1_{R}$ , and $n \cdot 1_{R} > 0$ for natural $n \geq 1$ , so these field images are nonnegative for every natural n (Canonical naturals are positive and strictly increasing, The unique embedding of ℚ into an ordered field).

Proof

technique · induction

1.1baseL1L4L5

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

1.2ih

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

1.3givenL3

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.

1.4L3L4L5

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.

1.5L1L2L3L4L5

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.

2.1step 1.2step 1.3L1L3L5

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}$ .

2.2step 1.1L1L5

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$ .

3.1step 2.1step 1.4L3

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

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

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$ .

Bernoulli's inequality $(1 + x)^{n} \geq 1 + n x$

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

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

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Bernoulli's inequality $(1 + x)^{n} \geq 1 + n x$