avewright/proofwiki-math huggingface dataset:
Theorem: Fundamental Theorem of Algebra

Every non-constant polynomial with coefficients in $\C$ has a root in $\C$.
That is, the field of complex numbers is algebraically closed.

Proof:
Let $\map p z$ be an arbitrary non-constant polynomial with coefficients in $\C$.
This means that for some $n \in \Z_{ge 1}$ and $a_n \ne 0$:
:$\map p z = a_n z^n + a_{n - 1}z^{n - 1} + \dots + a_0$
We have:
:$\map p z = a_n z^n \paren {1 + \dfrac {a_{n - 1} } {a_n}z^{-1} + \dots + \dfrac 1 {a_n}z^{-n} } = a_n z^n \paren {1 + \map \OO {z^{-1} } }$
as $\size z \to \infty$.
Hence:
:$\ds \lim_{\size z \mathop \to \infty} \size {\map p z} = \infty$
Thus we can pick $R > 0$ large enough so that:
:$\ds \inf_{\size z \mathop \ge R} \size {\map p z} > \size {\map p 0}$
It follows that:
:$\ds \inf_{z \mathop \in \C} \size {\map p z} = \inf_{\size z \mathop \le R} \size {\map p z}$
Since $D_R = \set {z \in \C : \size z \le R}$ is compact and $p$ is continuous, there exists $z_0 \in D_R$ such that:
:$\ds \inf_{\size z \mathop \le R} \size {\map p z} = \size {\map p {z_0} }$
Hence:
:$\ds \size {\map p {z_0} } = \inf_{z \mathop \in \C} \size {\map p z}$
It remains to show that $\map p {z_0} = 0$.
{{AimForCont}}:
:$\map p {z_0} = a \ne 0$
Write:
:$\map {z_0 + \zeta} = a + \map q \zeta$
Note that $\map q \zeta$ is a nonconstant polynomial in $\zeta$ satisfying $\map q 0 = 0$.
Hence for some $k \ge 1$ and $b \ne 0$, we have:
:$\map q \zeta = b \zeta^k + b_{k + 1} \zeta^{k + 1} + \dots + b_n \zeta^n$
That is:
:$\map q \zeta = b \zeta^k + \map \OO {\zeta^{k + 1} }$
as $\zeta \to 0$.
Thus, uniformly in $\omega \in S^1 = \set {\omega \in \C : \size {\omega} = 1}$:
:$\map p {z_0 + \epsilon \omega} = a + b \omega^k \epsilon^k + \map \OO {\epsilon^{k + 1} }$
as $\epsilon \searrow 0$.
Since $\size {-\dfrac {a / \size a} {b / \size b} } = 1$, by Euler's theorem, we can pick $\omega \in S^1$ such that:
:$\omega^k = -\dfrac {a / \size a} {b / \size b}$
Then:
:$\ds \map p {z_0 + \epsilon \omega} = a - a \dfrac {\size b} {\size a} \epsilon^k + \map \OO {\epsilon^{k + 1} } = a \paren {1 - \dfrac {\size b} {\size a} \epsilon^k} + \map \OO {\epsilon^{k + 1} }$
Thus:
:$\size {\map p {z_0 + \epsilon\omega} } = \size a \size {1 - \dfrac {\size b} {\size a} \epsilon^k} + \map \OO {\epsilon^{k + 1} }$
Thus for $\epsilon > 0$ small enough:
{{begin-eqn}}
{{eqn | l = \size {\map p {z_0 + \epsilon \omega} }
      | r = \size a \paren {1 - \dfrac {\size b} {\size a} \epsilon^k} + \map \OO {\epsilon^{k + 1} }
      | c = 
}}
{{eqn | r = \size a - \size b \epsilon^k + \map \OO {\epsilon^{k + 1} }
      | c = 
}}
{{eqn | r = \size a - \size b \epsilon^k \paren {1 + \map \OO \epsilon}
      | c = 
}}
{{eqn | o = >
      | r = \size a
      | c = 
}}
{{end-eqn}}
But this contradicts that:
:$\size a = \inf_{z \mathop \in \C} \size {\map p z}$
Thus:
:$\map p {z_0} = a = 0$
{{qed}}
Theorem: Fundamental Theorem of Algebra

Every non-constant polynomial with coefficients in $\C$ has a root in $\C$.
That is, the field of complex numbers is algebraically closed.

