avewright/proofwiki-math huggingface dataset:
Theorem: Squeeze Theorem/Functions

Let $a$ be a point on an open real interval $I$.
Let $f$, $g$ and $h$ be real functions defined at all points of $I$ except for possibly at point $a$.
Suppose that:
:$\forall x \ne a \in I: \map g x \le \map f x \le \map h x$
:$\ds \lim_{x \mathop \to a} \map g x = \lim_{x \mathop \to a} \map h x = L$
Then:
:$\ds \lim_{x \mathop \to a} \ \map f x = L$

Proof:
Let $f, g, h$ be real functions defined on an open interval $\openint a b$, except possibly at the point $c \in \openint a b$.
Let:
:$\ds \lim_{x \mathop \to c} \map g x = L$
:$\ds \lim_{x \mathop \to c} \map h x = L$
:$\map g x \le \map f x \le \map h x$ except perhaps at $x = c$.
Let $\sequence {x_n}$ be a sequence of points of $\openint a b$ such that:
:$\forall n \in \N_{>0}: x_n \ne c$
and:
:$\ds \lim_{n \mathop \to \infty} \ x_n = c$
By Limit of Function by Convergent Sequences:
:$\ds \lim_{n \mathop \to \infty} \map g {x_n} = L$
and:
:$\ds \lim_{n \mathop \to \infty} \map h {x_n} = L$
Since:
:$\map g {x_n} \le \map f {x_n} \le \map h {x_n}$
it follows from the Squeeze Theorem for Real Sequences that:
:$\ds \lim_{n \mathop \to \infty} \map f {x_n} = L$
The result follows from Limit of Function by Convergent Sequences.
{{qed}}
Theorem: Squeeze Theorem/Functions

Let $a$ be a point on an open real interval $I$.
Let $f$, $g$ and $h$ be real functions defined at all points of $I$ except for possibly at point $a$.
Suppose that:
:$\forall x \ne a \in I: \map g x \le \map f x \le \map h x$
:$\ds \lim_{x \mathop \to a} \map g x = \lim_{x \mathop \to a} \map h x = L$
Then:
:$\ds \lim_{x \mathop \to a} \ \map f x = L$

