avewright/proofwiki-math huggingface dataset:
Theorem: Monomorphism from Rational Numbers to Totally Ordered Field

Let $\struct {F, +, \circ, \le}$ be a totally ordered field.
There is one and only one (ring) monomorphism from the totally ordered field $\Q$ onto $F$.
Its image is the prime subfield of $F$.

Proof:
Follows from:
:Characteristic of Ordered Integral Domain is Zero
:Order Embedding between Quotient Fields is Unique.
{{Qed}}
Theorem: Set of Polynomials over Integral Domain is Subring

Let $\struct {R, +, \circ}$ be a commutative ring.
Let $\struct {D, +, \circ}$ be an integral subdomain of $R$.
Then $\forall x \in R$, the set $D \sqbrk x$ of polynomials in $x$ over $D$ is a subring of $R$.

Proof:
By application of the Subring Test:
As $D$ is an integral domain, it has a unity $1_D$ and so $x = 1_D x$.
Hence $x \in D \sqbrk x$ and so $D \sqbrk x \ne \O$.
Let $p, q \in D \sqbrk x$.
Then let:
:$\ds p = \sum_{k \mathop = 0}^m a_k \circ x^k, q = \sum_{k \mathop = 0}^n b_k \circ x^k$
Thus:
:$\ds -q = -\sum_{k \mathop = 0}^n b_k \circ x^k = \sum_{k \mathop = 0}^n \paren {-b_k} \circ x^k$
and so:
:$q \in D \sqbrk x$
Thus as Polynomials Closed under Addition, it follows that:
:$p + \paren {-q} \in D \sqbrk x$
Finally, from Polynomials Closed under Ring Product, we have that $p \circ q \in D \sqbrk x$.
All the criteria of the Subring Test are satisfied.
Hence the result.
{{qed}}
Theorem: Polynomials Closed under Ring Product

Let $\struct {R, +, \circ}$ be a commutative ring.
Let $\ds f = \sum_{k \mathop \in Z} a_k \mathbf X^k$, $\ds g = \sum_{k \in Z} b_k \mathbf X^k$ be polynomials in the indeterminates $\set {X_j: j \in J}$ over $R$, where $Z$ is the set of all multiindices indexed by $\set {X_j: j \in J}$.
Define the product
:$\ds f \otimes g = \sum_{k \in Z} c_k \mathbf X^k$
where
:$\ds c_k = \sum_{\substack {p + q = k \\ p, q \in Z} } a_p b_q$
Then $f \otimes g$ is a polynomial.

Proof:
{{handwaving}}
It is immediate that $f \otimes g$ is a map from the free commutative monoid to $R$, so we need only prove that $f \otimes g$ is nonzero on finitely many $\mathbf X^k$, $k \in Z$.
Suppose that for some $k \in Z$:
:$\ds \sum_{\substack {p + q = k \\ p, q \mathop \in Z}} a_p b_q \ne 0$
Therefore if $c_k \ne 0$ there exist $p, q \in Z$ such that $p + q = k$ and $a_p$, $b_q$ are both nonzero.
Since $f$ and $g$ are polynomials, the set $\set {p + q: a_p \ne 0, b_q \ne 0}$ is finite.
Hence the result.
{{qed}}
{{proofread}}
Category:Polynomial Theory
kfggk2gsxh5ess6hkd0nxyxvyg8kewg
Theorem: Unique Representation in Polynomial Forms

Let $\struct {R, +, \circ}$ be a commutative ring with unity whose zero is $0_R$ and whose unity is $1_R$.
Let $\struct {D, +, \circ}$ be an integral subdomain of $R$.
Let $X \in R$ be transcendental over $D$.
Let $D \sqbrk X$ be the ring of polynomials in $X$ over $D$.
Then each non-zero member of $D \left[{X}\right]$ can be expressed in just one way in the form:
:$\ds f \in D \sqbrk X: f = \sum_{k \mathop = 0}^n {a_k \circ X^k}$

