ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

The two-term AM-GM inequality, its equality case, and $x + x^{- 1} \geq 2$

Example

(a) For all $a, b \geq 0$ ,

$\frac{a + b}{2} \geq \sqrt{a b}, equivalently a b \leq (\frac{a + b}{2})^{2},$

with equality in either form exactly when $a = b$ .

(b) Consequently, for every $x > 0$ , $x + x^{- 1} \geq 2$ , with equality exactly when $x = 1$ .

Facts & Assumptions

Given: Reals $a, b \geq 0$ for part (a), a real $x > 0$ for part (b), and the display abbreviations $A : = (a + b) / 2$ , $G : = (a b)^{1 / 2}$ .

[L1]

Arithmetic-geometric mean (The arithmetic mean, geometric mean inequality): for $n = 2$ and entries $a, b \geq 0$ , $\prod_{k < 2} a_{k} \leq A^{2}$ , equivalently $G \leq A$ , with equality in either form exactly when $a = b$ .

[L2]

Roots and square roots (Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ , Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , Rational powers $a^{r}$ of a positive base): for $c \geq 0$ , $c^{1 / 2} = \sqrt{c}$ is the unique $s \geq 0$ with $s^{2} = c$ , and it is positive when $c > 0$ ; in particular $1^{1 / 2} = 1$ .

[L3]

Rational power and integer power algebra (Laws of rational exponents, Integer powers $a^{m}$ ): $x \cdot x^{- 1} = 1$ for $x \neq 0$ , where $x^{- 1} = (x^{1})^{- 1}$ is the inverse; and $1^{1 / 2} = 1$ . For $x > 0$ , the inverse $x^{- 1}$ is positive by claim 1 of Laws of rational exponents at the exponent $- 1$ .

[L4]

Monotonicity of squaring (Squaring is monotone on the nonnegatives): for $u, v \geq 0$ , $u \leq v$ holds exactly when $u^{2} \leq v^{2}$ ; consequently a nonnegative $s$ with $s^{2} = c$ is the unique square root of $c$ .

[L5]

Monotonicity of powers (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ ): $y \mapsto y^{j}$ is strictly increasing on the nonnegatives for $j \geq 1$ and $1^{j} = 1$ ; so $0 \leq y < 1$ gives $y^{2} < 1$ and $y > 1$ gives $y^{2} > 1$ .

Verification

technique · direct

1.1L1L2L4algebra

Part (a). Since $a, b \geq 0$ we have $A = (a + b) / 2 \geq 0$ and $G = (a b)^{1 / 2} \geq 0$ with $G^{2} = a b$ by [L2]; the theorem [L1] gives $G^{2} = a b \leq A^{2}$ , and the monotonicity of squaring on the nonnegatives [L4] turns $G^{2} \leq A^{2}$ into the equivalent $G \leq A$ , that is $\sqrt{a b} \leq (a + b) / 2$ ; conversely $G \leq A$ gives $a b = G^{2} \leq A^{2}$ , so the two displayed forms are equivalent for all $a, b \geq 0$ ; and the equality clause of [L1] gives $a b = A^{2}$ exactly when $a = b$ , equivalently $G = A$ exactly when $a = b$ by [L4], which is the equality assertion in both forms.

2.1step 1.1L2L3L5algebra

Part (b). Let $x > 0$ and apply part (a), as established in step 1.1, to the nonnegative pair $x$ and $x^{- 1}$ : the product is $x \cdot x^{- 1} = 1$ by [L3], so the geometric mean is $1^{1 / 2} = 1$ by [L2] and [L3], and the arithmetic mean is $(x + x^{- 1}) / 2$ ; hence $1 \leq (x + x^{- 1}) / 2$ , that is $x + x^{- 1} \geq 2$ ; equality holds exactly when $x = x^{- 1}$ by the equality clause of step 1.1, and $x = x^{- 1}$ holds exactly when $x^{2} = 1$ , since multiplying $x = x^{- 1}$ by $x$ gives $x^{2} = 1$ , while $x^{2} = 1$ gives $x = x \cdot 1 = x (x \cdot x^{- 1}) = (x \cdot x) x^{- 1} = 1 \cdot x^{- 1} = x^{- 1}$ ; finally, for $x > 0$ the equation $x^{2} = 1$ holds exactly at $x = 1$ , because $0 < x < 1$ gives $x^{2} < 1$ and $x > 1$ gives $x^{2} > 1$ by [L5] while $x = 1$ gives $x^{2} = 1$ .

3.1step 1.1step 2.1L1∎

The two claims are therefore proved: part (a) with its equality case for all nonnegative $a, b$ (step 1.1), and part (b) for every $x > 0$ with equality exactly at $x = 1$ (step 2.1).

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

48 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

Jiří Lebl, Basic Analysis I: Introduction to Real Analysis, Volume I, version 6.3, 15 May 2026 (author-hosted complete book) (standard reference, not scraped)
John K. Hunter, An Introduction to Real Analysis (author-hosted complete lecture notes, University of California at Davis) (standard reference, not scraped)

The two-term AM-GM inequality, its equality case, and x+x−1≥2x+x−1≥2