Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26
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.

For every a>0a > 0, a1/n1a^{1/n} \to 1

Statement

Let aRa \in \mathbb{R} with a>0a > 0, write ι(n):=n1R\iota(n) := n \cdot 1_{\mathbb{R}} for the canonical natural (Canonical naturals are positive and strictly increasing) and a1/na^{1/n} for the nn-th root (Existence and uniqueness of nn-th roots: a unique a1/n0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a, Rational powers ara^r of a positive base), defined for naturals n1n \ge 1. Then:

  1. for every real b1b \ge 1 and every natural n1n \ge 1, 1    b1/n    1+b1ι(n);1 \;\le\; b^{1/n} \;\le\; 1 + \frac{b-1}{\iota(n)};
  2. the sequence ck:=a1/(k+1)c_k := a^{1/(k+1)}, kNk \in \mathbb{N}, converges to 11 (Limits and Cauchy sequences of reals).

Index range. As for the previous lemma on this page, a1/na^{1/n} requires n1n \ge 1, so the sequence indexed by N\mathbb{N} (Sequences of reals: bounded, eventually, frequently, tails, subsequences) is the shifted family a1/(k+1)a^{1/(k+1)}; it is the classical family a1/na^{1/n}, n1n \ge 1, reindexed by n=k+1n = k+1.

Facts & Assumptions

Given: A real a>0a > 0; the canonical naturals ι(n)=n1R\iota(n) = n \cdot 1_{\mathbb{R}} for n1n \ge 1; and the sequence ck:=a1/(k+1)c_k := a^{1/(k+1)}.

[L1]

Roots: for real x0x \ge 0 and natural n1n \ge 1 there is a unique real s0s \ge 0 with sn=xs^n = x, written x1/nx^{1/n}; it is >0> 0 when x>0x > 0, and 11/n=11^{1/n} = 1 by uniqueness (Existence and uniqueness of nn-th roots: a unique a1/n0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a, Integer powers ama^m).

[L2]

Rational powers: x1/nx^{1/n} is the rational power at exponent 1/n1/n; for rational t>0t > 0, x>1x > 1 implies xt>1x^t > 1; and (xy)1/n=x1/ny1/n(xy)^{1/n} = x^{1/n} y^{1/n} for x,y>0x, y > 0 (Rational powers ara^r of a positive base, Monotonicity of rarr \mapsto a^{r} and of aara \mapsto a^{r}, Laws of rational exponents).

[L3]

Bernoulli's inequality: (1+x)n1+ι(n)x(1+x)^n \ge 1 + \iota(n) x for x1x \ge -1 and nNn \in \mathbb{N} (Bernoulli's inequality (1+x)n1+nx(1+x)^n \ge 1 + nx).

[L4]

Canonical naturals: ι(n)>0\iota(n) > 0 and invertible for n1n \ge 1, and ι\iota is strictly increasing (Canonical naturals are positive and strictly increasing, Order on the natural numbers, \le is a linear order on N\mathbb{N}).

[L5]

Reciprocal Archimedean property: for every real η>0\eta > 0 there is a natural p1p \ge 1 with 1/p<η1/p < \eta; and 0<x<y0 < x < y gives 0<1/y<1/x0 < 1/y < 1/x (For every ε>0\varepsilon > 0 in a complete ordered field there is a natural n1n \ge 1 with 1/n<ε1/n < \varepsilon, Every complete ordered field is Archimedean, Inverses of positives are positive, and reciprocation reverses order).

[L6]

Order arithmetic: inequalities may be added and translated, and multiplying an inequality by a positive element preserves it; the order is total, so exactly one of a<1a < 1, a=1a = 1, a>1a > 1 holds (Order is preserved by adding a constant and by adding inequalities, Sign rules for products and monotonicity of multiplication, Ordered field, Complete ordered field (least-upper-bound property)).

[L7]

Squeeze theorem; a constant sequence converges to its value; to establish convergence it suffices to produce a threshold for every real ε>0\varepsilon > 0 (The squeeze theorem, Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals).

[L8]

Algebra of limits, reciprocal rule: if zjzz_j \to z with z0z \ne 0 and zj0z_j \ne 0 for every jj, then 1/zj1/z1/z_j \to 1/z (Algebra of limits: sums, scalar multiples, products and quotients).

Proof

technique · cases
1.1

