ThmDex – An index of mathematical definitions, results, and conjectures.
Cauchy's real mean value theorem

Let $[a, b] \subseteq \mathbb{R}$ be a D544: Closed real interval such that
 (i) $$a < b$$ (ii) $f, g : [a, b] \to \mathbb{R}$ are each a D5231: Standard-continuous real function on $[a, b]$ (iii) $f, g$ are each a D5614: Differentiable real function on $(a, b)$
Then $$\exists \, x \in (a, b) : f'(x) (g(b) - g(a)) = g'(x) (f(b) - f(a))$$
Proofs
Proof 0
Let $\emptyset \neq [a, b] \subseteq \mathbb{R}$ be a D544: Closed real interval.
Let $(a, b) \subseteq [a, b]$ be an D543: Open real interval.
Let $f, g : [a, b] \to \mathbb{R}$ each be a D2943: Continuous function.
Let $f, g$ each be a D1416: Differentiable euclidean real function on $(a, b)$.
If $g(b) - g(a) = 0$, then $g(a) = g(b)$ and the claim follows from R1074: Rolle's theorem. Assume thus that $g(b) - g(a) \neq 0$ and consider a function $h : [a, b] \to \mathbb{R}$ given by $$h(x) = f(x) - \frac{f(b) - f(a)}{g(b) - g(a)} g(x)$$ Now $$\begin{split} h(b) - h(a) = f(b) - f(a) - \frac{f(b) - f(a)}{g(b) - g(a)} (g(b) - g(a)) = 0 \end{split}$$ That is, $h(a) = h(b)$. Moreover, $h$ is continuous on $[a, b]$ and differentiable on $(a, b)$ since $f$ and $g$ are. Therefore, R1074: Rolle's theorem implies that there exists $c \in (a, b)$ such that $$h'(c) = f'(c) - \frac{f(b) - f(a)}{g(b) - g(a)} g'(c) = 0$$ and equivalently $$f'(c) (g(b) - g(a)) = g'(c)(f(b) - f(a))$$ $\square$