Proof:
Let $p: \C \to \C$ be a complex, non-constant polynomial.
{{AimForCont}} that $\map p z \ne 0$ for all $z \in \C$.
Therefore by Reciprocal of Holomorphic Function $\dfrac 1 {\map p z}$ is entire.
{{begin-eqn}}
{{eqn | l = 0
      | o = <
      | r = \cmod {\dfrac 1 {\map p 0} }
}}
{{eqn | r = \cmod {\frac 1 {2 \pi i} \oint_{\set {w \in \C : \cmod w = R} } \frac {\rd z} {z \cdot \map p z} }
      | c = Cauchy's Integral Formula
}}
{{eqn | o = \le
      | r = \frac 1 {2 \pi} \max \limits_{\size z \mathop = R} \paren {\frac 1 {\size {z \cdot \map p z} } } 2 \pi R
      | c = Estimation Lemma for Contour Integrals
}}
{{eqn | r = \max \limits_{\size z \mathop = R} \frac 1 {\size {\map p z} }
}}
{{eqn | o = \to
      | r = 0
      | c = as $R \to +\infty$
}}
{{end-eqn}}
This is a contradiction.
{{qed}}
Theorem: Extendability Theorem for Intersection Numbers

Let $X = \partial W$ be a smooth manifold which is the boundary of a smooth compact manifold $W$.
Let:
:$Y$ be a smooth manifold
:$Z$ be a closed smooth submanifold of $Y$
:$f: X \to Y$ be a smooth mapping.
Let there exist a smooth mapping $g: W \to Y$ such that $g \restriction_X = f$.
Then:
:$\map I {f, Z} = 0$
where $\map I {f, Z}$ is the intersection number.

Proof:
{{ProofWanted}}
Category:Extendability Theorem for Intersection Numbers
Category:Smooth Manifolds
Category:Named Theorems
0acfthtqqi1fi4rbdp3g4fm6k5luk72
Theorem: Relative Homotopy is Equivalence Relation

Let $X$ and $Y$ be topological spaces.
Let $K \subseteq X$ be a (possibly empty) subset of $X$.
Let $\map \CC {X, Y}$ be the set of all continuous mappings from $X$ to $Y$.
Define a relation $\sim$ on $\map \CC {X, Y}$ as:
:$f \sim g$ {{iff}} $f$ and $g$ are homotopic relative to $K$.
Then $\sim$ is an equivalence relation.

Proof:
We examine each condition for equivalence.
Theorem: Homotopy Group is Homeomorphism Invariant

Let $X$ and $Y$ be two topological spaces.
Let $\phi: X \to Y$ be a homeomorphism.
Let $x_0 \in X$, $y_0 \in Y$.
Then for all $n \in \N$ the induced mapping:
:$\phi_* : \pi_n \left({X, x_0}\right) \to \pi_n \left({Y, y_0}\right):$
::$\left[{\!\left[{\, c \,}\right]\!}\right] \mapsto \left[{\!\left[{\, \phi \circ c \,}\right]\!}\right]$
is an isomorphism, where $\pi_n$ denotes the $n$th homotopy group.

Proof:
Let $\phi: X \to Y$ be a homeomorphism.
We must show that:
:$(1): \quad$ If $c: \left[{0 \,.\,.\, 1}\right]^n \to X$ is a continuous mapping, then $ \phi \circ c: \left[{0 \,.\,.\, 1}\right]^n \to Y$ is also continuous
:$(2): \quad$ If $c, d: \left[{0 \,.\,.\, 1}\right]^n \to X$ are freely homotopic, then $\phi \circ c, \phi \circ d: \left[{0 \,.\,.\, 1}\right]^n \to Y$ are also freely homotopic
:$(3): \quad$ If $c, d: \left[{0 \,.\,.\, 1}\right]^n \to X$ are not freely homotopic, there can be no free homotopy between $\phi \circ c$ and $\phi \circ d$
:$(4): \quad$ The image of the concatenation of two maps, $\phi \left({c * d}\right)$, is freely homotopic to the concatenation of the images, $\phi \left({c}\right) * \phi \left({d}\right)$.
{{finish}}
Category:Homotopy Theory
Category:Algebraic Topology
k56fmuxw5p3gs43xabyg5nndpghuet7
Theorem: Homotopy Group is Group