Proof:
Suppose $f \in D \sqbrk X \setminus \set {0_R}$ has more than one way of being expressed in the above form.
Then you would be able to subtract one from the other and get a polynomial in $D \sqbrk X$ equal to zero.
As $f$ is transcendental, the result follows.
{{qed}}
Theorem: Ring of Polynomial Forms is Integral Domain

Let $\struct {R, +, \circ}$ be a commutative ring with unity.
Let $\struct {D, +, \circ}$ be an integral subdomain of $R$.
Let $X \in R$ be transcendental over $D$.
Let $D \sqbrk X$ be the ring of polynomials in $X$ over $D$.
Then $D \sqbrk X$ is an integral domain.

Proof:
By Ring of Polynomial Forms is Commutative Ring with Unity we know that $D \sqbrk X$ is a commutative ring with unity.
Let neither $\ds \map f X = \sum_{k \mathop = 0}^n a_k x^k$ nor $\ds \map g X = \sum_{k \mathop = 0}^m b_k X^k$ be the null polynomial.
Then their leading coefficients $a_n$ and $b_m$ are non-zero.
Therefore, as $D$ is an integral domain and $a_n, b_m \in D$, so is their product $a_n b_m$.
By the definition of polynomial multiplication, it follows that $f g$ is not the null polynomial.
It follows that $D \sqbrk X$ has no proper zero divisors.
Hence $D \sqbrk X$ is an integral domain.
{{qed}}
Theorem: Rings of Polynomials in Ring Elements are Isomorphic

Let $R_1, R_2$ be commutative rings with unity.
Let $D$ be an integral subdomain of both $R_1$ and $R_2$.
Let $X_1, X_2 \in R$ be transcendental over $D$.
Let $D \sqbrk {X_1}, D \sqbrk {X_2}$ be the rings of polynomials in $X_1$ and $X_2$ over $D$.
Then $D \sqbrk {X_1}$ is isomorphic to $D \sqbrk {X_2}$.

Proof:
First it is shown that the mapping $\phi: D \sqbrk {X_1} \to D \sqbrk {X_2}$ given by:
:$\ds \map \phi {\sum_{k \mathop = 0}^n a_k \circ X_1^k} = \sum_{k \mathop = 0}^n a_k \circ X_2^k$
is a bijection.
Let $p, q \in \phi: D \sqbrk {X_1}$.
Suppose $\map \phi p = \map \phi q$.
Then the coefficients of $\map \phi p$ and $\map \phi q$ are equal, and $p_1 = q_1$.
Thus, by definition, $\phi$ is an injection.
By the same argument, the mapping $\psi: D \sqbrk {X_2} \to D \sqbrk {X_1}$ defined as:
:$\ds \map \psi {\sum_{k \mathop = 0}^n a_k \circ X_2^k} = \sum_{k \mathop = 0}^n a_k \circ X_1^k$
is similarly an injection.
Thus by Injection is Bijection iff Inverse is Injection, $\phi$ is a bijection.
It remains to show that $\phi$ is a ring homomorphism. 
Let $\ds p = \sum_{k \mathop = 0}^n a_k \circ X_1^k, q = \sum_{k \mathop = 0}^n b_k \circ X_2^k \in D \sqbrk {X_1}$. 
For convenience we set $a_k = 0$, $k > n$ and $b_k = 0$, $k > m$.
We have:
{{begin-eqn}}
{{eqn | l = \map \phi {p + q}
      | r = \map \phi {\sum_{k \mathop = 0}^\infty \paren {a_k + b_k} X_1^k}
      | c = {{Defof|Polynomial Addition}}
}}
{{eqn | r = \sum_{k \mathop = 0}^\infty \left({a_k + b_k}\right) X_2^k
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 0}^m a_k X_2^k + \sum_{k \mathop = 0}^n b_k X_2^k
      | c = 
}}
{{eqn | r = \map \phi p + \map \phi q
      | c = 
}}
{{end-eqn}}
Similarly for multiplication:
{{begin-eqn}}
{{eqn | l = \map \phi {p q}
      | r = \map \phi {\sum_{k \mathop = 0}^{m n} \sum_{i + j = k} a_i b_j X_1^k}
      | c = {{Defof|Multiplication of Polynomials}}
}}
{{eqn | r = \sum_{k \mathop = 0}^{m n} \sum_{i + j \mathop = k} a_i b_j X_2^k
      | c = 
}}
{{eqn | r = \paren {\sum_{k \mathop = 0}^n a_k \circ X_1^k} \paren {\sum_{k \mathop = 0}^n b_k \circ X_2^k}
      | c = 
}}
{{eqn | r = \map \phi p \map \phi q
      | c = 
}}
{{end-eqn}}
This completes the proof.
{{qed}}
Theorem: Injection is Bijection iff Inverse is Injection

