LemmaStatement: AI-adaptedProof: AI-generatedSession-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 real $x$ , $x^k/k! \to 0$

Statement

Write $\iota(n) := n \cdot 1_{\mathbb{R}}$ for the canonical natural (Canonical naturals are positive and strictly increasing) and define the factorial as the finite product (Finite sums and finite products, by recursion)

$k! \;:=\; \prod_{j < k} \iota(j+1) \qquad (k \in \mathbb{N}),$

so that $0! = 1$ , the empty product, and $(k+1)! = k! \cdot \iota(k+1)$ . Every $k!$ is a positive real. Then, for every $x \in \mathbb{R}$ ,

$\frac{x^{k}}{k!} \longrightarrow 0 ,$

the numerator being the integer power of Integer powers $a^m$ and the convergence that of Limits and Cauchy sequences of reals.

The index range needs no adjustment: $k!$ is defined at $k = 0$ with value $1$ , and $x^0 = 1$ , so the sequence begins with $x^0/0! = 1$ .

Facts & Assumptions

Given: A real $x$ ; the modulus $M := |x| \ge 0$ ; the factorials $k! = \prod_{j<k}\iota(j+1)$ ; and the canonical naturals $\iota(n) = n \cdot 1_{\mathbb{R}}$ .

[A1]

$P(j)$ denotes the statement $M^{N+j}/(N+j)! \le A \lambda^{j}$ , where $N$ , $\lambda$ and $A$ are fixed in step 1.3.

[L1]

Finite products: the empty product is $1$ , $\prod_{j<m+1} a_j = \big(\prod_{j<m} a_j\big) a_m$ , and a product of positive factors is positive (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L2]

Integer powers: $z^{0} = 1$ , $z^{m+1} = z^{m} z$ , and $z \ge 0$ implies $z^{m} \ge 0$ (Integer powers $a^m$ , Monotonicity of $x \mapsto x^n$ and of $n \mapsto a^n$ , Laws of integer exponents).

[L3]

Absolute value: $|zw| = |z||w|$ , $|z| \ge 0$ , and $|z| = z$ for $z \ge 0$ (Basic properties of the absolute value).

[L4]

Induction principle (The principle of mathematical induction).

[L5]

Canonical naturals: $\iota(n) > 0$ and invertible for $n \ge 1$ , $\iota$ is strictly increasing, and for every real $y$ there is a natural $N \ge 1$ with $y < \iota(N)$ (Canonical naturals are positive and strictly increasing, Every complete ordered field is Archimedean, Order on the natural numbers, $\le$ is a linear order on $\mathbb{N}$ ).

[L6]

Order arithmetic: Inverses of positives are positive, and reciprocation reverses order, claim 4 of Sign rules for products and monotonicity of multiplication and Order is preserved by adding a constant and by adding inequalities state the strict forms, that $0 < u < v$ gives $0 < 1/v < 1/u$ , that multiplication by a positive element preserves $<$ , and that inequalities may be translated and added; adjoining the case of equality gives the nonstrict forms used below, and multiplication by $0$ sends both sides to $0$ , so a nonnegative multiplier preserves $\le$ . Products of nonnegative inequalities multiply in the nonstrict form stated by Multiplying inequalities of positives.

[L7]

Geometric sequences: $|r| < 1$ implies $r^{j} \to 0$ (For $|r| < 1$ the sequence $r^k$ is null, and for $|r| > 1$ the sequence $|r|^k$ diverges to $+\infty$ ); a scalar multiple of a convergent sequence converges to the scalar multiple of the limit (Algebra of limits: sums, scalar multiples, products and quotients).

[L8]

Squeeze theorem, and the fact that a constant sequence converges to its value (The squeeze theorem, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L9]

