Worked derivatives from the algebra of derivatives and the power rule: $(3x^{4} - 5x + 2)' = 12x^{3} - 5$, and the quotient rule applied to $(x^{2}+1)/(x-1)$ on $\mathbb{R} \setminus \{1\}$

Numerals below denote canonical naturals of $\mathbb{R}$: $3$ is $\iota(3)$, $12$ is $\iota(12)$, and so on (The canonical natural $\iota(n) = n \cdot 1_F$ of a field). Powers are those of Integer powers $a^m$.

Claim 1. Let $p : \mathbb{R} \to \mathbb{R}$ be given by

$p(x) \;=\; \iota(3)\,x^{4} \;-\; \iota(5)\,x \;+\; \iota(2) .$

Then $p$ is differentiable at every $c \in \mathbb{R}$ (The derivative $f'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c}$ of $f : A \to \mathbb{R}$ at a point $c \in A$ that is a limit point of $A$, and differentiability on a set) and

$p'(c) \;=\; \iota(12)\,c^{3} - \iota(5) .$

Claim 2. Put $A_0 := \{\, x \in \mathbb{R} : x - 1 \ne 0 \,\} = \mathbb{R} \setminus \{1\}$ and let $r : A_0 \to \mathbb{R}$ be given by $r(x) = (x^{2}+1)/(x-1)$. Then every $c \in A_0$ is a limit point of $A_0$, $r$ is differentiable at $c$ as a function on $A_0$, and

$r'(c) \;=\; \frac{c^{2} - \iota(2)c - 1}{(c-1)^{2}} .$

Nothing here is new: both computations are readings of Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$ on top of For a natural $n \ge 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $\iota(n)\,x^{\,n-1}$; for $n = 0$ it is the constant $1$, with derivative $0$; for a natural $n \ge 1$ the function $x \mapsto x^{-n}$ is differentiable at every $x \ne 0$ with derivative $-\iota(n)\,x^{-n-1}$; consequently every polynomial function is differentiable at every real, with the derivative computed term by term. They are written out because the two places a computation of this kind goes wrong are the constant term, whose derivative is $0$ and not $\iota(0)c^{-1}$, and the domain of the quotient, which is not $\mathbb{R}$.

• The constant term is where the index trap sits. Written informally, the derivative of $\iota(2)x^{0}$ "is" $\iota(2)\iota(0)x^{-1}$, and $x^{-1}$ is undefined at $0$. Claim 1 of For a natural $n \ge 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $\iota(n)\,x^{\,n-1}$; for $n = 0$ it is the constant $1$, with derivative $0$; for a natural $n \ge 1$ the function $x \mapsto x^{-n}$ is differentiable at every $x \ne 0$ with derivative $-\iota(n)\,x^{-n-1}$; consequently every polynomial function is differentiable at every real, with the derivative computed term by term exists precisely so that the constant case is handled by its own statement, and the answer there is $0$ on the whole line.

• The quotient lives on $\mathbb{R} \setminus \{1\}$, not on $\mathbb{R}$. The function $r$ is not defined at $1$, and no derivative of it there is asserted or could be. Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$ states its quotient case on the set where the denominator does not vanish for exactly this reason, and it also supplies the fact that the smaller set still has $c$ as a limit point, without which the derivative there would not be a defined symbol.

• Reading the numerals. $\iota(12)$ is what "$12$" means as an element of $\mathbb{R}$; the equality $\iota(3)\iota(4) = \iota(12)$ is a lemma (Canonical naturals are positive and strictly increasing) and not an act of arithmetic on the page. Every numeral in this library is such an image, and where a computation multiplies two of them the lemma is what licenses collapsing the product.