ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

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.

$\prod_{j \geq 0} (1 - 1 / (j + 2))$ has partial products $1 / (n + 1)$ , which tend to $0$ , so the product does not converge in the sense used here

Example

Put $p_{j} : = 1 / ι (j + 2)$ , so $0 < p_{j} \leq 1 / 2 < 1$ , and consider

$\prod_{j \geq 0} (1 - \frac{1}{j + 2}) = \prod_{j \geq 0} \frac{ι (j + 1)}{ι (j + 2)} = \frac{1}{2} \cdot \frac{2}{3} \cdot \frac{3}{4} \dots$

Its partial products telescope:

$\prod_{j < n} (1 - \frac{1}{ι (j + 2)}) = \frac{1}{ι (n + 1)} (n \in N),$

so they tend to $0$ . Every factor is nonzero, and yet the product does not converge in the sense of Infinite products: partial products, and convergence to a nonzero limit after finitely many vanishing factors, because no tail of it has partial products with a nonzero limit.

This is the example the definition of a convergent infinite product is written to exclude, and Infinite products: partial products, and convergence to a nonzero limit after finitely many vanishing factors names it for that purpose. Were a limit of $0$ admitted, this product would "converge to $0$ " with no factor equal to $0$ , and a convergent product could no longer be divided by.

The behaviour is also exactly what For $p_{k} \geq 0$ the product $\prod (1 + p_{k})$ converges iff $\sum p_{k}$ converges, with $1 + \sum_{k < n} p_{k} \leq \prod_{k < n} (1 + p_{k}) \leq 1 / (1 - \sum_{k < n} p_{k})$ when $\sum_{k < n} p_{k} < 1$ ; for $0 \leq p_{k} < 1$ the product $\prod (1 - p_{k})$ converges iff $\sum p_{k}$ converges and its partial products tend to $0$ otherwise; and $\sum ∣ p_{k} ∣$ convergent implies $\prod (1 + p_{k})$ convergent predicts: $\sum_{j} p_{j}$ is a tail of the harmonic series and diverges, so the partial products of $\prod (1 - p_{j})$ tend to $0$ .

Facts & Assumptions

Given: The sequence $p_{j} = 1 / ι (j + 2)$ and the partial products $Q_{n} = \prod_{j < n} (1 - p_{j})$ .

[L1]

Finite products: $\prod_{j < 0} x_{j} = 1$ and $\prod_{j < n + 1} x_{j} = (\prod_{j < n} x_{j}) x_{n}$ ; splitting at an intermediate index; a finite product of positive factors is positive (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L2]

