avewright/proofwiki-math huggingface dataset:
Theorem: Fermat's Little Theorem

Let $p$ be a prime number.
Let $n \in \Z_{>0}$ be a positive integer such that $p$ is not a divisor of $n$.
Then:
:$n^{p - 1} \equiv 1 \pmod p$

Proof:
Proof by induction over $n$.
Induction base:
:$1^p \equiv 1 \pmod p$
Induction step:
Assume $n^p \equiv n \pmod p$
{{begin-eqn}}
{{eqn | l = \paren {n + 1}^p
      | r = \sum_{k \mathop = 0}^p {p \choose k} n^{p - k} \cdot 1^k
      | c = Binomial Theorem
}}
{{eqn | q = \forall k: 0 < k < p
      | l = {p \choose k}
      | o = \equiv
      | r = 0 \pmod p
      | c = Binomial Coefficient of Prime
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^p {p \choose k} n^{p - k}
      | o = \equiv
      | r = n^p + n^0 \pmod p
}}
{{eqn | o = \equiv
      | r = n^p + 1 \pmod p
}}
{{eqn | o = \equiv
      | r = n + 1 \pmod p
      | c = Induction Step
}}
{{end-eqn}}
Dividing by $n$:
:$\forall n: n^p \equiv n \pmod p \implies n^{p - 1} \equiv 1 \pmod p$
{{qed}}
Theorem: Fermat's Little Theorem

Let $p$ be a prime number.
Let $n \in \Z_{>0}$ be a positive integer such that $p$ is not a divisor of $n$.
Then:
:$n^{p - 1} \equiv 1 \pmod p$

Proof:
Let $S$ be a set of n elements, and consider $p$-tuples $\left( a_1, a_2, \dots, a_p \right)$ and consider the Group Action of these p-tuples by $\Z/p\Z$ via cyclic shifts.
For example, if:
:$S = \{ b, r, g \}$
and:
:$p=5$
then $rgbgg$ is equivalent to:
:$grgbg, ggrgb, bggrg, gbggr$.
We use Burnside's Lemma, counting the number of elements fixed by each element of the group $\Z/p\Z$. Note that the identity fixes all $a^p$ elements, and the only tuples fixed by any of the other $p-1$ elements of $\Z/p\Z$ are the $a$ tuples that are made up of only one element of $S$, for example $rrrrr$, $ggggg$, and $bbbbb$. 
Burnside's Lemma says that:
:$p \mid \left( n^p + (p-1) n \right)$
equivalently:
:$n^p \equiv n \pmod p$
{{qed}}
Theorem: De Morgan's Laws (Set Theory)