Proof:
By the definition of the limit of a real function, we have to prove that:
:$\forall \epsilon \in \R_{>0}: \exists \delta \in \R_{>0}: \paren {\size {x - a} < \delta \implies \size {\map f x - L} < \epsilon}$
Let $\epsilon \in \R_{>0}$ be given.
We have:
:$\ds \lim_{x \mathop \to a} \map g x = \lim_{x \mathop \to a} \map h x$
Hence by Sum Rule for Limits of Real Functions:
:$\ds \lim_{x \mathop \to a} \paren {\map h x - \map g x} = 0$
By the definition of the limit of a real function:
:$(1): \quad \forall \epsilon' \in \R_{>0}: \exists \delta \in \R_{>0}: \paren {\size {x - a} < \delta \implies \size {\map h x - L} < \epsilon'}$
:$(2): \quad \forall \epsilon' \in \R_{>0}: \exists \delta \in \R_{>0}: \paren {\size {x - a} < \delta \implies \size {\map g x - L} < \epsilon'}$
:$(3): \quad \forall \epsilon' \in \R_{>0}: \exists \delta \in \R_{>0}: \paren {\size {x - a} < \delta \implies \size {\map h x - \map g x} < \epsilon'}$
Take $\epsilon' = \dfrac {\epsilon} 3$ in $(1)$, $(2)$, $(3)$.
Then there exists $\delta_1, \delta_2, \delta_3$ that satisfies $(1)$, $(2)$, $(3)$ with $\epsilon' = \dfrac \epsilon 3$. 
Take $\delta = \min \set {\delta_1, \delta_2, \delta_3}$.
Then:
{{begin-eqn}}
{{eqn | l = \size {x - a}
      | o = <
      | r = \delta
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \size {\map h x - L}
      | o = <
      | r = \frac {\epsilon} 3
      | c =
}}
{{eqn | lo= \land
      | l = \size {\map g x - L}
      | o = <
      | r = \frac {\epsilon} 3
      | c = 
}}
{{eqn | lo= \land
      | l = \size {\map h x - \map g x}
      | o = <
      | r = \frac {\epsilon} 3
      | c = 
}}
{{end-eqn}}
So, if $\size {x - a} < \delta$:
{{begin-eqn}}
{{eqn | l = \size {\map f x - L}
      | r = \size {\map f x - \map g x + \map h x - L + \map g x - \map h x}
      | c = 
}}
{{eqn | o = \le
      | r = \size {\map f x - \map g x} + \size {\map h x - L} + \size {\map h x - \map g x}
      | c = 
}}
{{eqn | o = \le
      | r = \size {\map h x - \map g x} + \size {\map h x - L} + \size {\map h x - \map g x}
      | c = 
}}
{{eqn | o = \le
      | r = \frac {\epsilon} 3 + \frac {\epsilon} 3 + \frac {\epsilon} 3
      | c = 
}}
{{eqn | r = \epsilon
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Weierstrass's Theorem

There exists a real function $f: \closedint 0 1 \to \closedint 0 1$ such that:
:$(1): \quad f$ is continuous
:$(2): \quad f$ is nowhere differentiable.

Proof:
Let $C \closedint 0 1$ denote the set of all real functions $f: \closedint 0 1 \to \R$ which are continuous on $\closedint 0 1$.
From Closed Real Interval is Compact Space, it follows that $\closedint 0 1$ is compact.
From Metric Space is Hausdorff, it follows that $\R$ is a Hausdorff space.
From Subspace of Hausdorff Space is Hausdorff, it follows that $\closedint 0 1$ is a Hausdorff space.
By Continuous Functions on Compact Space form Banach Space, $C \closedint 0 1$ is a Banach space under the supremum norm $\norm {\,\cdot \,}_\infty$.
By the definition of complete metric space, it follows that every Banach space is a complete metric space.
Let $X$ consist of the $f \in C \closedint 0 1$ such that:
:$\map f 0 = 0$
:$\map f 1 = 1$
:$\forall x \in \closedint 0 1: 0 \le \map f x \le 1$
Theorem: Combination Theorem for Limits of Functions/Real/Sum Rule

:$\ds \lim_{x \mathop \to c} \paren {\map f x + \map g x} = l + m$

Proof:
Let $\sequence {x_n}$ be any sequence of elements of $S$ such that:
:$\forall n \in \N_{>0}: x_n \ne c$
:$\ds \lim_{n \mathop \to \infty} \ x_n = c$
By Limit of Real Function by Convergent Sequences:
:$\ds \lim_{n \mathop \to \infty} \map f {x_n} = l$
:$\ds \lim_{n \mathop \to \infty} \map g {x_n} = m$
By the Sum Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \paren {\map f {x_n} + \map g {x_n} } = l + m$
Applying Limit of Real Function by Convergent Sequences again, we get:
:$\ds \lim_{x \mathop \to c} \paren {\map f x + \map g x} = l + m$
{{qed}}
Theorem: Combination Theorem for Limits of Functions/Real/Multiple Rule

:$\ds \lim_{x \mathop \to c} \lambda \map f x = \lambda l$

Proof:
Let $\sequence {x_n}$ be any sequence of elements of $S$ such that:
:$\forall n \in \N_{>0}: x_n \ne c$
:$\ds \lim_{n \mathop \to \infty} x_n = c$
By Limit of Real Function by Convergent Sequences:
:$\ds \lim_{n \mathop \to \infty} \map f {x_n} = l$
By the Multiple Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \lambda \map f {x_n} = \lambda l$
Applying Limit of Real Function by Convergent Sequences again:
:$\ds \lim_{x \mathop \to c} \lambda \map f x = \lambda l$
{{qed}}
Category:Combination Theorems for Limits of Functions
arix1yx7ve809fvaty3fta7sndrj86r
Theorem: Combination Theorem for Limits of Functions/Real/Combined Sum Rule

:$\ds \lim_{x \mathop \to c} \paren {\lambda \map f x + \mu \map g x} = \lambda l + \mu m$

Proof:
Let $\sequence {x_n}$ be any sequence of elements of $S$ such that:
:$\forall n \in \N^*: x_n \ne c$
:$\ds \lim_{n \mathop \to \infty} x_n = c$
By Limit of Real Function by Convergent Sequences:
:$\ds \lim_{n \mathop \to \infty} \map f {x_n} = l$
:$\ds \lim_{n \mathop \to \infty} \map g {x_n} = m$
By the Combined Sum Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \paren {\lambda \map f {x_n} + \mu \map g {x_n} } = \lambda l + \mu m$
Applying Limit of Real Function by Convergent Sequences again, we get:
:$\ds \lim_{x \mathop \to c} \paren {\lambda \map f x + \mu \map g x} = \lambda l + \mu m$
{{qed}}
Theorem: Combination Theorem for Limits of Functions/Real/Product Rule

:$\ds \lim_{x \mathop \to c} \paren {\map f x \map  g x} = l m$

Proof:
Let $\sequence {x_n}$ be a sequence of elements of $S$ such that:
:$\forall n \in \N: x_n \ne c$
:$\ds \lim_{n \mathop \to \infty} x_n = c$
By Limit of Real Function by Convergent Sequences:
:$\ds \lim_{n \mathop \to \infty} \map f {x_n} = l$
:$\ds \lim_{n \mathop \to \infty} \map g {x_n} = m$
By the Product Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \paren {\map f {x_n} \map g {x_n} } = l m$
Applying Limit of Real Function by Convergent Sequences again, we get:
:$\ds \lim_{x \mathop \to c} \paren {\map f x \map g x} = l m$
{{qed}}
Theorem: Combination Theorem for Limits of Functions/Real/Quotient Rule

:$\ds \lim_{x \mathop \to c} \frac {\map f x} {\map g x} = \frac l m$
provided that $m \ne 0$.

Proof:
Let $\sequence {x_n}$ be any sequence of elements of $S$ such that:
:$\forall n \in \N_{>0}: x_n \ne c$
:$\ds \lim_{n \mathop \to \infty} x_n = c$
By Limit of Real Function by Convergent Sequences:
:$\ds \lim_{n \mathop \to \infty} \map f {x_n} = l$
:$\ds \lim_{n \mathop \to \infty} \map g {x_n} = m$
By the Quotient Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \frac {\map f {x_n} } {\map g {x_n} } = \frac l m$
provided that $m \ne 0$.
Applying Limit of Real Function by Convergent Sequences again, we get:
:$\ds \lim_{x \mathop \to c} \frac {\map f x} {\map g x} = \frac l m$
provided that $m \ne 0$.
{{qed}}
Theorem: Combination Theorem for Continuous Functions/Real/Sum Rule

:$f + g$ is continuous on $S$.

Proof:
By definition of continuous:
:$\forall c \in S: \ds \lim_{x \mathop \to c} \map f x = \map f c$
:$\forall c \in S: \ds \lim_{x \mathop \to c} \map g x = \map g c$
Let $f$ and $g$ tend to the following limits:
:$\ds \lim_{x \mathop \to c} \map f x = l$
:$\ds \lim_{x \mathop \to c} \map g x = m$
From the Sum Rule for Limits of Real Functions, we have that:
:$\ds \lim_{x \mathop \to c} \paren {\map f x + \map g x} = l + m$
So, by definition of continuous again, we have that $f + g$ is continuous on $S$.
{{qed}}
Theorem: Combination Theorem for Continuous Functions/Real/Product Rule

:$f g$ is continuous on $S$

Proof:
By definition of continuous:
:$\forall c \in S: \ds \lim_{x \mathop \to c} \map f x = \map f c$
:$\forall c \in S: \ds \lim_{x \mathop \to c} \map g x = \map g c$
Let $f$ and $g$ tend to the following limits:
:$\ds \lim_{x \mathop \to c} \map f x = l$
:$\ds \lim_{x \mathop \to c} \map g x = m$
From the Product Rule for Limits of Real Functions:
:$\ds \lim_{x \mathop \to c} \paren {\map f x \map g x} = l m$
So, by definition of continuous again, we have that $f g$ is continuous on $S$.
{{qed}}
Theorem: Combination Theorem for Continuous Functions/Real/Multiple Rule

:$\lambda f$ is continuous on $S$.

Proof:
By definition of continuous, we have that
:$\forall c \in S: \ds \lim_{x \mathop \to c} \map f x = \map f c$
Let $f$ tend to the following limit:
:$\ds \lim_{x \mathop \to c} \map f x = l$
From the Multiple Rule for Limits of Real Functions, we have that:
:$\ds \lim_{x \mathop \to c} \paren {\lambda \map f x} = \lambda l$
So, by definition of continuous again, we have that $\lambda f$ is continuous on $S$.
{{qed}}
Category:Combination Theorems for Continuous Real Functions
p2bsx9fyfpxcsstyd8118k6uu8onz5o
Theorem: Combination Theorem for Continuous Functions/Real/Combined Sum Rule

:$\lambda f + \mu g$ is continuous on $S$.

Proof:
By definition of continuous, we have that
:$\forall c \in S: \ds \lim_{x \mathop \to c} \map f x = \map f c$
:$\forall c \in S: \ds \lim_{x \mathop \to c} \map g x = \map g c$
Let $f$ and $g$ tend to the following limits:
:$\ds \lim_{x \mathop \to c} \map f x = l$
:$\ds \lim_{x \mathop \to c} \map g x = m$
From the Combined Sum Rule for Limits of Real Functions, we have that:
:$\ds \lim_{x \mathop \to c} \paren {\lambda \map f x + \mu \map g x} = \lambda l + \mu m$
So, by definition of continuous again, we have that $\lambda f + \mu g$ is continuous on $S$.
{{qed}}
Theorem: Combination Theorem for Continuous Functions/Real/Quotient Rule

:$\dfrac f g$ is continuous on $S \setminus \set {x \in S: \map g x = 0}$
that is, on all the points $x$ of $S$ where $\map g x \ne 0$.

Proof:
By definition of continuous:
:$\forall c \in S: \ds \lim_{x \mathop \to c} \map f x = \map f c$
:$\forall c \in S: \ds \lim_{x \mathop \to c} \map g x = \map g c$
Let $f$ and $g$ tend to the following limits:
:$\ds \lim_{x \mathop \to c} \map f x = l$
:$\ds \lim_{x \mathop \to c} \map g x = m$
From the Quotient Rule for Limits of Real Functions, we have that:
:$\ds \lim_{x \mathop \to c} \frac {\map f x} {\map g x} = \frac l m$
wherever $m \ne 0$.
So, by definition of continuous again, we have that $\dfrac f g$ is continuous on all points $x$ of $S$ where $\map g x \ne 0$.
{{qed}}
Theorem: Brouwer's Fixed Point Theorem/One-Dimensional Version

Let $f: \closedint a b \to \closedint a b$ be a real function which is continuous on the closed interval $\closedint a b$.
Then:
:$\exists \xi \in \closedint a b: \map f \xi = \xi$
That is, a continuous real function from a closed real interval to itself fixes some point of that interval.

Proof:
By Subset of Real Numbers is Interval iff Connected, $\closedint a b$ is connected.
{{AimForCont}} there is no fixed point.
Then $\map f a > a$ and $\map f b < b$.
Let:
:$U = \set {x \in \closedint a b: \map f x > x}$
:$V = \set {x \in \closedint a b: \map f x < x}$
Then $U$ and $V$ are open in $\closedint a b$.
Because $a \in U$ and $b\in V$, $U$ and $V$ are non-empty.
By assumption:
:$U \cup V = \closedint a b$
Thus $\closedint a b$ is not connected, which is a contradiction.
Thus, by Proof by Contradiction, there exists at least one fixed point.
{{qed}}
Theorem: Brouwer's Fixed Point Theorem/One-Dimensional Version

Let $f: \closedint a b \to \closedint a b$ be a real function which is continuous on the closed interval $\closedint a b$.
Then:
:$\exists \xi \in \closedint a b: \map f \xi = \xi$
That is, a continuous real function from a closed real interval to itself fixes some point of that interval.

Proof:
As the codomain of $f$ is $\closedint a b$, it follows that the image of $f$ is a subset of $\closedint a b$.
Thus:
:$\map f a \ge a$
and
:$\map f b \le b$
Let us define the real function $g: \closedint a b \to \R$ by:
:$\map g x = \map f x - x$
Then by the Combined Sum Rule for Continuous Real Functions, $\map g x$ is continuous on $\closedint a b$.
But:
:$\map g a \ge 0$ and $\map g b \le 0$
By the Intermediate Value Theorem:
:$\exists \xi \in \openint a b: \map g \xi = 0$
Thus:
:$\map f \xi = \xi$
{{qed}}
Theorem: Brouwer's Fixed Point Theorem/Smooth Mapping

A smooth mapping $f$ of the closed unit ball $\overline B^n \subset \R^n$ into itself has a fixed point:
:$\forall f \in \map {C^\infty} {\overline B^n \to \overline B^n}: \exists x \in \overline B^n: \map f x = x$

Proof:
Suppose there exists such a mapping $f$ of the unit ball to itself without fixed points.
Since $\map f x \ne x$, the two points $x$ and $\map f x$ are distinct and there is a unique ray from $x$ to $\map f x$ on which they both lie.
Call this line $L$ and let $\map h x = \partial \overline B^n \cap L$.
If $x \in \partial \overline B^n$, then $\map h x = x$ and $h$ restricts to the identity on $\partial \overline B^n$.
Since $x$ is in the line segment between $\map f x$ and $\map h x$, one may write the vector $\map h x - \map f x$ as a multiple $t$ times the vector $x - \map f x$, where $t \ge 1$.
Hence:
:$\map h x = t x + \paren {1 - t} \map f x$
Since $f$ is smooth, the smoothness of $t$ with respect to $x$ implies the smoothness of $h$.
Taking the dot product of both sides of this formula and noting that $\size {\map h x} = 1$:
:$t^2 \size {x - \map f x}^2 + 2 t \map f x \cdot \paren {x - \map f x} + \size {\map f x}^2 - 1 = 0$
Applying the Quadratic Formula gives:
:$t = \dfrac {\map f x \cdot \paren {\map f x - x} } {\size {x - \map f x}^2}$
an expression for $t$ in smooth terms of $x$.
Hence $h$ is a smooth retract of a compact manifold onto its boundary, which contradicts the Retraction Theorem.
{{qed}}
{{Namedfor|Luitzen Egbertus Jan Brouwer}}
Category:Brouwer's Fixed Point Theorem
49luvf2h46dcxtjcz7mub8p3ge9zl9q
Theorem: Power Rule for Derivatives/Natural Number Index

Let $n \in \N$.
Let $f: \R \to \R$ be the real function defined as $\map f x = x^n$.
Then:
:$\map {f'} x = n x^{n-1}$
everywhere that $\map f x = x^n$ is defined.
When $x = 0$ and $n = 0$, $\map {f'} x$ is undefined.

Proof:
Let $\map f x = x^n$ for $x \in \R, n \in \N$.
By the definition of the derivative:
:$\ds \dfrac \d {\d x} \map f x = \lim_{h \mathop \to 0} \dfrac {\map f {x + h} - \map f x} h = \lim_{h \mathop \to 0} \dfrac {\paren {x + h}^n - x^n} h$
Using the Binomial Theorem this simplifies to:
{{begin-eqn}}
{{eqn | o = 
      | r = \lim_{h \mathop \to 0} \paren {\frac {\dbinom n 0 x^n + \dbinom n 1 x^{n - 1} h + \dbinom n 2 x^{n - 2} h^2 + \cdots + \dbinom n {n - 1} x h^{n - 1} + \dbinom n n h^n - x^n} h}
      | c = 
}}
{{eqn | r = \lim_{h \mathop \to 0} \paren {\frac {\dbinom n 1 x^{n - 1} h + \dbinom n 2 x^{n - 2} h^2 + \cdots + \dbinom n {n - 1} x h^{n - 1} + \dbinom n n h^n} h}
      | c = 
}}
{{eqn | r = \lim_{h \mathop \to 0} \paren {\dbinom n 1 x^{n - 1} + \dbinom n 2 x^{n - 2} h^1 + \cdots + \dbinom n {n - 1} x h^{n - 2} + \dbinom n n h^{n - 1} }
      | c = 
}}
{{eqn | r = \dbinom n 1 x^{n - 1}
      | c = evaluating the limit
}}
{{eqn | r = n x^{n - 1}
      | c = Binomial Coefficient with One
}}
{{end-eqn}}
{{qed}}
Theorem: Power Rule for Derivatives/Natural Number Index

Let $n \in \N$.
Let $f: \R \to \R$ be the real function defined as $\map f x = x^n$.
Then:
:$\map {f'} x = n x^{n-1}$
everywhere that $\map f x = x^n$ is defined.
When $x = 0$ and $n = 0$, $\map {f'} x$ is undefined.

Proof:
Let $\map f x = x^n$ for $x \in \R, n \in \N$.
Let $a \in \R$.
By definition of the derivative:
:$\ds \map {f'} a = \lim_{x \mathop \to a} \frac {\map f x - \map f a} {x - a} = \lim_{x \mathop \to a} \frac {x^n - a^n} {x - a}$
=== Case $\text I$ ===
For $n = 0$ it is possible to do:
{{begin-eqn}}
{{eqn | l = \map {f'} a
      | r = \lim_{x \mathop \to a} \frac {x^0 - a^0} {x - a}
      | c = 
}}
{{eqn | r = \lim_{x \mathop \to a} \frac 0 {x - a}
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
We have that:
:$0 \cdot x^{0 - 1} = 0$
for all $x \ne 0$.
So in this case:
:$\map {f'} x = n x^{n - 1}$
{{qed|lemma}}
=== Case $\text {II}$ ===
For $n = 1$ we have:
:$\map f x = x$
From Derivative of Identity Function:
:$\map {f'} x = 1$
Then we note that:
:$1 \cdot x^{1 - 1} = 1$
So for the case $n = 1$:
:$\map {f'} x = n x^{n - 1}$
{{qed|lemma}}
=== Case $\text {III}$ ===
$\R$ is a commutative ring, so for $n \ge 2$ it is possible to do:
{{begin-eqn}}
{{eqn | l = \map {f'} a
      | r = \lim_{x \mathop \to a} \frac {x^n - a^n} {x - a}
      | c = 
}}
{{eqn | r = \lim_{x \mathop \to a} \frac {\paren {x - a} \sum_{j \mathop = 0}^{n - 1} x^{n - j - 1} a^j} {x - a}
      | c = Difference of Two Powers
}}
{{eqn | r = \lim_{x \mathop \to a} \sum_{j \mathop = 0}^{n - 1} x^{n - j - 1} a^j
}}
{{eqn | r = \sum_{j \mathop = 0}^{n - 1} a^{n - j - 1} a^j
      | c = Real Polynomial Function is Continuous
}}
{{eqn | r = \sum_{j \mathop = 0}^{n - 1} a^{n - 1}
}}
{{eqn | r = \sum_{j \mathop = 1}^n a^{n - 1}
      | c = shifting the index from $0$ to $1$
}}
{{eqn | r = n a^{n - 1}
}}
{{end-eqn}}
This holds for all $a \in \R$, so:
:$\map {f'} x = n x^{n - 1}$
{{qed}}
Theorem: Power Rule for Derivatives/Natural Number Index

Let $n \in \N$.
Let $f: \R \to \R$ be the real function defined as $\map f x = x^n$.
Then:
:$\map {f'} x = n x^{n-1}$
everywhere that $\map f x = x^n$ is defined.
When $x = 0$ and $n = 0$, $\map {f'} x$ is undefined.

Proof:
We will use the notation $D \map f x = \map {f'} x$ as it is convenient.
Let $n = 0$.
Then:
:$\forall x \in \R: x^n = 1$
Thus $\map f x$ is the constant function $\map {f_1} x$ on $\R$.
Thus from Derivative of Constant, $D \map f x = \map D {x^0} = 0 x^{-1}$, except where $x = 0$.
So the result holds for $n = 0$.
Let $n = 1$.
Then:
:$\forall x \in \R: \map f x = x^n = x$
Then from Derivative of Identity Function:
:$\map D x = 1 = 1 \cdot x^{1 - 1}$
So the result holds for $n = 1$.
Now assume $\map D {x^k} = k x^{k - 1}$.
Then by the Product Rule for Derivatives:
:$\map D {x^{k + 1} } = \map D {x^k x} = x^k \map D x + \map D {x^k} x = x^k \cdot 1 + k x^{k - 1} x = \paren {k + 1} x^k$
The result follows by induction.
{{qed}}
Theorem: Power Rule for Derivatives/Integer Index

Let $n \in \Z$.
Let $f: \R \to \R$ be the real function defined as $\map f x = x^n$.
Then:
:$\map {f'} x = n x^{n - 1}$
everywhere that $\map f x = x^n$ is defined.
When $x = 0$ and $n = 0$, $\map {f'} x$ is undefined.

Proof:
When $n \ge 0$ we use the result for Natural Number Index.
Now let $n \in \Z: n < 0$.
Then let $m = -n$ and so $m > 0$.
Thus $x^n = \dfrac 1 {x^m}$.
{{begin-eqn}}
{{eqn | l = \map D {x^n}
      | r = \map D {\frac 1 {x^m} }
      | c = 
}}
{{eqn | r = \frac {x^m \cdot 0 - 1 \cdot m x^{m - 1} } {x^{2 m} }
      | c = Quotient Rule for Derivatives
}}
{{eqn | r = -m x^{-m - 1}
      | c = 
}}
{{eqn | r = n x^{n - 1}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Power Rule for Derivatives/Fractional Index

Let $n \in \N_{>0}$.
Let $f: \R \to \R$ be the real function defined as $\map f x = x^{1 / n}$.
Then:
:$\map {f'} x = n x^{n - 1}$
everywhere that $\map f x = x^n$ is defined.
When $x = 0$ and $n = 0$, $\map {f'} x$ is undefined.

Proof:
Let $n \in \N_{>0}$.
Thus, let $\map f x = x^{1 / n}$.
From the definition of the power to a rational number, or alternatively from the definition of the root of a number, $\map f x$ is defined when $x \ge 0$.
(However, see the special case where $x = 0$.)
From Continuity of Root Function, $\map f x$ is continuous over the open interval $\openint 0 \infty$, but not at $x = 0$ where it is continuous only on the right.
Let $y > x$.
From Inequalities Concerning Roots:
:$\forall n \in \N_{>0}: X Y^{1 / n} \, \size {x - y} \le n X Y \, \size {x^{1 / n} - y^{1 / n} } \le Y X^{1 / n} \, \size {x - y}$
where $x, y \in \closedint X Y$.
Setting $X = x$ and $Y = y$, this reduces (after algebra) to:
:$\dfrac 1 {n y} y^{1 / n} \le \dfrac {y^{1 / n} - x^{1 / n} } {y - x} \le \dfrac 1 {n x} x^{1 / n}$
From the Squeeze Theorem for Functions, it follows that:
:$\ds \lim_{y \mathop \to x^+} \dfrac {y^{1 / n} - x^{1 / n} } {y - x} = \dfrac 1 {n x} x^{1 / n} = \dfrac 1 n x^{\dfrac 1 n - 1}$
A similar argument shows that the left hand limit is the same.
Thus the result holds for $\map f x = x^{1 / n}$.
{{qed}}
Theorem: Power Rule for Derivatives/Fractional Index

Let $n \in \N_{>0}$.
Let $f: \R \to \R$ be the real function defined as $\map f x = x^{1 / n}$.
Then:
:$\map {f'} x = n x^{n - 1}$
everywhere that $\map f x = x^n$ is defined.
When $x = 0$ and $n = 0$, $\map {f'} x$ is undefined.

Proof:
Let $n \in \N_{>0}$.
Thus, let $\map f x = y = x^{1/n}$.
Thus $\map {f^{-1} } y = x = y^n$ from the definition of root.
So:
{{begin-eqn}}
{{eqn | l = D x^{1/n}
      | r = \frac 1 {D y^n}
      | c = Derivative of Inverse Function
}}
{{eqn | r = \frac 1 {n y^{n - 1} }
      | c = Power Rule for Derivatives: Integer Index
}}
{{eqn | r = \frac 1 {n \paren {x^{1/n} }^{n - 1} }
      | c = 
}}
{{eqn | r = \frac 1 n x^{\frac 1 n - 1}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Power Rule for Derivatives/Rational Index

Let $n \in \Q$.
Let $f: \R \to \R$ be the real function defined as $\map f x = x^n$.
Then:
:$\map {f'} x = n x^{n - 1}$
everywhere that $\map f x = x^n$ is defined.
When $x = 0$ and $n = 0$, $\map {f'} x$ is undefined.

Proof:
Let $n \in \Q$, such that $n = \dfrac p q$ where $p, q \in \Z, q \ne 0$.
Then we have:
{{begin-eqn}}
{{eqn | l = \map D {x^n}
      | r = \map D {x^{p / q} }
      | c = 
}}
{{eqn | r = \map D {\paren {x^p}^{1 / q} }
      | c = 
}}
{{eqn | r = \frac 1 q \paren {x^p}^{1 / q} x^{-p} p x^{p - 1}
      | c = Chain Rule for Derivatives
}}
{{eqn | r = \frac p q x^{\frac p q - 1}
      | c = after some algebra
}}
{{eqn | r = n x^{n - 1}
      | c = 
}}
{{end-eqn}}
{{qed}}