A sequence converges to $z$ if and only if some tail of it does; the $K$ -th tail of $(z_k)$ is $j \mapsto z_{j+K}$ (Convergence depends only on the tail, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

Proof

technique · induction

1.1

Each $k!$ is a product of the positive reals $\iota(j+1)$ , $j < k$ , hence positive, and $(k+1)! = k! \cdot \iota(k+1)$ ; also $M = |x| \ge 0$ .

givenL1L3L5

1.2

For every $k \in \mathbb{N}$ one has $|x^{k}| = M^{k}$ : at $k = 0$ both sides are $|1| = 1 = M^{0}$ , and if $|x^{k}| = M^{k}$ then $|x^{k+1}| = |x^{k} x| = |x^{k}||x| = M^{k} M = M^{k+1}$ , so this follows by induction on $k$ .

givenL2L3L4

1.3

Take a natural $N \ge 1$ with $M < \iota(N)$ and put $\lambda := M/\iota(N)$ and $A := M^{N}/N!$ . Then $0 \le \lambda < 1$ , since $0 \le M < \iota(N)$ and $\iota(N) > 0$ , and $A \ge 0$ .

givenL1L2L5L6choose

1.4

The statement $P(0)$ holds, with equality: $M^{N+0}/(N+0)! = M^{N}/N! = A = A \cdot 1 = A\lambda^{0}$ .

givenA1L2base

1.5

Fix $j \in \mathbb{N}$ and assume $P(j)$ , that is $M^{N+j}/(N+j)! \le A\lambda^{j}$ .

A1ih

2.1

Then $P(j+1)$ holds. Indeed $M^{N+j+1}/(N+j+1)! = \big(M^{N+j}/(N+j)!\big)\big(M/\iota(N+j+1)\big)$ , and $N + j + 1 > N$ gives $\iota(N+j+1) > \iota(N) > 0$ , hence $0 \le M/\iota(N+j+1) \le M/\iota(N) = \lambda$ ; since also $0 \le M^{N+j}/(N+j)! \le A\lambda^{j}$ by step 1.5 and $A\lambda^{j} \ge 0$ , multiplying the two nonnegative inequalities gives $M^{N+j+1}/(N+j+1)! \le A\lambda^{j}\lambda = A\lambda^{j+1}$ .

step 1.5A1L1L2L5L6

3.1

By the induction principle $P(j)$ holds for every $j \in \mathbb{N}$ , and $M^{N+j}/(N+j)! \ge 0$ always, so $0 \le M^{N+j}/(N+j)! \le A\lambda^{j}$ for every $j$ .

step 1.4step 2.1A1L1L2L4

4.1

Since $|\lambda| = \lambda < 1$ , the sequence $(\lambda^{j})_j$ converges to $0$ , hence so does $(A\lambda^{j})_j$ ; the constant sequence $0$ also converges to $0$ , so the squeeze theorem applied to step 3.1 shows that the $N$ -th tail $j \mapsto M^{N+j}/(N+j)!$ converges to $0$ , and therefore $(M^{k}/k!)_k$ converges to $0$ . Finally $|x^{k}/k! - 0| = |x^{k}|/k! = M^{k}/k!$ by steps 1.1 and 1.2, so $x^{k}/k! \to 0$ .

step 3.1step 1.1step 1.2L3L7L8L9discharge-induction∎

Remarks

The threshold $N$ is chosen so that the ratio is bounded by a constant less than $1$ . Beyond index $N$ each further factor of the factorial is at least $\iota(N)$ , so multiplying by $x$ and dividing by that factor shrinks the term by at least the factor $\lambda = M/\iota(N) < 1$ . That is the entire mechanism: a factorial eventually beats a geometric sequence because its ratios, unlike a geometric sequence's, tend to $0$ .
No halving is used. Many texts take $N$ with $M/N \le 1/2$ ; here it is enough to take $N$ with $M < \iota(N)$ , which the Archimedean property supplies directly and which keeps every quantity a ratio of things already in hand.
The case $x = 0$ is not special. Then $M = 0$ , $\lambda = 0$ and the bound reads $M^{N+j}/(N+j)! \le 0$ for $j \ge 1$ , which is correct since those terms are $0$ ; and $(0^{j})_j$ converges to $0$ because $|0| < 1$ , so For $|r| < 1$ the sequence $r^k$ is null, and for $|r| > 1$ the sequence $|r|^k$ diverges to $+\infty$ applies unchanged.
This is the strongest of the three standard comparisons on this page. For every $p > 0$ and every positive rational $\alpha$ , $n^{\alpha}/(1+p)^n \to 0$ says a power is beaten by a geometric sequence; this says every geometric sequence, that is every fixed $x$ , is beaten by the factorial. Instances are worked in The four standard limits $n^{1/n} \to 1$ , $a^{1/n} \to 1$ , $n^{\alpha}/(1+p)^n \to 0$ and $x^k/k! \to 0$ , computed ↗.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 93 results over 28 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

Factorial (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §6.5 (standard reference, not scraped)

For every real xxx, xk/k!→0x^k/k! \to 0xk/k!→0