# Quantified definition of the derivative

How do you quantify:

A function $f:\mathrm{dom}(f) \longrightarrow \mathrm{codom}(f)$ is differentiable at every $x$ contained in $\mathrm{dom}(f)$ if the limit $$\lim_{h \to 0}\frac{f(x+h)-f(x)}{h}$$ exists.

I have looked everywhere for a quantified definition of the above and have only found quantified versions that don't utilize the limit as $h$ approaches zero. Here is my attempt:

$$(\forall \varepsilon > 0)(\exists \delta > 0)(\forall x)\left( |h| < \delta \Rightarrow \left| f'(x) - \frac{f(x + h) - f(x)}{h} \right| < \varepsilon \right).$$

I believe this to be correct however as I am teaching myself analysis, I am being extra cautious with everything.

-
$(\forall x) (\forall \epsilon >0) (\exists \delta>0)(|h|<\delta \Rightarrow |f(x+h)-f(x)-f'(x)h| < \epsilon |h|)$. The $x$ quantifier appears before the $\delta$ one unless there is some uniformity involved. Also, multiplying through by $|h|$ avoids having to add the restriction $h \neq 0$. – copper.hat Jul 15 '12 at 0:01
what if I AND'ed the premise (h not equal to 0) with the antecedent? would this allow me to keep h in the denominator? – skyfire Jul 15 '12 at 0:09
@skyfire: The definition of $\lim\limits_{t\to a}f(t) = L$ is: $$\forall\epsilon\gt 0\exists\delta\gt 0\left( 0\lt |t-a|\lt \delta\implies |f(t)-L|\lt\epsilon\right).$$ In the definition, you include the exclusion of the case $t=a$. Here, you do need to exclude $h=0$, otherwise, the formula never holds because we can let $h=0$, in which case the premise of the implication holds, but the consequent is false, so the implication is false, so the formula is false. – Arturo Magidin Jul 15 '12 at 0:11

One problem is that $f'(x)$ is free in your formula; another second problem is that you need to exclude the limit point $0$ (that is, you need to exclude $h=0$).
Since the definition says that a certain thing exists, the correct quantification should start with an existential, followed by the definition of "the limit is equal to"; since the limit may depend on the $x$, the existential must follow the $x$. $$(\forall x)(\exists L)(\forall\epsilon\gt 0)(\exists\delta\gt 0)\left( 0\lt |h|\lt \delta\implies \left|\frac{f(x+h)-f(x)}{h} - L\right|\lt\epsilon\right).$$
That is: for every $x$, there is a real number $L$ such that the corresponding limit exists and is equal to $L$.
Alternatively, you can rewrite "$0\lt |h|\lt \delta$" as $(|h|\lt \delta\land h\neq 0)$", or any formula that amounts to "the absolute value of $h$ is smaller than $\delta$ and $h$ is not zero".