LemmaStatement: AI-adaptedProof: AI-generatedprecheck 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 $ι (n) : = n \cdot 1_{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} ι (j + 1) (k \in N),$

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

$\frac{x^{k}}{k!} ⟶ 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 ∣ \geq 0$ ; the factorials $k! = \prod_{j < k} ι (j + 1)$ ; and the canonical naturals $ι (n) = n \cdot 1_{R}$ .

[A1]

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

[L1]

Finite products: the empty product is $1$ , $\prod_{j < m + 1} a_{j} = (\prod_{j < m} a_{j}) 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 \geq 0$ implies $z^{m} \geq 0$ (Integer powers $a^{m}$ , Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ , Laws of integer exponents).

[L3]

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

[L4]

Induction principle (The principle of mathematical induction).

[L5]

Canonical naturals: $ι (n) > 0$ and invertible for $n \geq 1$ , $ι$ is strictly increasing, and for every real $y$ there is a natural $N \geq 1$ with $y < ι (N)$ (Canonical naturals are positive and strictly increasing, Every complete ordered field is Archimedean, Order on the natural numbers, $\leq$ is a linear order on $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 $\leq$ . 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.1givenL1L3L5

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

1.2givenL2L3L4

For every $k \in 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$ .

1.3givenL1L2L5L6choose

Take a natural $N \geq 1$ with $M < ι (N)$ and put $λ : = M / ι (N)$ and $A : = M^{N} / N!$ . Then $0 \leq λ < 1$ , since $0 \leq M < ι (N)$ and $ι (N) > 0$ , and $A \geq 0$ .

1.4givenA1L2base

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

1.5A1ih

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

2.1step 1.5A1L1L2L5L6

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

3.1step 1.4step 2.1A1L1L2L4

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

4.1step 3.1step 1.1step 1.2L3L7L8L9discharge-induction∎

Since $∣ λ ∣ = λ < 1$ , the sequence $(λ^{j})_{j}$ converges to $0$ , hence so does $(A λ^{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$ .

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 $ι (N)$ , so multiplying by $x$ and dividing by that factor shrinks the term by at least the factor $λ = M / ι (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 \leq 1 / 2$ ; here it is enough to take $N$ with $M < ι (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$ , $λ = 0$ and the bound reads $M^{N + j} / (N + j)! \leq 0$ for $j \geq 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 $α$ , $n^{α} / (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^{α} / (1 + p)^{n} \to 0$ and $x^{k} / k! \to 0$ , computed ↗.

For every real $x$ , $x^{k} / k! \to 0$

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

For every real xx, xk/k!→0xk/k!→0

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

For every real $x$ , $x^{k} / k! \to 0$