{{:De Morgan's Laws (Set Theory)/Set Difference}}

Proof:
Let the cardinality $\card I$ of the indexing set $I$ be $n$.
Then by the definition of cardinality, it follows that $I \cong \N^*_n$ and we can express the proposition:
:$\ds S \setminus \bigcap_{i \mathop \in I} T_i = \bigcup_{i \mathop \in I} \paren {S \setminus T_i}$
as:
:$\ds S \setminus \bigcap_{i \mathop = 1}^n T_i = \bigcup_{i \mathop = 1}^n \paren {S \setminus T_i}$
The proof of this is more amenable to proof by Principle of Mathematical Induction.
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\ds S \setminus \bigcap_{i \mathop = 1}^n T_i = \bigcup_{i \mathop = 1}^n \paren {S \setminus T_i}$
$\map P 1$ is true, as this just says $S \setminus T_1 = S \setminus T_1$.
=== Base Case ===
$\map P 2$ is the case:
:$S \setminus \paren {T_1 \cap T_2} = \paren {S \setminus T_1} \cup \paren {S \setminus T_2}$
which has been proved. 
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 2$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\ds S \setminus \bigcap_{i \mathop = 1}^k T_i = \bigcup_{i \mathop = 1}^k \paren {S \setminus T_i}$
=== Induction Step ===
Now we need to show:
:$\ds S \setminus \bigcap_{i \mathop = 1}^{k + 1} T_i = \bigcup_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}$
This is our induction step:
{{begin-eqn}}
{{eqn | l = S \setminus \bigcap_{i \mathop = 1}^{k + 1} T_i
      | r = S \setminus \paren {\bigcap_{i \mathop = 1}^k T_i \cap T_{k + 1} }
      | c = Intersection is Associative
}}
{{eqn | r = \paren {S \setminus \bigcap_{i \mathop = 1}^k T_i} \cup \paren {S \setminus T_{k + 1} }
      | c = Base case
}}
{{eqn | r = \paren {\bigcup_{i \mathop = 1}^k \paren {S \setminus T_i} } \cup \paren {S \setminus T_{k + 1} }
      | c = Induction hypothesis
}}
{{eqn | r = \bigcup_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}
      | c = Union is Associative
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\ds S \setminus \bigcap_{i \mathop = 1}^n T_i = \bigcup_{i \mathop = 1}^n \paren {S \setminus T_i}$
that is:
:$\ds S \setminus \bigcap_{i \mathop \in I} T_i = \bigcup_{i \mathop \in I} \paren {S \setminus T_i}$
{{qed}}
Theorem: De Morgan's Laws (Set Theory)

{{:De Morgan's Laws (Set Theory)/Set Difference}}

Proof:
Let the cardinality $\size I$ of the indexing set $I$ be $n$.
Then by the definition of cardinality, it follows that $I \cong \N^*_n$ and we can express the proposition:
:$\ds S \setminus \bigcup_{i \mathop \in I} T_i = \bigcap_{i \mathop \in I} \paren {S \setminus T_i}$
as:
:$\ds S \setminus \bigcup_{i \mathop = 1}^n T_i = \bigcap_{i \mathop = 1}^n \paren {S \setminus T_i}$
The proof of this is more amenable to proof by Principle of Mathematical Induction.
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\ds S \setminus \bigcup_{i \mathop = 1}^n T_i = \bigcap_{i \mathop = 1}^n \paren {S \setminus T_i}$.
$\map P 1$ is true, as this just says $S \setminus T_1 = S \setminus T_1$.
=== Base Case ===
$\map P 2$ is the case:
:$S \setminus \paren {T_1 \cup T_2} = \paren {S \setminus T_1} \cap \paren {S \setminus T_2}$
which has been proved.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 2$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\ds S \setminus \bigcup_{i \mathop = 1}^k T_i = \bigcap_{i \mathop = 1}^k \paren {S \setminus T_i}$
=== Induction Step ===
Now we need to show:
:$\ds S \setminus \bigcup_{i \mathop = 1}^{k + 1} T_i = \bigcap_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}$
This is our induction step:
{{begin-eqn}}
{{eqn | l = S \setminus \bigcup_{i \mathop = 1}^{k + 1} T_i
      | r = S \setminus \paren {\bigcup_{i \mathop = 1}^k T_i \cup T_{k + 1} }
      | c = Union is Associative
}}
{{eqn | r = \paren {S \setminus \bigcup_{i \mathop = 1}^k T_i} \cap \paren {S \setminus T_{k + 1} }
      | c = Base case
}}
{{eqn | r = \paren {\bigcap_{i \mathop = 1}^k \paren {S \setminus T_i} } \cap \paren {S \setminus T_{k + 1} }
      | c = Induction hypothesis
}}
{{eqn | r = \bigcap_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}
      | c = Intersection is Associative
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\ds S \setminus \bigcup_{i \mathop = 1}^n T_i = \bigcap_{i \mathop = 1}^n \paren {S \setminus T_i}$
that is:
:$\ds S \setminus \bigcup_{i \mathop \in I} T_i = \bigcap_{i \mathop \in I} \paren {S \setminus T_i}$
{{qed}}
Theorem: De Morgan's Laws (Set Theory)

{{:De Morgan's Laws (Set Theory)/Set Difference}}

Proof:
Let $x \in S$ througout.
{{begin-eqn}}
{{eqn | o = 
      | r = x \in \relcomp S {T_1 \cup T_2}
}}
{{eqn | o = \leadsto
      | r = x \notin \paren {T_1 \cup T_2}
      | c = {{Defof|Relative Complement}}
}}
{{eqn | o = \leadsto
      | r = \neg \paren {x \in T_1 \lor x \in T_2}
      | c = {{Defof|Set Union}}
}}
{{eqn | o = \leadsto
      | r = x \notin T_1 \land x \notin T_2
      | c = De Morgan's Laws: Conjunction of Negations
}}
{{eqn | o = \leadsto
      | r = x \in \relcomp S {T_1} \land x \in \relcomp S {T_2}
      | c = {{Defof|Relative Complement}}
}}
{{eqn | o = \leadsto
      | r = x \in \relcomp S {T_1} \cap \relcomp S {T_2}
      | c = {{Defof|Set Intersection}}
}}
{{eqn | o = \leadsto
      | r = \relcomp S {T_1 \cup T_2} \subseteq \relcomp S {T_1} \cap \relcomp S {T_2}
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | o = 
      | r = x \in \relcomp S {T_1} \cap \relcomp S {T_2}
}}
{{eqn | o = \leadsto
      | r = x \in \relcomp S {T_1} \land x \in \relcomp S {T_2}
      | c = {{Defof|Set Intersection}}
}}
{{eqn | o = \leadsto
      | r = x \notin T_1 \land x \notin T_2
      | c = {{Defof|Relative Complement}}
}}
{{eqn | o = \leadsto
      | r = \neg \paren {x \in T_1 \lor x \in T_2}
      | c = De Morgan's Laws: Conjunction of Negations
}}
{{eqn | o = \leadsto
      | r = x \notin \paren {T_1 \cup T_2}
      | c = {{Defof|Set Union}}
}}
{{eqn | o = \leadsto
      | r = x \in \relcomp S {T_1 \cup T_2}
      | c = {{Defof|Relative Complement}}
}}
{{eqn | o = \leadsto
      | r = \relcomp S {T_1} \cap \relcomp S {T_2} \subseteq \relcomp S {T_1 \cup T_2}
      | c = {{Defof|Set Intersection}}
}}
{{end-eqn}}
By definition of set equality:
:$\relcomp S {T_1 \cup T_2} = \relcomp S {T_1} \cap \relcomp S {T_2}$
{{qed}}
Theorem: De Morgan's Laws (Set Theory)

{{:De Morgan's Laws (Set Theory)/Set Difference}}

Proof:
{{begin-eqn}}
{{eqn | l = \overline {T_1 \cap T_2}
      | r = \mathbb U \setminus \paren {T_1 \cap T_2}
      | c = {{Defof|Set Complement}}
}}
{{eqn | r = \paren {\mathbb U \setminus T_1} \cup \paren {\mathbb U \setminus T_2}
      | c = De Morgan's Laws: Difference with Intersection
}}
{{eqn | r = \overline {T_1} \cup \overline {T_2}
      | c = {{Defof|Set Complement}}
}}
{{end-eqn}}
{{qed}}
Theorem: De Morgan's Laws (Set Theory)

{{:De Morgan's Laws (Set Theory)/Set Difference}}

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in \overline {T_1 \cap T_2}
}}
{{eqn | o = \leadstoandfrom
      | r = x \notin \paren {T_1 \cap T_2}
      | c = {{Defof|Set Complement}}
}}
{{eqn | o = \leadstoandfrom
      | r = \neg \paren {x \in T_1 \land x \in T_2}
      | c = {{Defof|Set Intersection}}
}}
{{eqn | o = \leadstoandfrom
      | r = \neg \paren {x \in T_1} \lor \neg \paren {x \in T_2}
      | c = De Morgan's Laws (Logic): Disjunction of Negations
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \overline {T_1} \lor x \in \overline {T_2}
      | c = {{Defof|Set Complement}}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \overline {T_1} \cup \overline {T_2}
      | c = 
}}
{{end-eqn}}
By definition of set equality:
:$\overline {T_1 \cap T_2} = \overline {T_1} \cup \overline {T_2}$
{{qed}}
Theorem: De Morgan's Laws (Set Theory)

{{:De Morgan's Laws (Set Theory)/Set Difference}}

Proof:
{{begin-eqn}}
{{eqn | l = \map \complement {\map \complement A \cup \map \complement B}
      | r = \map \complement {\map \complement A} \cap \map \complement {\map \complement B}
      | c = De Morgan's Laws: Complement of Union
}}
{{eqn | r = A \cap B
      | c = Complement of Complement
}}
{{eqn | ll= \leadstoandfrom
      | l = \map \complement {\map \complement {\map \complement A \cup \map \complement B} }
      | r = \map \complement {A \cap B}
      | c = taking complements of both sides
}}
{{eqn | ll= \leadstoandfrom
      | l = \map \complement A \cup \map \complement B
      | r = \map \complement {A \cap B}
      | c = Complement of Complement
}}
{{end-eqn}}
{{qed}}
Theorem: De Morgan's Laws (Set Theory)

{{:De Morgan's Laws (Set Theory)/Set Difference}}

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in \overline {T_1 \cup T_2}
}}
{{eqn | o = \leadstoandfrom
      | r = x \notin \paren {T_1 \cup T_2}
      | c = {{Defof|Set Complement}}
}}
{{eqn | o = \leadstoandfrom
      | r = \neg \paren {x \in T_1 \lor x \in T_2}
      | c = {{Defof|Set Union}}
}}
{{eqn | o = \leadstoandfrom
      | r = \neg \paren {x \in T_1} \land \neg \paren {x \in T_2}
      | c = De Morgan's Laws (Logic): Conjunction of Negations
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \overline {T_1} \land x \in \overline {T_2}
      | c = {{Defof|Set Complement}}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \overline {T_1} \cap \overline {T_2}
      | c = 
}}
{{end-eqn}}
By definition of set equality:
:$\overline {T_1 \cup T_2} = \overline {T_1} \cap \overline {T_2}$
{{qed}}
Theorem: De Morgan's Laws (Set Theory)

{{:De Morgan's Laws (Set Theory)/Set Difference}}

Proof:
Suppose:
:$\ds x \in S \setminus \bigcap \mathbb T$
Note that by Set Difference is Subset we have that $x \in S$ (we need this later).
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = S \setminus \bigcap \mathbb T
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \notin
      | r = \bigcap \mathbb T
      | c = {{Defof|Set Difference}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \neg \leftparen {\forall T' \in \mathbb T}
      | l = x
      | o = \in
      | r = \rightparen {T'}
      | c = {{Defof|Intersection of Set of Sets}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists T' \in \mathbb T
      | l = x
      | o = \notin
      | r = T'
      | c = Denial of Universality
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists T' \in \mathbb T
      | l = x
      | o = \in
      | r = S \setminus T'
      | c = {{Defof|Set Difference}}: note $x \in S$ from above
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcup_{T' \mathop \in \mathbb T} \paren {S \setminus T'}
      | c = {{Defof|Union of Set of Sets}}
}}
{{end-eqn}}
Therefore:
:$\ds S \setminus \bigcap \mathbb T = \bigcup_{T' \mathop \in \mathbb T} \paren {S \setminus T'}$
{{qed}}
Theorem: De Moivre's Formula

Let $z \in \C$ be a complex number expressed in complex form:
:$z = r \paren {\cos x + i \sin x}$
Then:
:$\forall \omega \in \C: \paren {r \paren {\cos x + i \sin x} }^\omega = r^\omega \paren {\map \cos {\omega x} + i \, \map \sin {\omega x} }$

Proof:
$\cos x + i \sin x$ is a complex number expressed in polar form $\left\langle{r, \theta}\right\rangle$ whose complex modulus is $1$ and whose argument is $x$.
From De Moivre's Formula: Positive Integer Index:
:$\forall n \in \Z_{>0}: \left({r \left({\cos x + i \sin x}\right)}\right)^n = r^n \left({\cos \left({n x}\right) + i \sin \left({n x}\right)}\right)$
The result follows by setting $r = 1$.
{{qed}}
Theorem: De Moivre's Formula

Let $z \in \C$ be a complex number expressed in complex form:
:$z = r \paren {\cos x + i \sin x}$
Then:
:$\forall \omega \in \C: \paren {r \paren {\cos x + i \sin x} }^\omega = r^\omega \paren {\map \cos {\omega x} + i \, \map \sin {\omega x} }$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {\cos \theta + i \sin \theta}^n
      | r = \paren {e^{i \theta} }^n
      | c = Euler's Formula
}}
{{eqn | r = e^{i n \theta}
      | c = Exponential of Product
}}
{{eqn | r = \cos n \theta + i \sin n \theta
      | c = Euler's Formula
}}
{{end-eqn}}
Theorem: De Moivre's Formula

Let $z \in \C$ be a complex number expressed in complex form:
:$z = r \paren {\cos x + i \sin x}$
Then:
:$\forall \omega \in \C: \paren {r \paren {\cos x + i \sin x} }^\omega = r^\omega \paren {\map \cos {\omega x} + i \, \map \sin {\omega x} }$

Proof:
Proof by induction:
For all $n \in \Z_{> 0}$, let $\map P n$ be the proposition:
:$\paren {r \paren {\cos x + i \sin x} }^n = r^n \paren {\map \cos {n x} + i \, \map \sin {n x} }$
$\map P 1$ is the case:
:$\paren {r \paren {\cos x + i \sin x} }^1 = r^1 \paren {\map \cos {1 x} + i \, \map \sin {1 x} }$
which is trivially true.
=== Basis for the Induction ===
$\map P 2$ is the case:
:$\paren {r \paren {\cos x + i \sin x} }^2 = r^2 \paren {\map \cos {n x} + i \, \map \sin {2 x} }$
From Product of Complex Numbers in Polar Form, we have:
:$r_1 \paren {\cos x_1 + i \sin x_1 } r_2 \paren {\cos x_2 + i \sin x_2} = r_1 r_2 \paren {\map \cos {x_1 + x_2} + i \, \map \sin {x_1 + x_2} }$
Setting $r_1 = r_2 = r$ and $x_1 = x_2 = x$ gives the result.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 1$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\paren {r \paren {\cos x + i \sin x} }^k = r^k \paren {\map \cos {k x} + i \, \map \sin {k x} }$
Then we need to show:
:$\paren {r \paren {\cos x + i \sin x} }^{k + 1} = r^{k + 1} \paren {\map \cos {\paren {k + 1} x} + i \, \map \sin {\paren {k + 1} x} }$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn| l = \paren {r \paren {\cos x + i \sin x} }^{k + 1}
     | r = \paren {r \paren {\cos x + i \sin x} }^k \paren {r \paren {\cos x + i \sin x} }
}}
{{eqn| r = r^k \paren {\map \cos {k x} + i \, \map \sin {k x} } \paren {r \paren {\cos x + i \sin x} }
     | c = Induction Hypothesis
}}
{{eqn| r = r^{k + 1} \paren {\map \cos {\paren {k + 1} x} + i \, \map \sin {\paren {k + 1} x} }
     | c = Product of Complex Numbers in Polar Form
}}
{{end-eqn}}
Hence, by induction, for all $n \in \Z_{> 0}$:
:$\paren {r \paren {\cos x + i \sin x} }^n = r^n \paren {\map \cos {n x} + i \, \map \sin {n x} }$
{{qed}}
Theorem: De Moivre's Formula

Let $z \in \C$ be a complex number expressed in complex form:
:$z = r \paren {\cos x + i \sin x}$
Then:
:$\forall \omega \in \C: \paren {r \paren {\cos x + i \sin x} }^\omega = r^\omega \paren {\map \cos {\omega x} + i \, \map \sin {\omega x} }$

Proof:
From Product of Complex Numbers in Polar Form: General Result:
:$z_1 z_2 \cdots z_n = r_1 r_2 \cdots r_n \paren {\map \cos {\theta_1 + \theta_2 + \cdots + \theta_n} + i \, \map \sin {\theta_1 + \theta_2 + \cdots + \theta_n} }$
Setting $z_1 = z_2 = \cdots = z_n = r \paren {\cos x + i \sin x}$ gives the result.
Theorem: De Moivre's Formula

Let $z \in \C$ be a complex number expressed in complex form:
:$z = r \paren {\cos x + i \sin x}$
Then:
:$\forall \omega \in \C: \paren {r \paren {\cos x + i \sin x} }^\omega = r^\omega \paren {\map \cos {\omega x} + i \, \map \sin {\omega x} }$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {r \paren {\cos x + i \sin x} }^\omega
      | r = \paren {r e^{i x} }^\omega
      | c = Euler's Formula
}}
{{eqn | r = r^\omega e^{i \omega x}
      | c = Power of Power
}}
{{eqn | r = r^\omega \paren {\map \cos {\omega x} + i \map \sin {\omega x} }
      | c = Euler's Formula
}}
{{end-eqn}}
{{qed}}
Theorem: Power Rule for Derivatives

Let $n \in \R$.
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:
This can be done in sections.
Theorem: Power Rule for Derivatives

Let $n \in \R$.
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 \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

Let $n \in \R$.
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 \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

Let $n \in \R$.
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

Let $n \in \R$.
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

Let $n \in \R$.
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}}