LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

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 a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term

Statement

Powers are those of Integer powers $a^{m}$ , and $ι : N \to R$ is the canonical natural of The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, so that $ι (0) = 0$ and $ι (m + 1) = ι (m) + 1$ . Let $n \in N$ .

The function $p_{0} : R \to R$ , $p_{0} (x) = x^{0}$ , is the constant function $1$ , and it is differentiable at every $c \in R$ with $p_{0}^{'} (c) = 0$ (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set).
For $n \geq 1$ the function $p_{n} : R \to R$ , $p_{n} (x) = x^{n}$ , is differentiable at every $c \in R$ , and $p_{n}^{'} (c) = ι (n) c^{n - 1} .$
For $n \geq 1$ put $A_{0} : = {x \in R : x \neq 0}$ . The function $m_{n} : A_{0} \to R$ , $m_{n} (x) = x^{- n}$ , is differentiable at every $c \in A_{0}$ as a function on $A_{0}$ , and $m_{n}^{'} (c) = - ι (n) c^{- n - 1} .$
Let $a : N \to R$ with $a_{j} = 0$ for $j \geq n$ , and let $P : R \to R$ be the polynomial function $P (x) = \sum_{j < n} a_{j} x^{j}$ (Finite sums and finite products, by recursion). Then $P$ is differentiable at every $c \in R$ , and, defining $e : N \to R$ by $e_{0} : = 0$ and $e_{j} : = ι (j) a_{j} c^{j - 1}$ for $j \geq 1$ , $P^{'} (c) = \sum_{j < n} e_{j} .$

Claim 2 is stated for $n \geq 1$ and not for $n \geq 0$ , and that is not timidity. At $n = 0$ its right-hand side reads $ι (0) c^{- 1}$ , and $c^{- 1}$ is not defined at $c = 0$ (Integer powers $a^{m}$ ), so the formula is not a statement about the whole line. Claim 1 is what covers $n = 0$ , and it says the derivative is $0$ there, which is what the informal reading " $0 \cdot c^{- 1}$ " is reaching for. The same shift is why the term $e_{0}$ of claim 4 is defined to be $0$ outright rather than by the formula.

Facts & Assumptions

Given: A natural $n$ , a real $c$ , and the functions $p_{n}$ , $m_{n}$ and $P$ of the statement.

[L1]

Powers (Integer powers $a^{m}$ ): $a^{0} = 1$ and $a^{m + 1} = a^{m} a$ for every $a \in R$ and $m \in N$ ; $a^{- m} : = (a^{m})^{- 1}$ for $a \neq 0$ and $m \geq 1$ ; and $0^{m} = 0$ for $m \geq 1$ .

[L2]

Canonical naturals (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field): $ι (0) = 0$ , $ι (m + 1) = ι (m) + 1$ , and hence $ι (1) = 1$ .

[L3]

Algebra of derivatives (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ): at a limit point $c$ of the common domain, sums, scalar multiples and products of functions differentiable at $c$ are differentiable at $c$ with the four stated formulas, and if the denominator is nonzero at $c$ then the quotient, restricted to the set where the denominator does not vanish, is differentiable at $c$ with the quotient formula; that restricted set has $c$ as a limit point.

[L4]

Derivative and difference quotient (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set): $f$ is differentiable at a limit point $c$ of its domain $D$ exactly when the difference quotient $x \mapsto (f (x) - f (c)) / (x - c)$ , a function on $D ∖ {c}$ , has a limit at $c$ , and $f^{'} (c)$ is that limit. A constant function $h \equiv K$ on a set having $c$ as a limit point has $\lim_{x \to c} h (x) = K$ : given a real $ε > 0$ , any real $δ > 0$ serves, since $∣ K - K ∣ = 0 < ε$ (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ).

[L5]

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

[L6]

Finite sums (Finite sums and finite products, by recursion): $\sum_{j < 0} b_{j} = 0$ and $\sum_{j < m + 1} b_{j} = (\sum_{j < m} b_{j}) + b_{m}$ .

[L7]

Integer exponent laws for a nonzero base (Laws of integer exponents): $a^{k} \neq 0$ for every $k \in N$ when $a \neq 0$ ; and for integers $j, k$ one has $a^{j} a^{k} = a^{j + k}$ , $(a^{j})^{k} = a^{j k}$ and $a^{- k} = (a^{k})^{- 1}$ .

[L8]

Every real is a limit point of $R$ , punctured neighbourhoods in $R$ being never empty (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ , The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ).

Proof

technique · induction

1.1

Base case, claim 2 at $n = 1$ . By [L1], $x^{1} = x^{0} x = 1 \cdot x = x$ , so $p_{1}$ is the identity. Fix $c \in R$ ; for every $x \neq c$ the difference quotient is $(x - c) / (x - c) = 1$ , so it is the constant function $1$ on $R ∖ {c}$ , and by [L4] and [L8] its limit at $c$ is $1$ . Since $ι (1) c^{0} = 1 \cdot 1 = 1$ by [L1] and [L2], claim 2 holds at $n = 1$ .

baseL1L2L4L8

1.2

Inductive hypothesis. Fix a natural $n \geq 1$ and assume that $p_{n}$ is differentiable at every $c \in R$ with $p_{n}^{'} (c) = ι (n) c^{n - 1}$ .

1.3

Claim 1. By [L1] the function $p_{0}$ is the constant function $1$ . Fix $c \in R$ ; for every $x \neq c$ its difference quotient is $(1 - 1) / (x - c) = 0$ , the constant function $0$ on $R ∖ {c}$ , whose limit at $c$ is $0$ by [L4] and [L8]. So $p_{0}$ is differentiable at every $c$ with $p_{0}^{'} (c) = 0$ .

L1L4L8

2.1

Successor step. Let $c \in R$ . By [L1], $p_{n + 1} (x) = x^{n + 1} = x^{n} x = p_{n} (x) p_{1} (x)$ for every $x$ . Both factors are differentiable at $c$ , by step 1.2 and step 1.1, so the product rule of [L3] gives that $p_{n + 1}$ is differentiable at $c$ with $p_{n + 1}^{'} (c) = p_{n}^{'} (c) p_{1} (c) + p_{n} (c) p_{1}^{'} (c) = ι (n) c^{n - 1} c + c^{n} \cdot 1$ . Now $c^{n - 1} c = c^{(n - 1) + 1} = c^{n}$ by [L1], so the right-hand side is $ι (n) c^{n} + c^{n} = (ι (n) + 1) c^{n} = ι (n + 1) c^{n}$ by [L2].

step 1.1step 1.2L1L2L3

3.1

Claim 2. Steps 1.1 and 2.1 are the base case and the successor step of an induction over the naturals $n \geq 1$ , so by [L5] the function $p_{n}$ is differentiable at every $c \in R$ with $p_{n}^{'} (c) = ι (n) c^{n - 1}$ , for every natural $n \geq 1$ .

step 1.1step 2.1L5

4.1

Claim 3. Let $n \geq 1$ . The set ${x \in R : p_{n} (x) \neq 0}$ is exactly $A_{0}$ : a nonzero $x$ has $x^{n} \neq 0$ by [L7], and $0^{n} = 0$ by [L1]. Fix $c \in A_{0}$ . The constant function $1$ on $R$ is differentiable at $c$ with derivative $0$ by step 1.3, and $p_{n}$ is differentiable at $c$ with derivative $ι (n) c^{n - 1}$ by step 3.1, with $p_{n} (c) = c^{n} \neq 0$ . So the quotient rule of [L3] applies: the function $x \mapsto 1 / x^{n}$ on $A_{0}$ , which by [L1] and [L7] is $m_{n}$ , is differentiable at $c$ with derivative $(0 \cdot c^{n} - 1 \cdot ι (n) c^{n - 1}) / (c^{n})^{2} = - ι (n) c^{n - 1} (c^{2 n})^{- 1} = - ι (n) c^{n - 1 - 2 n} = - ι (n) c^{- n - 1}$ , where $(c^{n})^{2} = c^{2 n}$ and $c^{n - 1} c^{- 2 n} = c^{- n - 1}$ are [L7].

step 1.3step 3.1L1L3L7

4.2

Claim 4, by a second induction on $n$ . Fix $c \in R$ and the sequence $a$ . At $n = 0$ the sum $P (x) = \sum_{j < 0} a_{j} x^{j}$ is $0$ for every $x$ by [L6], so $P$ is the constant function $0$ and, as in step 1.3, $P^{'} (c) = 0 = \sum_{j < 0} e_{j}$ . Suppose the claim holds at $n$ , and let $P_{n + 1} (x) : = \sum_{j < n + 1} a_{j} x^{j}$ . By [L6], $P_{n + 1} (x) = P_{n} (x) + a_{n} x^{n}$ for every $x$ , where $P_{n} (x) = \sum_{j < n} a_{j} x^{j}$ . The function $x \mapsto a_{n} x^{n}$ is differentiable at $c$ with derivative $e_{n}$ : for $n = 0$ it is the constant $a_{n}$ , of derivative $0 = e_{0}$ , by step 1.3 and the scalar rule of [L3]; for $n \geq 1$ it is the scalar multiple $a_{n} p_{n}$ , of derivative $a_{n} ι (n) c^{n - 1} = e_{n}$ , by step 3.1 and the scalar rule of [L3]. The inductive hypothesis gives $P_{n}^{'} (c) = \sum_{j < n} e_{j}$ , so the sum rule of [L3] gives that $P_{n + 1}$ is differentiable at $c$ with $P_{n + 1}^{'} (c) = \sum_{j < n} e_{j} + e_{n} = \sum_{j < n + 1} e_{j}$ by [L6]. By [L5] claim 4 holds for every $n \in N$ .

step 1.3step 3.1L3L5L6

5.1

All four claims are established: claim 1 by step 1.3, claim 2 by step 3.1, claim 3 by step 4.1 and claim 4 by step 4.2.

step 1.3step 3.1step 4.1step 4.2discharge-induction∎

Remarks

Why the induction starts at $n = 1$ and not at $n = 0$ . The successor step multiplies by the identity, and the identity is $p_{1}$ ; starting at $n = 0$ would require the formula of claim 2 to hold at $n = 0$ , which it does not, since $c^{- 1}$ is undefined at $c = 0$ . The two statements are therefore kept apart, and claim 1 is proved on its own from the definition. This is the same index care that The canonical natural $ι (n) = n \cdot 1_{F}$ of a field records for families of reciprocals: $N$ contains $0$ , and a formula written for " $n$ " is a claim about $n = 0$ unless it says otherwise.
The negative exponents cost nothing extra. Claim 3 is the quotient rule of Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ applied with numerator the constant $1$ , and the domain it produces, the set where $x^{n}$ does not vanish, is exactly $R ∖ {0}$ ; no separate argument and no separate limit is needed. Rational exponents are a different matter, resting on Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ , and are treated on the companion page rather than here.
Claim 4 is a statement about a finite sum, not about an infinite one. Nothing here says anything about differentiating a series term by term; that is a separate question, needing hypotheses about convergence that this page does not have and does not assume.

Depends on

Used by

…and 44 more results.

Dependency tree · two levels

43 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

Power rule (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 5 (standard reference, not scraped)
J. Lebl, Basic Analysis I, §4.1 (standard reference, not scraped)
J. Lebl, Basic Analysis I, The Derivative (standard reference, not scraped)