Let $\phi: S \to T$ be an injection.
Then $\phi$ is a bijection {{iff}} its inverse $\phi^{-1}$ is also an injection.

Proof:
=== Necessary Condition ===
Let $\phi$ be a bijection.
Then from Bijection iff Inverse is Bijection, its inverse $\phi^{-1}$ is also a bijection and therefore by definition an injection.
{{qed|lemma}}
Theorem: Division Theorem for Polynomial Forms over Field

Let $\struct {F, +, \circ}$ be a field whose zero is $0_F$ and whose unity is $1_F$.
Let $X$ be transcendental over $F$.
Let $F \sqbrk X$ be the ring of polynomials in $X$ over $F$.
Let $d$ be an element of $F \sqbrk X$ of degree $n \ge 1$.
Then $\forall f \in F \sqbrk X: \exists q, r \in F \sqbrk X: f = q \circ d + r$ such that either:
:$(1): \quad r = 0_F$
or:
:$(2): \quad r \ne 0_F$ and $r$ has degree that is less than $n$.

Proof:
From the equation $0_F = 0_F \circ d + 0_F$, the theorem is true for the trivial case $f = 0_F$.
So, if there is a counterexample to be found, it will have a degree.
{{AimForCont}} there exists at least one counterexample.
By a version of the Well-Ordering Principle, we can assign a number $m$ to the lowest degree possessed by any counterexample.
So, let $f$ denote a counterexample which has that minimum degree $m$.
If $m < n$, the equation $f = 0_F \circ d + f$ would show that $f$ was not a counterexample.
Therefore $m \ge n$.
Suppose $d \divides f$ in $F \sqbrk X$.
Then:
:$\exists q \in F \sqbrk X: f = q \circ d + 0_F$
and $f$ would not be a counterexample.
So $d \nmid f$ in $F \sqbrk X$.
So, suppose that:
{{begin-eqn}}
{{eqn | l = f
      | r = \sum_{k \mathop = 0}^m {a_k \circ X^k}
}}
{{eqn | l = d
      | r = \sum_{k \mathop = 0}^n {b_k \circ X^k}
}}
{{eqn | l = m
      | o = \ge
      | r = n
}}
{{end-eqn}}
We can create the polynomial $\paren {a_m \circ b_n^{-1} \circ X^{m - n} } \circ d$ which has the same degree and leading coefficient as $f$.
Thus $f_1 = f - \paren {a_m \circ b_n^{-1} \circ X^{m - n} } \circ d$ is a polynomial of degree less than $m$.
Since $d \nmid f$, $f_1$ is a non-zero polynomial.
There is no counterexample of degree less than $m$.
Therefore:
:$f_1 = q_1 \circ d + r$
for some $q_1, r \in F \sqbrk X$, where either:
:$r = 0_F$
or:
:$r$ is non-zero with degree strictly less than $n$.
Hence:
{{begin-eqn}}
{{eqn | l = f
      | r = f_1 + \paren {a_m \circ b_n^{-1} \circ X^{m - n} } \circ d
      | c = 
}}
{{eqn | r = \paren {q_1 + a_m \circ b_n^{-1} \circ X^{m - n} } \circ d + r
      | c = 
}}
{{end-eqn}}
Thus $f$ is not a counterexample.
From this contradiction follows the result.
{{qed}}
Theorem: Division Theorem for Polynomial Forms over Field

