TheoremStatement: Literature-sourcedProof: 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.

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$

Statement

Let $A \subseteq R$ , let $c \in A$ be a limit point of $A$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ), let $f, g : A \to R$ be differentiable at $c$ (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) and let $α \in R$ . Then:

$f + g$ is differentiable at $c$ and $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ ;
$α f$ is differentiable at $c$ and $(α f)^{'} (c) = α f^{'} (c)$ ;
$f g$ is differentiable at $c$ and $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ ;
if $g (c) \neq 0$ then, writing $A_{0} : = {x \in A : g (x) \neq 0}$ , the point $c$ lies in $A_{0}$ and is a limit point of $A_{0}$ , the quotient $(f / g) ∣_{A_{0}} : A_{0} \to R$ , $x \mapsto f (x) / g (x)$ , is differentiable at $c$ as a function on $A_{0}$ , and $((f / g) ∣_{A_{0}})^{'} (c) = \frac{f^{'} (c) g (c) - f (c) g^{'} (c)}{g (c)^{2}} .$

Each claim asserts two things: that the derivative on the left exists, and that it has the stated value. Both are proved.

Why claim 4 is stated on $A_{0}$ . The function $f / g$ is not defined where $g$ vanishes, and $g$ may vanish at points of $A$ far from $c$ ; restricting to $A_{0}$ is forced. That the restriction still has $c$ as a limit point, so that a derivative there means anything at all, is not free either, and it is the last claim of If $\lim_{x \to c} f (x) = L \neq 0$ then $∣ f ∣ > ∣ L ∣ / 2$ on a punctured neighbourhood of $c$ ; in particular if $L > 0$ then $f > L / 2 > 0$ there applied to $g$ . The hypothesis is $g (c) \neq 0$ , not " $g$ vanishes nowhere".

Everything is proved through Carathéodory's characterisation: $f$ is differentiable at $c$ if and only if there is $φ : A \to R$ , continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ for every $x \in A$ , and then $φ$ is unique and $φ (c) = f^{'} (c)$ . No difference quotient is estimated and no limit theorem beyond continuity is used, so no choice principle is spent. The four identities are four algebraic rearrangements of an increment, each followed by a reading of Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function.

Facts & Assumptions

Given: A set $A \subseteq R$ , a point $c \in A$ that is a limit point of $A$ , functions $f, g : A \to R$ differentiable at $c$ , and a real $α$ ; for claim 4 also the hypothesis $g (c) \neq 0$ together with $A_{0} : = {x \in A : g (x) \neq 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, Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ).

[L1]

Carathéodory's characterisation (Carathéodory's characterisation: $f$ is differentiable at $c$ if and only if there is $φ : A \to R$ , continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ for every $x \in A$ , and then $φ$ is unique and $φ (c) = f^{'} (c)$ ), used in both directions: for a set $B \subseteq R$ , a point $p \in B$ that is a limit point of $B$ and a function $h : B \to R$ , the function $h$ is differentiable at $p$ if and only if there is $η : B \to R$ , continuous at $p$ , with $h (x) - h (p) = η (x) (x - p)$ for every $x \in B$ , and then $η (p) = h^{'} (p)$ .

[L2]

Algebra of continuous functions (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function): sums, scalar multiples and products of functions continuous at a point are continuous there (claim 1); every constant function and the identity are continuous everywhere on the domain (claim 5); and if $u, v$ are continuous at a point $p$ of their common domain $D$ with $v (p) \neq 0$ , then $p$ lies in $D_{0} : = {x \in D : v (x) \neq 0}$ and $(u / v) ∣_{D_{0}}$ is continuous at $p$ as a function on $D_{0}$ (claim 4).

[L3]

Continuity passes to a subset of the domain: if $B \subseteq A$ , if $p \in B$ and if $ψ : A \to R$ is continuous at $p$ , then $ψ ∣_{B}$ is continuous at $p$ , the condition on the restriction quantifying over fewer points (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point).

[L4]

A function differentiable at $c$ is continuous at $c$ (A function differentiable at $c$ is continuous at $c$ ); in particular $g$ is.

[L5]

At a limit point $c$ of $A$ , continuity of $g$ at $c$ says exactly that $\lim_{x \to c} g (x)$ exists and equals $g (c)$ (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point, clause 1, The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ).

[L6]

Sign preservation (If $\lim_{x \to c} f (x) = L \neq 0$ then $∣ f ∣ > ∣ L ∣ / 2$ on a punctured neighbourhood of $c$ ; in particular if $L > 0$ then $f > L / 2 > 0$ there): if $c$ is a limit point of $A$ and $\lim_{x \to c} g (x)$ exists and is nonzero, then $c$ is a limit point of $A_{0} = {x \in A : g (x) \neq 0}$ .

[L7]

A product of two nonzero reals is nonzero (A field has no zero divisors: $a b = 0 \Rightarrow a = 0$ or $b = 0$ ), and $g (c)^{2} = g (c) g (c)$ (Integer powers $a^{m}$ ).

Proof

technique · direct

1.1

By [L1], applied to $f$ and to $g$ on $A$ at $c$ , fix $φ, ψ : A \to R$ , both continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ and $g (x) - g (c) = ψ (x) (x - c)$ for every $x \in A$ , and with $φ (c) = f^{'} (c)$ and $ψ (c) = g^{'} (c)$ .

L1choose

1.2