Let bb be any real with b1b \ge 1 and let n1n \ge 1 be a natural. If b=1b = 1 then b1/n=1b^{1/n} = 1 and both inequalities hold. If b>1b > 1 then 1/n1/n is a positive rational, so t:=b1/n1>0t := b^{1/n} - 1 > 0; Bernoulli's inequality applied to t1t \ge -1 gives b=(b1/n)n=(1+t)n1+ι(n)tb = \big(b^{1/n}\big)^n = (1+t)^n \ge 1 + \iota(n)t, hence ι(n)tb1\iota(n) t \le b - 1 and t(b1)/ι(n)t \le (b-1)/\iota(n) since ι(n)>0\iota(n) > 0. In both cases 1b1/n1+(b1)/ι(n)1 \le b^{1/n} \le 1 + (b-1)/\iota(n), which is claim 1.

givenL1L2L3L4L6
1.2

Case one: a=1a = 1.

givenassume-case one
1.3

Case big: a>1a > 1.

givenassume-case big
1.4

Case small: 0<a<10 < a < 1.

givenassume-case small
2.1

For every real b>1b > 1 the sequence b1/(k+1)b^{1/(k+1)} converges to 11. Put dk:=1+(b1)/ι(k+1)d_k := 1 + (b-1)/\iota(k+1). Given a real ε>0\varepsilon > 0, the quotient ε/(b1)\varepsilon/(b-1) is positive, so there is a natural p1p \ge 1 with 1/p<ε/(b1)1/p < \varepsilon/(b-1); for kpk \ge p we have k+1>pk+1 > p, hence ι(k+1)>ι(p)>0\iota(k+1) > \iota(p) > 0 and 0<(b1)/ι(k+1)<(b1)(1/p)<ε0 < (b-1)/\iota(k+1) < (b-1)(1/p) < \varepsilon, so dk1<ε|d_k - 1| < \varepsilon and dk1d_k \to 1. By step 1.1 applied at n=k+1n = k+1 we have 1b1/(k+1)dk1 \le b^{1/(k+1)} \le d_k for every kk, and the constant sequence 11 converges to 11, so the squeeze theorem gives b1/(k+1)1b^{1/(k+1)} \to 1.

step 1.1L4L5L6L7
2.2

In case one, ck=11/(k+1)=1c_k = 1^{1/(k+1)} = 1 for every kk, so (ck)(c_k) is the constant sequence 11 and converges to 11.

step 1.2L1L7
3.1

In case big, a>1a > 1, so step 2.1 applied with b=ab = a gives ck=a1/(k+1)1c_k = a^{1/(k+1)} \to 1.

step 2.1step 1.3
3.2

In case small, put a:=1/aa' := 1/a, which satisfies a>1a' > 1 because 0<a<10 < a < 1. For each natural n1n \ge 1 the product rule for roots gives a1/n(a)1/n=(aa)1/n=11/n=1a^{1/n} (a')^{1/n} = (a a')^{1/n} = 1^{1/n} = 1, so a1/n=1/(a)1/na^{1/n} = 1/(a')^{1/n}, and (a)1/n>0(a')^{1/n} > 0. By step 2.1 the sequence (a)1/(k+1)(a')^{1/(k+1)} converges to 101 \ne 0 with all terms nonzero, so the reciprocal rule gives ck=1/(a)1/(k+1)1/1=1c_k = 1/(a')^{1/(k+1)} \to 1/1 = 1.

step 2.1step 1.4L1L2L5L8
4.1

The three cases are exhaustive by trichotomy applied to aa and 11, the hypothesis a>0a > 0 excluding nothing else, and in each of them (ck)(c_k) converges to 11; together with step 1.1 this proves both claims.

step 2.2step 3.1step 3.2step 1.1L6cases: trichotomy of the ordercases-exhaustive

Remarks

  • Bernoulli is doing the whole job in the case a>1a > 1. The inequality (1+t)n1+nt(1+t)^n \ge 1 + nt converts the exact identity (a1/n)n=a\big(a^{1/n}\big)^n = a into the linear bound t(a1)/nt \le (a-1)/n on the excess t=a1/n1t = a^{1/n} - 1, and that bound is what tends to 00. No estimate on a1/na^{1/n} itself is needed beyond a1/n>1a^{1/n} > 1.

  • The case 0<a<10 < a < 1 is not symmetric to the case a>1a > 1 and is not proved again. It is transported by the reciprocal, using a1/n(1/a)1/n=1a^{1/n} (1/a)^{1/n} = 1 (Laws of rational exponents) and the reciprocal rule of Algebra of limits: sums, scalar multiples, products and quotients. The hypothesis of that rule, that the limit be nonzero and every term nonzero, is met because roots of positive reals are positive.

  • The rate is different from the one in n1/n1n^{1/n} \to 1. Here the excess is O(1/n)O(1/n) with a constant depending on aa; there the base itself grows with nn and the excess is only O(1/n1/2)O(1/n^{1/2}). The two lemmas are therefore not instances of one another in either direction.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 98 results over 27 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources