Alphabeta Math
TheoremStatement: AI-adaptedProof: Literature-sourcedprecheck passverified 2026-08-05 (gpt-5.6-sol-codex-subscription)
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 squeeze theorem

Statement

Let (ak), (xk) and (bk) be sequences of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) with

ak≤xk≤bkeventually,

and suppose (ak) and (bk) both converge to the same real L (Limits and Cauchy sequences of reals). Then (xk) converges to L.

The middle sequence is not assumed to converge; that is the point of the theorem, and it is why the squeeze is a tool for establishing convergence rather than for computing a limit already known to exist.

Facts & Assumptions

Given: Sequences (ak), (xk), (bk) of reals, an index K0∈N with ak≤xk≤bk for every k≥K0, and a real L such that (ak) converges to L and (bk) converges to L (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals).

[L1]

Convergence, quantified over rational ε>0 (Limits and Cauchy sequences of reals).

[L2]

Absolute value: for c>0, ∣u∣<c if and only if −c<u<c (Basic properties of the absolute value).

[L3]

Order arithmetic in R: adding a constant preserves < and ≤; u<v≤w and u≤v<w both give u<w; and ≤ is transitive (Order is preserved by adding a constant and by adding inequalities, Complete ordered field (least-upper-bound property), Ordered field).

[L4]

The order on N is total and transitive, so three indices K0,K1,K2 admit an index K with K≥K0, K≥K1 and K≥K2, and then k≥K gives k≥K0, k≥K1, k≥K2 (≤ is a linear order on N).

Proof

technique · direct
1.1

Let ε>0 be rational. By convergence of (ak) there is K1 with ∣ak−L∣<ε for all k≥K1, and by convergence of (bk) there is K2 with ∣bk−L∣<ε for all k≥K2.

L1
2.1

By [L2], ∣ak−L∣<ε gives −ε<ak−L, that is L−ε<ak, for all k≥K1; and ∣bk−L∣<ε gives bk−L<ε, that is bk<L+ε, for all k≥K2.

step 1.1L2L3
3.1

Choose K with K≥K0, K≥K1 and K≥K2. For every k≥K the hypothesis gives ak≤xk≤bk, so L−ε<ak≤xk≤bk<L+ε, hence L−ε<xk<L+ε, hence −ε<xk−L<ε, hence ∣xk−L∣<ε.

step 2.1givenL2L3L4choose
4.1

The rational ε>0 was arbitrary, so for every rational ε>0 there is an index K beyond which ∣xk−L∣<ε; that is, (xk) converges to L.

step 3.1L1∎

Remarks

  • The proof is direct from the definition and does not route through Limits preserve non-strict inequalities. It could not: that lemma assumes the middle sequence converges, which is what is being proved here.

  • Both bounding sequences must have the same limit. With ak=−1, bk=1 and any (xk) taking values in [−1,1] the hypothesis ak≤xk≤bk holds and nothing whatever follows, since a bounded sequence need not converge (FALSE: every bounded sequence converges).

  • The most common use is with ak=−ck and bk=ck for a null sequence (ck): if ∣xk∣≤ck eventually and ck→0, then xk→0. That special case also follows from A null sequence times a bounded sequence is null whenever xk is presented as a product of a null sequence and a bounded one, but the squeeze needs no such presentation.

Depends on

Used by

Dependency tree · two levels

24 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