Proof of $\frac{d \sqrt{x}}{dx}$ including proof of the limit? Looking at proofs for $\frac{d \sqrt{x}}{dx}$, ($0<x$) they often get to this point:
$$ \frac{d \sqrt{x}}{dx} = \lim_{h \to 0}\frac{1}{\sqrt{x} + \sqrt{x + h}} $$
At this point magical limits are taken. Unfortunately I'm trying to prove this in Coq so need to use a formal definition of the limit e.g. the limit of $f(x)$ at $c$ is $l$ means:
$$\forall \epsilon > 0,\ \exists \delta \ s.t.\ |x-c|<\delta \Rightarrow |f(x) -l| < \epsilon$$
I think that this gives me the following:
$$|h| < \delta \Rightarrow \left| \frac{1}{\sqrt{x} + \sqrt{x + h}} - \frac{1}{2\sqrt{x}} \right| < \epsilon $$
It's at this point that I get stuck trying to find a $\delta$ to satisfy this equation. Any help would be appreciated.
 A: HINT:
$$\begin{align}
\left|\frac{1}{\sqrt{x+h}+\sqrt{x}}-\frac{1}{2\sqrt{x}}\right|&=\left|\frac{\sqrt{x}-\sqrt{x+h}}{2\sqrt{x}(\sqrt{x+h}+\sqrt{x})}\right|\\\\
&=\left|\frac{h}{2\sqrt{x}(\sqrt{x+h}+\sqrt{x})^2}\right|\\\\
&\le \frac{|h|}{2x^{3/2}}
\end{align}$$
A: Suppose we could prove the following lemma:
If $\lim_{h\rightarrow a} f(h) = m$ then
i) $\lim_{h\rightarrow a} (f(h) + w) = m + w = (\lim_{h\rightarrow a} f(h)) + w$.
ii) if $m \ge 0$ then $\lim_{h\rightarrow a}\sqrt{h} = \sqrt{m} = \sqrt{\lim_{h\rightarrow a}f(h)}$
iii) if $m \ne 0$ then $\lim_{h\rightarrow a}\frac{1}{f(h)} = 1/m = \frac 1{\lim_{h\rightarrow a}f(h)}$
Then we'd pretty much be done.  
$\lim_{h\rightarrow 0}(x + h) = x + \lim_{h\rightarrow 0} h = x + 0=x$
$\lim_{h\rightarrow 0}\sqrt{x + h} = \sqrt{\lim_{h\rightarrow 0}(x+h)} = \sqrt{x}$
$\lim_{h\rightarrow 0}(\sqrt{x} + \sqrt{x+h}) = \sqrt{x} + \lim_{h\rightarrow 0}\sqrt{x + h} = \sqrt{x} + \sqrt{x} = 2\sqrt{x}$.
$\lim_{h\rightarrow 0}\frac 1{\sqrt{x} + \sqrt{x+h}} = \frac 1{\lim_{h\rightarrow 0}(\sqrt{x} + \sqrt{x+h})} = 1/2\sqrt{x}$.
Done.  
Must prove lemmma.
i) For $\epsilon > 0$ there is a $\delta$ so that $|h - a| < \delta \implies |f(h) - m| < \epsilon$ so $|h-a| < \delta \implies |(f(h)+w)-(m+w)|= |f(h) -m| < \epsilon$.
ii) For $2\sqrt{m} > \epsilon > 0$ let $\gamma = 2\sqrt{m}\epsilon - \epsilon^2 > 0$.
There is a $\delta$ so that $|h - a| < \delta \implies |f(h) - m| < \gamma$
$\implies m - \gamma < f(h) < m + \gamma $
$\implies (\sqrt{m} - \epsilon)^2 = m - 2\sqrt{m}\epsilon + \epsilon^2 < f(h) < m + 2\sqrt{m}\epsilon - \epsilon^2 < m + 2\sqrt{m}\epsilon + \epsilon^2=(\sqrt{m} + \epsilon)^2$
$\implies \sqrt{m} - \epsilon < f(h) < \sqrt{m} + \epsilon$
$\implies |f(h) - \sqrt{m}| < \epsilon$.
iii)  For $ \epsilon > 0$.  Let $\epsilon_2 =   \min(|m|/2, m^2*\epsilon/2) > 0$.  (Remember $m \ne 0$, so we can be assured $\epsilon_2 > 0$.) 
We can find a $\delta$ so that $|h-a| < \delta \implies |f(h) - m| < \epsilon_2$. 
So $|h-a| < \delta \implies |f(h) - m| < \epsilon_2 \le |m|/2 \implies |f(h)| > |m|/2$.
So if $|h - a| < \delta$ then
$|\frac 1{f(h)} - \frac 1m| = |\frac{m - f(h)}{m*f(h)}| = |m - f(h)|*\frac 1{|m*f(h)|}$
$< |m-f(h)|*\frac 1{m^2/2} < \epsilon_2*\frac 2{m^2}$
$\le  \frac{m^2\epsilon}{2}*\frac 2{m^2}=\epsilon$.
So we proved the lemma and thus the result.
===
Actually let's see what Mr. Rudin says.  In Principles of Mathematical Analysis by walter rudin we have in chapter 4.
Theorem 4.4.  Suppose $E \subset X$ a metric space (we'll just say $X$ and $E$ are $\mathbb R$), $p$ is a limit point of $E$ (that just means we talk about $x \rightarrow p$), $f$ and $g$ are complex functions on $E$ (let's just say $f$ and $g$ are real functions) and 
$\lim_{x \rightarrow p}f(x) = A$, $\lim_{x\rightarrow p}g(x) = B$ then
a) $\lim_{x \rightarrow p}(f + g)(x)=A+B$
b) $\lim_{x\rightarrow p}(fg)(x) = AB$
c) $\lim_{x\rightarrow p}(f/g)(x) = A/B$ if $B\ne 0$.
The proof of a) and c) are as I gave them.  b) is pretty basic and similar.
Then Def 4.5 defines continuous functions.  ($f$ is continuous at $p$, if for every $\epsilon > 0$ there exists a $\delta > 0$ so that for all $x$ where $d(x,p)< \delta$ it follows that $d(f(x),f(p)) < \epsilon$)
Theorem 4.6: $f$ is continuous at $p$ if and only if $\lim_{x\rightarrow p}f(x) = f(p)$.  This follows purely by definitions.
Thereom 4.7: says that composition of continuous functions are continuous.  The proof is simple.  Basically you find $\epsilon, \gamma, \delta$ so that $|x-p|< \gamma \implies |f(x) - f(p)| < \epsilon$ and $|x-p|<\delta \implies |h(x) - h(p)|<\gamma$ there for $|x-p| < \delta \implies |h(x) - h(p)| < \gamma \implies |f(h(x)) - f(h(p))| < \epsilon$ so $f(h(x))$ is continuous at $p$..
With those we just have to show $\sqrt{x}$ is continuous which is basically my lemma ii).
A: Not having used Coq and only having the slightest idea about theorem provers....
Humans don't resort to epsilon delta proofs unless they need to. They spend lots of time learning the various interesting algebraic properties that limits, etc have.
Although it's not phrased this way at first, one of the first key ideas a student learns is, for spaces $X$ and $Y$, there is a subtype $\mathcal{C}(X, Y) \subseteq Y^X$ of continuous functions. Then we have


*

*The restriction of the limit to $\mathcal{C}(X, Y) \times X \to Y$ is a total function that is identical to the restriction of the evaluation map $Y^X \times X \to Y$

*Composition of functions restricts to a map $\mathcal{C}(Y,Z) \times \mathcal{C}(X,Y) \to \mathcal{C}(X, Z)$


Together with basic facts you should have proven prior:


*

*Addition is an element of $\mathcal{C}(\mathbb{R} \times \mathbb{R}, \mathbb{R})$

*Division is an element of $\mathcal{C}(\mathbb{R} \times (\mathbb{R} \setminus \{0\})), \mathbb{R})$

*The square root is an element of $\mathcal{C}(\mathbb{R}_{\geq 0}, \mathbb{R})$

*Constant functions are elements of $\mathcal{C}(\{ * \}, \mathbb{R})$


you can prove that, for every $x > 0$,
$$ h \mapsto \frac{1}{\sqrt{x+h} + \sqrt{x}} $$
is an element of $\mathcal{C}((-x, \infty), \mathbb{R})$.