Let $\struct {F, +, \circ}$ be a field whose zero is $0_F$ and whose unity is $1_F$.
Let $X$ be transcendental over $F$.
Let $F \sqbrk X$ be the ring of polynomials in $X$ over $F$.
Let $d$ be an element of $F \sqbrk X$ of degree $n \ge 1$.
Then $\forall f \in F \sqbrk X: \exists q, r \in F \sqbrk X: f = q \circ d + r$ such that either:
:$(1): \quad r = 0_F$
or:
:$(2): \quad r \ne 0_F$ and $r$ has degree that is less than $n$.

Proof:
Suppose $\map \deg f < \map \deg d$.
Then we take $\map q X = 0$ and $\map r X = \map f X$ and the result holds.
Otherwise, $\map \deg f \ge \map \deg d$.
Let:
:$\map f X = a_0 + a_1 X + a_2 x^2 + \cdots + a_m X^m$
:$\map d X = b_0 + b_1 X + b_2 x^2 + \cdots + b_n X^n$
We can subtract from $f$ a suitable multiple of $d$ so as to eliminate the highest term in $f$:
:$\map f X - \map d X \cdot \dfrac {a_m} {b_n} x^{m - n} = \map p X$
where $\map p X$ is some polynomial whose degree is less than that of $f$.
If $\map p X$ still has degree higher than that of $d$, we do the same thing again.
Eventually we reach:
:$\map f X - \map d X \cdot \paren {\dfrac {a_m} {b_n} x^{m - n} + \dotsb} = \map r X$
where either $r = 0_F$ or $r$ has degree that is less than $n$.
This approach can be formalised using the Principle of Complete Induction.
{{qed}}
Theorem: Division Theorem for Polynomial Forms over Field

Let $\struct {F, +, \circ}$ be a field whose zero is $0_F$ and whose unity is $1_F$.
Let $X$ be transcendental over $F$.
Let $F \sqbrk X$ be the ring of polynomials in $X$ over $F$.
Let $d$ be an element of $F \sqbrk X$ of degree $n \ge 1$.
Then $\forall f \in F \sqbrk X: \exists q, r \in F \sqbrk X: f = q \circ d + r$ such that either:
:$(1): \quad r = 0_F$
or:
:$(2): \quad r \ne 0_F$ and $r$ has degree that is less than $n$.