The set of all homotopy classes of continuous mappings:
:$c: \closedint 0 1^n \to X$
satisfying:
:$\map c {\partial \closedint 0 1^n} = x_0$
in a space $X$ at a base point $x_0$, under the operation of concatenation on class members, forms a group.
{{finish|This operation needs to be shown well-defined; probably a nasty proof}}
This group is called the $n$th homotopy group.

Proof:
We examine each of the group axioms separately.
Theorem: Interior Extremum Theorem

Let $f$ be a real function which is differentiable on the open interval $\openint a b$.
Let $f$ have a local minimum or local maximum at $\xi \in \openint a b$.
Then:
:$\map {f'} \xi = 0$

Proof:
By definition of derivative at a point:
:$\dfrac {\map f x - \map f \xi} {x - \xi} \to \map {f'} \xi$ as $x \to \xi$
Suppose $\map {f'} \xi > 0$.
Then from Behaviour of Function Near Limit it follows that:
:$\exists I = \openint {\xi - h} {\xi + h}: \dfrac {\map f x - \map f \xi} {x - \xi} > 0$
provided that $x \in I$ and $x \ne \xi$.
Now let $x_1$ be any number in the open interval $\openint {\xi - h} \xi$.
Then:
:$x_1 - \xi < 0$
and hence from:
:$\dfrac {\map f {x_1} - \map f \xi} {x_1 - \xi} > 0$
it follows that:
:$\map f {x_1} < \map f \xi$
Thus $f$ can not have a local minimum at $\xi$.
Now let $x_2$ be any number in the open interval $\openint \xi {\xi + h}$.
Then:
:$x_2 - \xi > 0$
and hence from:
:$\dfrac {\map f {x_2} - \map f \xi} {x_2 - \xi} > 0$
it follows that:
:$\map f {x_2} > \map f \xi$
Thus $f$ can not have a local maximum at $\xi$ either.
A similar argument can be applied to $-f$ to handle the case where $\map {f'} \xi < 0$.
The only other possibility is that $\map {f'} \xi = 0$, hence the result.
{{qed}}
Theorem: Interior Extremum Theorem

Let $f$ be a real function which is differentiable on the open interval $\openint a b$.
Let $f$ have a local minimum or local maximum at $\xi \in \openint a b$.
Then:
:$\map {f'} \xi = 0$

Proof:
By definition of local maximum:
:$(1): \quad \map f {\xi + \epsilon} - \map f \xi < 0$
for sufficiently small $\epsilon \in \R_{>0}$.
Similarly, definition of local minimum:
:$(2): \quad \map f {\xi + \epsilon} - \map f \xi > 0$
for sufficiently small $\epsilon \in \R_{>0}$.
Let it be assumed that $\map f {\xi + \epsilon}$ can be expanded, using Taylor's Theorem, in positive integer powers of $\epsilon$
Then:
:$(3): \quad \map f {\xi + \epsilon} - \map f \xi = \epsilon \map {f'} \xi + \dfrac {\epsilon^2 \map {f' '} \xi} 2 + \map \OO {\epsilon^3}$
where $\map \OO {\epsilon^3}$ denotes big-$\OO$ notation.
That is, the quantity $\dfrac {\map \OO {\epsilon^3} } {\epsilon^3}$ is bounded.
From $(1)$ and $(2)$, at a local maximum or local minimum, the sign of $\map f {\xi + \epsilon} - \map f \xi$ is independent the sign of $\epsilon$ itself.
So from $(3)$ it follows that $\map {f'} \xi = 0$.
{{qed}}
Theorem: Behaviour of Function Near Limit

Let $f$ be a real function.
Let $f \left({x}\right) \to l$ as $x \to \xi$.
Then:
:If $l > 0$, then $\exists h > 0: \forall x: \xi - h < x < \xi + h, x \ne \xi: \map f x > 0$
:If $l < 0$, then $\exists h > 0: \forall x: \xi - h < x < \xi + h, x \ne \xi: \map f x < 0$

Proof:
From the definition of limit of a function:
:$\forall \epsilon > 0: \exists \delta > 0: 0 < \size {x - \xi} < \delta \implies \size {\map f x - l} < \epsilon$
Let $l > 0$.
Since this is true for all $\epsilon > 0$, it is also true for $\epsilon = l$.
So let the value of $\delta$, for the above to be true, labelled $h$.
Then:
:$0 < \size {x - \xi} < h \implies \size {\map f x - l} < l$
That is:
:$\xi - h < x < \xi + h, x \ne \xi \implies 0 = l - l < \map f x < l + l = 2 l$
Hence:
:$\forall x: \xi - h < x < \xi + h, x \ne \xi: 0 < \map f x$
Now let $l < 0$, and consider $\epsilon = -l$.
A similar thread of reasoning leads us to:
:$\xi - h < x < \xi + h, x \ne \xi \implies -2 l < \map f x < 0$
and hence the second result.
{{qed}}
Theorem: Fundamental Group is Independent of Base Point for Path-Connected Space

Let $X$ be a path-connected space.
For $x \in X$, let $\map {\pi_1}{X, x}$ denote the fundamental group.
For $x, y \in X$, there is an isomorphism:
:$\phi: \map {\pi_1} {X, x} \to \map {\pi_1} {X, y}$

Proof:
Since $X$ is path-connected there exists a path $f$ connecting $y$ and $x$.
We define $\phi_f: \map {\pi_1} {X, x} \to \map {\pi_1} {X, y}$ by $\map {\phi_f} {\sqbrk g} =\sqbrk {f^{-1} g f}$.
$\phi$ is a homomorphism of groups, as is seen from:
:$\ds \map {\phi_f} {\sqbrk {g h} } = \sqbrk {f^{-1} g h f} = \sqbrk {f^{-1} g f f^{-1} h f} = \sqbrk {f^{-1} g f} \sqbrk {f^{-1} h f} = \map {\phi_f} {\sqbrk g} \map {\phi_f} {\sqbrk h}$ 
Also, $f^{-1}$ is a path from $x$ to $y$. Then by the same argument as before, $\phi_{f^{-1} }: \map {\pi_1} {X, y} \to \map {\pi_1} {X, x}$ where $\map {\phi_{f^{-1} } } {\sqbrk g} = \sqbrk {f g f^{-1} }$, is a homomorphism of groups.
Trivially, $\phi_f \circ \phi_{f^{-1} } = I_{\map {\pi_1} {X, y} }$ and $\phi_{f^{-1} } \circ \phi_f = I_{\map {\pi_1} {X, x} }$.
Then $\phi_f^{-1} = \phi_{f^{-1} }$, so $\phi_f$ is bijective and thus an isomorphism.
{{qed}}
Category:Algebraic Topology
ij73y2he3nhnck5rodsqb32kqnfemx3
Theorem: List of Fundamental Groups for 2-Manifolds

{{MissingLinks|two-mainfold, also review links for everything else because it's all over the place}}
For the following two-manifolds, the fundamental group for any point in $X$, written $\map {\pi_1} X$ is isomorphic to the listed group:
:$\map {\pi_1} {\Bbb S^1 \times \closedint 0 1} = \Z$
:$\map {\pi_1} {\Bbb S^2} = \set e$, the trivial group.
:$\map {\pi_1} {\Bbb T^2} = \map {\pi_1} {\Bbb S^1 \times \Bbb S^1} = \Z \times \Z$
:$\map {\pi_1} {\Bbb {RP}^2} = \Z_2$

Proof:
{{ProofWanted}}
Category:Algebraic Topology
0dl7p0jv58blp4y4j335ztzml678qi2
Theorem: Rolle's Theorem

Let $f$ be a real function which is:
:continuous on the closed interval $\closedint a b$
and:
:differentiable on the open interval $\openint a b$.
Let $\map f a = \map f b$.
Then:
:$\exists \xi \in \openint a b: \map {f'} \xi = 0$

Proof:
We have that $f$ is continuous on $\closedint a b$.
It follows from Continuous Image of Closed Real Interval is Closed Real Interval that $f$ attains:
:a maximum $M$ at some $\xi_1 \in \closedint a b$
and:
:a minimum $m$ at some $\xi_2 \in \closedint a b$.
Suppose $\xi_1$ and $\xi_2$ are both end points of $\closedint a b$.
Because $\map f a = \map f b$ it follows that $m = M$ and so $f$ is constant on $\closedint a b$.
Then, by Derivative of Constant, $\map {f'} \xi = 0$ for all $\xi \in \openint a b$.
Suppose $\xi_1$ is not an end point of $\closedint a b$.
Then $\xi_1 \in \openint a b$ and $f$ has a local maximum at $\xi_1$.
Hence the result follows from the Interior Extremum Theorem.
Similarly, suppose $\xi_2$ is not an end point of $\closedint a b$.
Then $\xi_2 \in \openint a b$ and $f$ has a local minimum at $\xi_2$.
Hence the result follows from the Interior Extremum Theorem.
{{qed}}
Theorem: Rolle's Theorem

Let $f$ be a real function which is:
:continuous on the closed interval $\closedint a b$
and:
:differentiable on the open interval $\openint a b$.
Let $\map f a = \map f b$.
Then:
:$\exists \xi \in \openint a b: \map {f'} \xi = 0$

Proof:
First take the case where:
:$\forall x \in \openint a b: \map f x = 0$
Then:
:$\forall x \in \openint a b: \map {f'} x = 0$
Otherwise:
:$\exists c \in \openint a b: \map f c \ne 0$
Let $\map f c > 0$.
Then there exists an absolute maximum at a point $\xi \in \openint a b$.
Hence:
{{begin-eqn}}
{{eqn | l = \dfrac {\map f {\xi + h} - \map f \xi} h
      | o = \le
      | r = 0
      | c = for $\xi < \xi + h < b$
}}
{{eqn | l = \dfrac {\map f {\xi + h} - \map f \xi} h
      | o = \ge
      | r = 0
      | c = for $a < \xi + h < \xi$
}}
{{end-eqn}}
As $h \to 0$, we see that both of the above approach $\map {f'} \xi$, which is then both non-negative and non-positive.
That is:
:$\map {f'} \xi = 0$
Similarly, let $\map f c < 0$.
Then there exists an absolute minimum at a point $\xi \in \openint a b$.
Hence:
{{begin-eqn}}
{{eqn | l = \dfrac {\map f {\xi + h} - \map f \xi} h
      | o = \ge
      | r = 0
      | c = for $\xi < \xi + h < b$
}}
{{eqn | l = \dfrac {\map f {\xi + h} - \map f \xi} h
      | o = \le
      | r = 0
      | c = for $a < \xi + h < \xi$
}}
{{end-eqn}}
Again, as $h \to 0$, we see that both of the above approach $\map {f'} \xi$, which is then both non-negative and non-positive.
That is:
:$\map {f'} \xi = 0$
Hence the result.
{{qed}}
Theorem: Rolle's Theorem

Let $f$ be a real function which is:
:continuous on the closed interval $\closedint a b$
and:
:differentiable on the open interval $\openint a b$.
Let $\map f a = \map f b$.
Then:
:$\exists \xi \in \openint a b: \map {f'} \xi = 0$

Proof:
Let the function $g$ be defined as:
:$\map g t = \map {R_n} t - \dfrac {\paren {t - a}^{n + 1} } {\paren {x - a}^{n + 1} } \map {R_n} x$
Then:
:$\map {g^{\paren k} } a = 0$
for $k = 0, \dotsc, n$, and $\map g x = 0$.
Apply Rolle's Theorem successively to $g, g', \dotsc, g^{\paren n}$.
Then there exist:
:$\xi_1, \ldots, \xi_{n + 1}$
between $a$ and $x$ such that:
:$\map {g'} {\xi_1} = 0, \map {g' '} {\xi_2} = 0, \ldots, \map {g^{\paren {n + 1} } } {\xi_{n + 1} } = 0$
Let $\xi = \xi_{n + 1}$.
Then:
:$0 = \map {g^{\paren {n + 1} } } \xi = \map {f^{\paren {n + 1} } } \xi - \dfrac {\paren {n + 1}!} {\paren {x - a}^{n + 1} } \map {R_n} x$
and the formula for $\map {R_n} x$ follows.
{{qed}}
Theorem: Mean Value Theorem

Let $f$ be a real function which is continuous on the closed interval $\closedint a b$ and differentiable on the open interval $\openint a b$.
Then:
:$\exists \xi \in \openint a b: \map {f'} \xi = \dfrac {\map f b - \map f a} {b - a}$

Proof:
From Continuous Real Function is Darboux Integrable, $f$ is Darboux integrable on $\closedint a b$.
By the Extreme Value Theorem, there exist $m, M \in \closedint a b$ such that:
:$\ds \map f m = \min_{x \mathop \in \closedint a b} \map f x$
:$\ds \map f M = \max_{x \mathop \in \closedint a b} \map f x$
Then, from Darboux's Theorem:
:$\ds \map f m \paren {b - a} \le \int_a^b \map f x \rd x \le \map f M \paren {b - a}$ 
Dividing all terms by $\paren {b - a}$ gives:
:$\ds \map f m \le \frac 1 {b - a}\int_a^b \map f x \rd x \le \map f M$
By the Intermediate Value Theorem, there exists some $k \in \openint a b$ such that:
{{begin-eqn}}
{{eqn | l = \frac 1 {b - a} \int_a^b \map f x \rd x
      | r = \map f k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int_a^b \map f x \rd x
      | r = \map f k \paren {b - a}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Mean Value Theorem

Let $f$ be a real function which is continuous on the closed interval $\closedint a b$ and differentiable on the open interval $\openint a b$.
Then:
:$\exists \xi \in \openint a b: \map {f'} \xi = \dfrac {\map f b - \map f a} {b - a}$

Proof:
From Continuous Real Function is Darboux Integrable, $f$ is Darboux integrable on $\closedint a b$.
Let $F : \closedint a b \to \R$ be a real function defined by: 
:$\ds \map F x = \int_a^x \map f x \rd x$
We are assured that this function is well-defined, since $f$ is integrable on $\closedint a b$.
From Fundamental Theorem of Calculus: First Part, we have: 
: $F$ is continuous on $\closedint a b$
: $F$ is differentiable on $\openint a b$ with derivative $f$
By the Mean Value Theorem, there therefore exists $k \in \openint a b$ such that: 
:$\map {F'} k = \dfrac {\map F b - \map F a} {b - a}$
As $F$ is differentiable on $\openint a b$ with derivative $f$: 
:$\map {F'} k = \map f k$
We therefore have: 
{{begin-eqn}}
{{eqn	| l = \map f k
	| r = \frac {\map F b - \map F a} {b - a}
}}
{{eqn	| r = \frac 1 {b - a} \paren {\int_a^b \map f x \rd x - \int_a^a \map f x \rd x}
}}
{{eqn	| r = \frac 1 {b - a} \int_a^b \map f x \rd x
	| c = Definite Integral on Zero Interval
}}
{{end-eqn}}
giving: 
:$\ds \int_a^b \map f x \rd x = \paren {b - a} \map f k$
as required.
{{qed}}
Theorem: Mean Value Theorem

Let $f$ be a real function which is continuous on the closed interval $\closedint a b$ and differentiable on the open interval $\openint a b$.
Then:
:$\exists \xi \in \openint a b: \map {f'} \xi = \dfrac {\map f b - \map f a} {b - a}$

Proof:
For any constant $h \in \R$ we may construct the real function defined on $\closedint a b$ by:
:$\map F x = \map f x + h x$
We have that $h x$ is continuous on $\closedint a b$ from Linear Function is Continuous.
From the Sum Rule for Continuous Real Functions, $F$ is continuous on $\closedint a b$ and differentiable on $\openint a b$.
Let us calculate what the constant $h$ has to be such that $\map F a = \map F b$:
{{begin-eqn}}
{{eqn | l = \map F a
      | r = \map F b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map f a + h a
      | r = \map f b + h b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map f a - \map f b
      | r = h b - h a
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = \map f a - \map f b
      | r = h \paren {b - a}
      | c = Real Multiplication Distributes over Real Addition
}}
{{eqn | ll= \leadsto
      | l = h
      | r = -\dfrac {\map f b - \map f a} {b - a}
      | c = rearranging
}}
{{end-eqn}}
Since $F$ satisfies the conditions for the application of Rolle's Theorem:
:$\exists \xi \in \openint a b: \map {F'} \xi = 0$
But then:
:$\map {F'} \xi = \map {f'} \xi + h = 0$
The result follows.
{{qed}}
Theorem: Mean Value Theorem

Let $f$ be a real function which is continuous on the closed interval $\closedint a b$ and differentiable on the open interval $\openint a b$.
Then:
:$\exists \xi \in \openint a b: \map {f'} \xi = \dfrac {\map f b - \map f a} {b - a}$

Proof:
Let $g : \closedint a b \to \R$ be a real function with: 
:$\map g x = x$
for all $x \in \closedint a b$. 
By Power Rule for Derivatives, we have: 
:$g$ is differentiable with $\map {g'} x = 1$ for all $x \in \closedint a b$.
Note that in particular: 
:$\map {g'} x \ne 0$ for all $x \in \openint a b$.
Since $f$ is continuous on $\closedint a b$ and differentiable on $\openint a b$, we can apply the Cauchy Mean Value Theorem.
We therefore have that there exists $\xi \in \openint a b$ such that: 
:$\dfrac {\map {f'} \xi} {\map {g'} \xi } = \dfrac {\map f b - \map f a} {\map g b - \map g a}$
Note that: 
:$\map {g'} \xi = 1$
and: 
:$\map g b - \map g a = b - a$
so this can be rewritten: 
:$\map {f'} \xi = \dfrac {\map f b - \map f a} {b - a}$
{{qed}}
Theorem: Mean Value Theorem

Let $f$ be a real function which is continuous on the closed interval $\closedint a b$ and differentiable on the open interval $\openint a b$.
Then:
:$\exists \xi \in \openint a b: \map {f'} \xi = \dfrac {\map f b - \map f a} {b - a}$

Proof:
Recall the Cauchy Mean Value Theorem:
{{:Cauchy Mean Value Theorem}}
The result follows by setting $\map g x = x$ for all $x \in \R$.
{{qed}}
Theorem: Mean Value Theorem

Let $f$ be a real function which is continuous on the closed interval $\closedint a b$ and differentiable on the open interval $\openint a b$.
Then:
:$\exists \xi \in \openint a b: \map {f'} \xi = \dfrac {\map f b - \map f a} {b - a}$

Proof:
Let $G$ be a real-valued function continuous on $\closedint a x$ and differentiable with non-vanishing derivative on $\openint a x$.
Let:
:$\map F t = \map f t + \dfrac {\map {f'} t} {1!} \paren {x - t} + \dotsb + \dfrac {\map {f^{\paren n} } t} {n!} \paren {x - t}^n$
By the Cauchy Mean Value Theorem:
:$(1): \quad \dfrac {\map {F'} x} {\map {G'} \xi} = \dfrac {\map F x - \map F a} {\map G x - \map G a}$
for some $\xi \in \openint a x$.
Note that the numerator:
:$\map F x - \map F a = R_n$
is the remainder of the Taylor polynomial for $\map f x$.
On the other hand, computing $\map {F'} \xi$:
:$\map {F'} \xi = \map {f'} \xi - \map {f'} \xi + \dfrac {\map {f' '} \xi} {1!} \paren {x - \xi} - \dfrac {\map {f' '} \xi} {1!} \paren {x - \xi} + \dotsb + \dfrac {\map {f^{\paren {n + 1} } } t} {n!} \paren {x - \xi}^n = \dfrac {\map {f^{\paren {n + 1} } } \xi} {n!} \paren {x - \xi}^n$
Putting these two facts together and rearranging the terms of $(1)$ yields:
:$R_n = \dfrac {\map {f^{\paren {n + 1} } } \xi} {n!} \paren {x - \xi}^n \dfrac {\map G x - \map G a} {\map {G'} \xi}$
which was to be shown.
{{improve|Find a way of neatly handling the two different remainder forms}}
Note that the Lagrange Form of the Remainder comes from taking $\map G t = \paren {x - t}^{n + 1}$ and the given Cauchy Form of the Remainder comes from taking $\map G t = t - a$.
{{qed}}
Theorem: Zero Derivative implies Constant Function

Let $f$ be a real function which is continuous on the closed interval $\closedint a b$ and differentiable on the open interval $\openint a b$.
Suppose that:
:$\forall x \in \openint a b: \map {f'} x = 0$
Then $f$ is constant on $\closedint a b$.

Proof:
When $x = a$ then $\map f x = \map f a$ by definition of mapping.
Otherwise, let $x \in \hointl a b$.
We have that:
:$f$ is continuous on the closed interval $\closedint a b$
:$f$ is differentiable on the open interval $\openint a b$
Hence it satisfies the conditions of the Mean Value Theorem on $\closedint a b$.
Hence:
:$\exists \xi \in \openint a x: \map {f'} \xi = \dfrac {\map f x - \map f a} {x - a}$
But by our supposition:
:$\forall x \in \openint a b: \map {f'} x = 0$
which means:
:$\forall x \in \openint a b: \map f x - \map f a = 0$
and hence:
:$\forall x \in \openint a b: \map f x = \map f a$
{{qed}}
Theorem: Ostrowski's Theorem

Every non-trivial norm on the rational numbers $\Q$ is equivalent to either:
:the $p$-adic norm $\norm {\, \cdot \,}_p$ for some prime $p$
or:
:the absolute value, $\size {\, \cdot \,}$.

Proof:
Let $\norm {\, \cdot \,}$ be a non-trivial norm on the rational numbers $\Q$.