The canonical naturals are positive for $n \geq 1$ , strictly increasing, and $ι (m + n) = ι (m) + ι (n)$ ; reciprocation reverses the order on the positives; and for every real $ε > 0$ there is $n \geq 1$ with $1 / ι (n) < ε$ (Canonical naturals are positive and strictly increasing, Inverses of positives are positive, and reciprocation reverses order, For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[L3]

The principle of induction on $N$ (The principle of mathematical induction).

[L4]

Convergence of an infinite product: some tail must have nonvanishing factors and partial products with a nonzero limit (Infinite products: partial products, and convergence to a nonzero limit after finitely many vanishing factors, Limits and Cauchy sequences of reals).

[L5]

$\sum_{k \geq 1} 1 / k^{p}$ converges if and only if $p > 1$ , with $ι (k)^{1} = ι (k)$ ; a series converges if and only if each of its tail series converges (For rational $p > 0$ , $\sum 1 / k^{p}$ converges iff $p > 1$ , A series converges iff each of its tail series converges, and the sum splits as $s_{N}$ plus the $N$ -th tail, Rational powers $a^{r}$ of a positive base, Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ , Integer powers $a^{m}$ , Series, partial sums, convergence and the sum, divergence, and the tail series).

[L6]

For $0 \leq p_{j} < 1$ with $\sum p_{j}$ divergent, the partial products of $\prod (1 - p_{j})$ tend to $0$ (For $p_{k} \geq 0$ the product $\prod (1 + p_{k})$ converges iff $\sum p_{k}$ converges, with $1 + \sum_{k < n} p_{k} \leq \prod_{k < n} (1 + p_{k}) \leq 1 / (1 - \sum_{k < n} p_{k})$ when $\sum_{k < n} p_{k} < 1$ ; for $0 \leq p_{k} < 1$ the product $\prod (1 - p_{k})$ converges iff $\sum p_{k}$ converges and its partial products tend to $0$ otherwise; and $\sum ∣ p_{k} ∣$ convergent implies $\prod (1 + p_{k})$ convergent).

Verification

technique · direct

1.1

For every $j$ , $ι (j + 2) \geq ι (2) = 2 > 0$ , so $0 < p_{j} \leq 1 / 2 < 1$ and $1 - p_{j} = ι (j + 1) / ι (j + 2) > 0$ .

givenL2

2.1

An induction gives $Q_{n} = 1 / ι (n + 1)$ for every $n$ : at $n = 0$ the empty product is $1 = 1 / ι (1)$ ; and $Q_{n + 1} = Q_{n} (1 - p_{n}) = \frac{1}{ι (n + 1)} \cdot \frac{ι (n + 1)}{ι (n + 2)} = \frac{1}{ι (n + 2)}$ .

step 1.1L1L2L3

2.2

The same conclusion follows from the general criterion: $\sum_{j} p_{j} = \sum_{j} 1 / ι (j + 2)$ is the first tail series of $\sum_{j} 1 / ι (j + 1)$ , which is the harmonic series and diverges, so $\sum_{j} p_{j}$ diverges and the partial products of $\prod (1 - p_{j})$ tend to $0$ .

step 1.1L5L6

3.1

Hence $Q_{n} \to 0$ : given a rational $ε > 0$ , an $n_{0} \geq 1$ with $1 / ι (n_{0}) < ε$ gives $0 < Q_{n} = 1 / ι (n + 1) \leq 1 / ι (n_{0}) < ε$ for every $n \geq n_{0}$ .

step 2.1L2

4.1

For every $N$ the $N$ -th tail products satisfy $\prod_{j = N}^{N + n - 1} (1 - p_{j}) = Q_{N + n} / Q_{N}$ , the finite product $Q_{N}$ being positive; so they also tend to $0$ as $n$ grows, $Q_{N}$ being a fixed nonzero real.

step 1.1step 2.1step 3.1L1

5.1

Therefore no tail of the product has partial products with a nonzero limit, and $\prod_{j} (1 - p_{j})$ does not converge, although every one of its factors is nonzero.

step 4.1L4

6.1

So the partial products are $1 / ι (n + 1)$ , they tend to $0$ , and the product diverges in the sense of Infinite products: partial products, and convergence to a nonzero limit after finitely many vanishing factors.

step 2.1step 5.1step 2.2∎

Remarks

The telescoping is the reason the answer is exactly $1 / (n + 1)$ . Each factor is $ι (j + 1) / ι (j + 2)$ , so consecutive numerators and denominators cancel and only the first numerator $ι (1) = 1$ and the last denominator $ι (n + 1)$ survive. Written informally, $\frac{1}{2} \cdot \frac{2}{3} \dots \frac{n}{n + 1} = \frac{1}{n + 1}$ .
Why a zero limit is excluded from the definition. If it were admitted, this product would have value $0$ although no factor is $0$ ; and then from $\prod a_{k} = 0$ one could infer nothing about the factors, whereas Infinite products: partial products, and convergence to a nonzero limit after finitely many vanishing factors arranges that a convergent product is $0$ exactly when some factor is. The exclusion costs this one example and buys that.
The index shift is not decorative. Written as $\prod_{n \geq 1} (1 - 1 / n)$ the same product begins with the factor $1 - 1 / 1 = 0$ ; the shift to $1 - 1 / (j + 2)$ is what keeps every factor nonzero, so that the failure is genuinely about the limit and not about a vanishing factor.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

64 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

Infinite product (Wikipedia) (standard reference, not scraped)
Telescoping series (Wikipedia) (standard reference, not scraped)
Thomson, Bruckner, and Bruckner, Elementary Real Analysis (standard reference, not scraped)

∏j≥0(1−1/(j+2))∏j≥0​(1−1/(j+2)) has partial products 1/(n+1)1/(n+1), which tend to 00, so the product does not converge in the sense used here