Proof:
Proof by induction:
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\forall f \in F \sqbrk X: \exists q, r \in F \sqbrk X: f = q \circ d + r$ provided that $\map \deg f < n$
=== Basis for the Induction ===
$\map P 0$ is the statement that $q$ and $r$ exist when $f = 0$.
This is shown trivially to be true by taking $q = r = 0$.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 0$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\forall f \in F \sqbrk X: \exists q, r \in F \sqbrk X: f = q \circ d + r$ provided that $\map \deg f < k$
Then we need to show:
:$\forall f \in F \sqbrk X: \exists q, r \in F \sqbrk X: f = q \circ d + r$ provided that $\map \deg f < k + 1$
=== Induction Step ===
This is our induction step:
Let $f$ be such that $\map \deg f = n$.
Let:
:$f = a_0 + a_1 \circ x + a_2 \circ x^2 + \cdots + a_n \circ x^n$ where $a_n \ne 0$
Let:
:$d = b_0 + b_1 \circ x + b_2 \circ x^2 + \cdots + b_j \circ x^j$ where $b_j \ne 0$
If $n < l$ then take $q = 0, r = f$.
If $n \ge l$, consider:
:$c := f - a_n b_j^{-1} x^{n - j} d$
This has been carefully arranged so that the coefficient of $x^n$ in $c$ is zero.
Thus $\map \deg c < n$.
Therefore, by the induction hypothesis:
:$c = d q_0 + r$
where $\map \deg r < \map \deg d$.
Therefore:
{{begin-eqn}}
{{eqn | l = f
      | r = d \paren {q_0 + a_n b_j^{-1} x^{n - j} } + r
      | c = 
}}
{{eqn | r = d q + r
      | c = where $\map \deg r < \map \deg d$ and $q = q_0 + a_n b_j^{-1} x^{n - j}$
}}
{{end-eqn}}
Thus the existence of $q$ and $r$ have been established.
As for uniqueness, assume:
:$d q + r = d q' + r'$
with $\map \deg r < \map \deg d, \map \deg {r'} < \map \deg d$
Then:
:$d \paren {q - q'} = r' - r$
By Degree of Sum of Polynomials:
:$\map \deg {r' - r} \le \max \set {\map \deg {r'}, \map \deg r} < \map \deg d$
and by Degree of Product of Polynomials over Integral Domain:
:$\map \deg {d \paren {q - q'} } = \map \deg d + \map \deg {q - q'}$
That is:
:$\map \deg d < \map \deg d + \map \deg {q - q'}$
and the only way for that to happen is for:
:$\map \deg {q - q'} = -\infty$
that is, for $q - q'$ to be the null polynomial.
That is, $q - q' = 0_F$ and by a similar argument $r' - r = 0_F$, demonstrating the uniqueness of $q$ and $r$.
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall f \in F \sqbrk X: \exists q, r \in F \sqbrk X: f = q \circ d + r$ such that either:
::$(1): \quad r = 0_F$
:or:
::$(2): \quad r \ne 0_F$ and $r$ has degree that is less than $n$.
{{qed}}
Theorem: Polynomial Forms over Field form Principal Ideal Domain

Let $\struct {F, +, \circ}$ be a field whose zero is $0_F$ and whose unity is $1_F$.
Let $X$ be transcendental over $F$.
Let $F \sqbrk X$ be the ring of polynomials in $X$ over $F$.
Then $F \sqbrk X$ is a principal ideal domain.

Proof:
For any $d \in F \sqbrk X$, let $\ideal d$ denote the principal ideal of $F \sqbrk X$ generated by $d$.
Let $J$ be any ideal of $F \sqbrk X$. What we need to prove is that $J$ is a principal ideal.
Let us first distinguish the following two cases for $J$:
:If $J = \set {0_F}$, then by Zero Element Generates Null Ideal $J = \ideal {0_F}$, and hence is a principal ideal.
:If $J = F \sqbrk X$, then by Ideal of Unit is Whole Ring: Corollary $J = \ideal {1_F}$, and hence is a principal ideal. 
Now suppose $J \ne \set {0_F}$ and $J \ne F \sqbrk X$.
Then $J$ necessarily contains a non-zero element.
By the Well-Ordering Principle, we can introduce the lowest degree of a non-zero element of $J$.
Denote this degree by $n$.
If $n = 0$, then $J$ contains a polynomial of degree $0$.
This is a non-zero element of $F$.
As $F$ is a field, this is therefore a unit of $F$, and thus by Ideal of Unit is Whole Ring, $J = F \sqbrk X$.
Because the degree of a non-zero element is a natural number, we conclude that $n \ge 1$.
Now let $d$ be a polynomial of degree $n$ in $J$, and let $f \in J$.
By Division Theorem for Polynomial Forms over Field, $f = q \circ d + r$ for some $q, r \in F \sqbrk X$ where either:
:$r = 0_F$
or:
:$r$ is a polynomial of degree smaller than $n$.
Because $J$ is an ideal and $d \in J$, it follows that:
:$q \circ d \in J$
Since $f \in J$, we also conclude:
:$r = f - q \circ d \in J$
From the construction of $d$, it follows that we must have $r = 0_F$.
Therefore:
:$f = q \circ d$
and thus:
:$f \in \ideal d$.
This reasoning shows that:
:$J \subseteq \ideal d$
From property $(3)$ of the principal ideal $\ideal d$, we conclude that:
:$\ideal d \subseteq J$
as $d \in J$.
Hence $J = \ideal d$.
These $2$ distinguished cases cover all of the possible ideals of $F \sqbrk X$. 
Hence $F \sqbrk X$ is a principal ideal domain.
{{qed}}
Theorem: Polynomial Forms over Field form Principal Ideal Domain

Let $\struct {F, +, \circ}$ be a field whose zero is $0_F$ and whose unity is $1_F$.
Let $X$ be transcendental over $F$.
Let $F \sqbrk X$ be the ring of polynomials in $X$ over $F$.
Then $F \sqbrk X$ is a principal ideal domain.

Proof:
We have that Polynomial Forms over Field is Euclidean Domain.
We also have that Euclidean Domain is Principal Ideal Domain.
Hence the result.
{{qed}}
Theorem: Equal Consecutive Prime Number Gaps are Multiples of Six

If you list the gaps between consecutive primes greater than $5$:
:$2, 4, 2, 4, 2, 4, 6, 2, 6, 4, 2, 4, \ldots$
you will notice that consecutive gaps that are equal are of the form $6 x$.
This is ''always'' the case.
{{OEIS|A001223}}

Proof:
Suppose there were two consecutive gaps between $3$ consecutive prime numbers that were equal, but not divisible by $6$.
Then the difference is $2 k$ where $k$ is not divisible by $3$.
Therefore the (supposed) prime numbers will be:
:$p, p + 2 k, p + 4 k$
But then $p + 4 k$ is congruent modulo $3$ to $p + k$.
That makes the three numbers congruent modulo $3$ to $p, p + k, p + 2k$.
One of those is divisible by $3$ and so cannot be prime.
So two consecutive gaps must be divisible by $3$ and therefore (as they have to be even) by $6$.
{{qed}}
Category:Prime Numbers
hgu4ntr4d4lxwd1liht6gqklzardaqc
Theorem: Standard Discrete Metric is Metric

The standard discrete metric is a metric.

Proof:
Let $d: S \times S \to \R$ denote the standard discrete metric on the underlying set $S$ of some space $\struct {S, d}$.
By definition:
:$\forall x, y \in S: \map d {x, y} = \begin {cases} 0 & : x = y  \\ 1 & : x \ne y \end {cases}$
Theorem: Derivative of Constant

Let $\map {f_c} x$ be the constant function on $\R$, where $c \in \R$.
Then:
:$\map { {f_c}'} x = 0$

Proof:
The function $f_c: \R \to \R$ is defined as:
:$\forall x \in \R: \map {f_c} x = c$
Thus:
{{begin-eqn}}
{{eqn | l = \map { {f_c}'} x
      | r = \lim_{\delta x \mathop \to 0} \frac {\map {f_c} {x + \delta x} - \map {f_c} x} {\delta x}
      | c = {{Defof|Differentiation}}
}}
{{eqn | r = \lim_{\delta x \mathop \to 0} \frac {c - c} {\delta x}
      | c =
}}
{{eqn | r = \lim_{\delta x \mathop \to 0} \frac 0 {\delta x}
      | c =
}}
{{eqn | r = 0
      | c =
}}
{{end-eqn}}
{{qed}}
Theorem: Product Rule for Derivatives

Let $\map f x, \map j x, \map k x$ be real functions defined on the open interval $I$.
Let $\xi \in I$ be a point in $I$ at which both $j$ and $k$ are differentiable.
Let $\map f x = \map j x \map k x$.
Then:
:$\map {f'} \xi = \map j \xi \map {k'} \xi + \map {j'} \xi \map k \xi$
It follows from the definition of derivative that if $j$ and $k$ are both differentiable on the interval $I$, then:
:$\forall x \in I: \map {f'} x = \map j x \map {k'} x + \map {j'} x \map k x$

Proof:
First we note that from Differentiable Function is Continuous, $j$ is continuous at $\xi$.
Hence:
:$(1): \quad \map j {\xi + h} \to \map j \xi$ as $h \to 0$
So:
{{begin-eqn}}
{{eqn | l = \map {f'} \xi
      | r = \lim_{h \mathop \to 0} \frac {\map f {\xi + h} - \map f \xi} h
      | c = {{Defof|Derivative}}
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\map j {\xi + h} \map k {\xi + h} - \map j \xi \map k \xi} h
      | c = {{hypothesis}}
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\map j {\xi + h} \map k {\xi + h} - \map j {\xi + h} \map k \xi + \map j {\xi + h} \map k \xi - \map j \xi \map k \xi} h
      | c = adding $\pm \map j {\xi + h} \map k \xi$ to numerator
}}
{{eqn | r = \lim_{h \mathop \to 0} \paren {\map j {\xi + h} \frac {\map k {\xi + h} - \map k \xi} h + \frac {\map j {\xi + h} - \map j \xi} h \map k \xi}
      | c = simplifying
}}
{{eqn | r = \lim_{h \mathop \to 0} \paren {\map j {\xi + h} \frac {\map k {\xi + h} - \map k \xi} h} +  \lim_{h \mathop \to 0} \paren {\frac {\map j {\xi + h} - \map j \xi} h \map k \xi}
      | c = Sum Rule for Limits of Real Functions
}}
{{eqn | r = \lim_{h \mathop \to 0} \paren {\map j {\xi + h} } \lim_{h \mathop \to 0} \paren {\frac {\map k {\xi + h} - \map k \xi} h} + \lim_{h \mathop \to 0} \paren {\frac {\map j {\xi + h} - \map j \xi} h} \lim_{h \mathop \to 0} \paren {\map k \xi}
      | c = Product Rule for Limits of Real Functions
}}
{{eqn | r = \lim_{h \mathop \to 0} \paren {\map j {\xi + h} } \map {k'} \xi + \map {j'} \xi \lim_{h \mathop \to 0} \paren {\map k \xi}
      | c = {{Defof|Derivative}}
}}
{{eqn | r = \map j \xi \map {k'} \xi + \map {j'} \xi \map k \xi
      | c = from $(1)$
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Composite Function

Let $I, J$ be open real intervals.
Let $g : I \to J$ and $f : J \to \R$ be real functions.
Let $h : I \to \R$ be the real function defined as:
:$\forall x \in I: \map h x = \map {f \circ g} x = \map f {\map g x}$
Then, for each $x_0 \in I$ such that:
:$g$ is differentiable at $x_0$
:$f$ is differentiable at $\map g {x_0}$
it holds that $h$ is differentiable at $x_0$ and:
:$\map {h'} {x_0} = \map {f'} {\map g {x_0}} \map {g'} {x_0}$
where $h'$ denotes the derivative of $h$.
Using the $D_x$ notation:
:$\map {D_x} {\map f {\map g x} } = \map {D_{\map g x} } {\map f {\map g x} } \map {D_x} {\map g x}$

Proof:
Some sources, introducing the Derivative of Composite Function at elementary level, provide the following non-rigorous argument:
:''If $z$ is a function of $y$ where $y$ itself is some function of $x$,''
::''it is obvious that:''
:::$\dfrac {\delta z} {\delta x} = \dfrac {\delta z} {\delta y} \cdot \dfrac {\delta y} {\delta x}$
::''since these quantities being finite can be cancelled as in Arithmetic.''
:''If we now let the quantities concerned tend to zero, taking the limit, we get
:::$\dfrac {\d z} {\d x} = \dfrac {\d z} {\d y} \cdot \dfrac {\d y} {\d x}$
However, this informal argument is insufficiently rigorous for {{ProofWiki}}.
Hence, this must '''not''' be interpreted to mean that derivatives can be treated as fractions.
It simply is a convenient notation.