Assume $g (c) \neq 0$ . Then $c \in A_{0}$ by the definition of $A_{0}$ ; $g$ is continuous at $c$ by [L4], so $\lim_{x \to c} g (x) = g (c) \neq 0$ by [L5]; and therefore $c$ is a limit point of $A_{0}$ by [L6].

L4L5L6

2.1

Sum. For every $x \in A$ , $(f + g) (x) - (f + g) (c) = (f (x) - f (c)) + (g (x) - g (c)) = (φ (x) + ψ (x)) (x - c)$ . The function $φ + ψ$ is continuous at $c$ by [L2], and $(φ + ψ) (c) = f^{'} (c) + g^{'} (c)$ . So [L1] gives claim 1.

step 1.1L1L2

2.2

Scalar multiple. For every $x \in A$ , $(α f) (x) - (α f) (c) = α (f (x) - f (c)) = (α φ (x)) (x - c)$ . The function $α φ$ is continuous at $c$ by [L2], with value $α f^{'} (c)$ there. So [L1] gives claim 2.

step 1.1L1L2

2.3

Product. For every $x \in A$ , $f (x) g (x) - f (c) g (c) = (f (x) - f (c)) g (x) + f (c) (g (x) - g (c)) = (φ (x) g (x) + f (c) ψ (x)) (x - c)$ . Put $χ : = φ g + f (c) ψ$ ; it is continuous at $c$ by [L2], since $φ$ , $ψ$ and (by [L4]) $g$ are, and constants are; and $χ (c) = φ (c) g (c) + f (c) ψ (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ . So [L1] gives claim 3.

step 1.1L1L2L4

2.4

Quotient, the rearrangement. Assume $g (c) \neq 0$ and let $x \in A_{0}$ , so $g (x) \neq 0$ and $g (c) \neq 0$ . Then $f (x) / g (x) - f (c) / g (c) = (f (x) g (c) - f (c) g (x)) / (g (x) g (c))$ , and $f (x) g (c) - f (c) g (x) = (f (x) - f (c)) g (c) - f (c) (g (x) - g (c)) = (φ (x) g (c) - f (c) ψ (x)) (x - c)$ . So, defining $θ : A_{0} \to R$ by $θ (x) : = (φ (x) g (c) - f (c) ψ (x)) / (g (x) g (c))$ , one has $(f / g) ∣_{A_{0}} (x) - (f / g) ∣_{A_{0}} (c) = θ (x) (x - c)$ for every $x \in A_{0}$ .

step 1.1L1L7

2.5

Quotient, continuity of the factor. Assume $g (c) \neq 0$ . The restrictions of $φ$ , $ψ$ and $g$ to $A_{0}$ are continuous at $c \in A_{0}$ by [L3] and [L4], so by [L2] the numerator $u (x) : = φ (x) g (c) - f (c) ψ (x)$ and the denominator $v (x) : = g (x) g (c)$ are continuous at $c$ as functions on $A_{0}$ . By [L7] the denominator vanishes at no point of $A_{0}$ , so ${x \in A_{0} : v (x) \neq 0} = A_{0}$ , and $v (c) = g (c)^{2} \neq 0$ ; hence claim 4 of [L2] gives that $θ = (u / v) ∣_{A_{0}}$ is continuous at $c$ , with $θ (c) = (φ (c) g (c) - f (c) ψ (c)) / g (c)^{2} = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ .

step 1.1step 1.2L2L3L4L7

3.1

Quotient, conclusion. Assume $g (c) \neq 0$ . By step 1.2 the point $c$ lies in $A_{0}$ and is a limit point of $A_{0}$ ; by steps 2.4 and 2.5 the function $θ : A_{0} \to R$ is continuous at $c$ and factors the increment of $(f / g) ∣_{A_{0}}$ . So [L1], applied on the domain $A_{0}$ at the point $c$ , gives that $(f / g) ∣_{A_{0}}$ is differentiable at $c$ with derivative $θ (c)$ : claim 4.

step 1.2step 2.4step 2.5L1

4.1

Claims 1 to 4 are proved, by steps 2.1, 2.2, 2.3 and 3.1 respectively, each by exhibiting the Carathéodory factor of the new function and reading its continuity at $c$ off the algebra of continuous functions.

step 2.1step 2.2step 2.3step 3.1∎

Remarks

The product rearrangement in one line. The identity $f g - f (c) g (c) = (f - f (c)) g + f (c) (g - g (c))$ splits the increment of a product into two increments, one multiplied by $g$ and one by a constant. It is the same identity that carries the product case of Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero, read at the level of increments rather than of $ε$ ; here the factor $g$ has to be continuous at $c$ rather than merely bounded near it, and A function differentiable at $c$ is continuous at $c$ is what supplies that.
The reciprocal is the case $f \equiv 1$ . Claim 4 then reads $((1 / g) ∣_{A_{0}})^{'} (c) = - g^{'} (c) / g (c)^{2}$ , since $f^{'} (c) = 0$ for a constant $f$ ; nothing separate has to be proved, and the derivative of a negative integer power on this page is obtained exactly this way.
Two hypotheses that look removable and are not. In claim 4 the hypothesis $g (c) \neq 0$ cannot be weakened to " $g$ is nonzero somewhere near $c$ ", because $c$ itself must lie in the smaller domain for a derivative there to be a statement about $c$ ; and the conclusion is about $(f / g) ∣_{A_{0}}$ , not about any extension of it to $A$ , since no such extension is canonical.

Depends on

Used by

…and 102 more results.

Dependency tree · two levels

37 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

Product rule (Wikipedia) (standard reference, not scraped)
Quotient rule (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 5 (Thm 5.3) (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)