avewright/proofwiki-math huggingface dataset:
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:
Let $f, g, x_0$ satisfy the conditions of the theorem.
Define $g^* : I \to \R$ as:
:$\map {g^*} x = \begin{cases} \dfrac {\map g x - \map g {x_0}} {x - x_0} & : x \ne x_0 \\ \map {g'} {x_0} & : x = x_0 \end{cases}$
Then, for every $x \in I$:
:$\paren 1: \quad \map g x - \map g {x_0} = \paren {x - x_0} \map {g^*} x$
for when $x = x_0$, both sides are equal to $0$.
Furthermore, by the definition of derivative, it follows that $g^*$ is continuous at $x_0$.
Define $y_0 := \map g {x_0}$
In the same way, define $f^* : J \to \R$ as:
:$\map {f^*} y = \begin{cases} \dfrac {\map f y - \map f {y_0}} {y - y_0} & : y \ne y_0 \\ \map {f'} {y_0} & : y = y_0 \end{cases}$
Likewise, for every $y \in J$:
:$\paren 2: \quad \map f y - \map f {y_0} = \paren {y - y_0} \map {f^*} y$
and $f^*$ is continuous at $y_0$.
Now, for every $x \in I$, we have:
{{begin-eqn}}
{{eqn | l = \map f {\map g x} - \map f {\map g {x_0} }
      | r = \map f {\map g x} - \map f {y_0}
      | c = Definition of $y_0$
}}
{{eqn | r = \paren {\map g x - y_0} \map {f^*} {\map g x}
      | c = By $\paren 2$
}}
{{eqn | r = \paren {\map g x - \map g {x_0} } \map {f^*} {\map g x}
      | c = Definition of $y_0$
}}
{{eqn | n = 3
      | r = \paren {x - x_0} \map {g^*} x \map {f^*} {\map g x}
      | c = By $\paren 1$
}}
{{end-eqn}}
Therefore, we have:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to x_0} \frac {\map h x - \map h {x_0} } {x - x_0}
      | r = \lim_{x \mathop \to x_0} \frac {\map f {\map g x} - \map f {\map g {x_0} } } {x - x_0}
      | c = Definition of $h$
}}
{{eqn | r = \lim_{x \mathop \to x_0} \map {g^*} x \map {f^*} {\map g x}
      | c = By $\paren 3$
}}
{{eqn | r = \paren {\lim_{x \mathop \to x_0} \map {g^*} x} \paren {\lim_{x \mathop \to x_0} \map {f^*} {\map g x} }
      | c = Product Rule for Limits of Real Functions
}}
{{eqn | r = \paren {\lim_{x \mathop \to x_0} \map {g^*} x} \map {f^*} {\lim_{x \mathop \to x_0} \map g x}
      | c = Limit of Composite Function: '''Hypothesis 1'''
}}
{{eqn | r = \map {g^*} {x_0} \map {f^*} {\map g {x_0} }
      | c = Differentiable Function is Continuous, {{Defof|Continuous Real Function at Point}}
}}
{{eqn | r = \map {g'} {x_0} \map {f'} {\map g {x_0} }
      | c = Definitions of $g^*$ and $f^*$
}}
{{end-eqn}}
Therefore, by definition of derivative:
:$\map {h'} {x_0} = \map {f'} {\map g {x_0}} \map {g'} {x_0}$
{{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:
Let $\map g x = y$, and let:
{{begin-eqn}}
{{eqn | l = \map g {x + \delta x}
      | r = y + \delta y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \delta y
      | r = \map g {x + \delta x} - \map g x
      | c = 
}}
{{end-eqn}}
Thus:
:$\delta y \to 0$ as $\delta x \to 0$
and:
:$(1): \quad \dfrac {\delta y} {\delta x} \to \map {g'} x$
There are two cases to consider:
=== Case 1 ===
Suppose $\map {g'} x \ne 0$ and that $\delta x$ is small but non-zero.
Then $\delta y \ne 0$ from $(1)$ above, and:
{{begin-eqn}}
{{eqn | l = \lim_{\delta x \mathop \to 0} \frac {\map h {x + \delta x} - \map h x} {\delta x}
      | r = \lim_{\delta x \mathop \to 0} \frac {\map f {\map g {x + \delta x} } - \map f {\map g x} } {\map g {x + \delta x} - \map g x} \frac {\map g {x + \delta x} - \map g x} {\delta x}
      | c = 
}}
{{eqn | r = \lim_{\delta x \mathop \to 0} \frac {\map f {y + \delta y} - \map f y} {\delta y} \frac {\delta y} {\delta x}
      | c = 
}}
{{eqn | r = \map {f'} y \map {g'} x
      | c = 
}}
{{end-eqn}}
hence the result.
{{qed|lemma}}
=== Case 2 ===
Now suppose $\map {g'} x = 0$ and that $\delta x$ is small but non-zero.
Again, there are two possibilities:
=== Case 2a ===
If $\delta y = 0$, then $\dfrac {\map h {x + \delta x} - \map h x} {\delta x} = 0$.
Hence the result.
{{qed|lemma}}
=== Case 2b ===
If $\delta y \ne 0$, then:
:$\dfrac {\map h {x + \delta x} - \map h x} {\delta x} = \dfrac {\map f {y + \delta y} - \map f y} {\delta y} \dfrac {\delta y} {\delta x}$
As $\delta y \to 0$:
:$(1): \quad \dfrac {\map f {y + \delta y} - \map f y} {\delta y} \to \map {f'} y$
:$(2): \quad \dfrac {\delta y} {\delta x} \to 0$
Thus:
:$\ds \lim_{\delta x \mathop \to 0} \frac {\map h {x + \delta x} - \map h x} {\delta x} \to 0 = \map {f'} y \map {g'} x$
Again, hence the result.
{{qed|lemma}}
All cases have been covered, so by Proof by Cases, the result is complete.
{{qed}}
Theorem: Derivative of Inverse Function

Let $I = \closedint a b$ and $J = \closedint c d$ be closed real intervals.
Let $I^o = \openint a b$ and $J^o = \openint c d$ be the corresponding open real intervals.
Let $f: I \to J$ be a real function which is continuous on $I$ and differentiable on $I^o$ such that $J = f \sqbrk I$.
Let either:
:$\forall x \in I^o: D \map f x > 0$
or:
:$\forall x \in I^o: D \map f x < 0$
Then:
:$f^{-1}: J \to I$ exists and is continuous on $J$
:$f^{-1}$ is differentiable on $J^o$
:$\forall y \in J^o: D \map {f^{-1} } y = \dfrac 1 {D \map f x}$

Proof:
From Derivative of Monotone Function, it follows that $f$ is either:
:strictly increasing on $I$ (if $\forall x \in I^o: D \, \map f x > 0$)
or:
:strictly decreasing on $I$ (if $\forall x \in I^o: D \, \map f x < 0$).
Therefore from Inverse of Strictly Monotone Function it follows that $f^{-1}: J \to I$ exists.
As $f$ is continuous, from Image of Real Interval under Continuous Real Function is Real Interval it follows that $J$ is an interval.
By {{Corollary|Limit of Monotone Real Function/Increasing|disp = Limit of Monotone Function: Increasing}} and {{Corollary|Limit of Monotone Real Function/Decreasing|disp = Limit of Monotone Function: Decreasing}}, $f^{-1}: J \to I$ is continuous.
Next its derivative is to be considered.
Suppose $f$ is strictly increasing.
Let $y \in J^o$.
Then $\map {f^{-1} } y \in I^o$.
Let $k = \map {f^{-1} } {y + h} - \map {f^{-1} } y$.
Thus:
:$\map {f^{-1} } {y + h} = \map {f^{-1} } y + k = x + k$
Thus:
:$y + h = \map f {x + k}$
and hence:
:$h = \map f {x + k} - y = \map f {x + k} - \map f x$
Since $f^{-1}$ is continuous on $J$, it follows that $k \to 0$ as $h \to 0$.
Also, $f^{-1}$ is strictly increasing from Inverse of Strictly Monotone Function and so $k \ne 0$ unless $h = 0$.
So by Limit of Composite Function we get:
:$\dfrac {\map {f^{-1} } {y + h} - \map {f^{-1} } y} h = \dfrac k {\map f {x + k} - \map f x}$
Thus:
:$\dfrac {\map {f^{-1} } {y + h} - \map {f^{-1} } y} h \to \dfrac 1 {D \map f x}$
as $h \to 0$.
Suppose $f$ is strictly decreasing.
Exactly the same argument applies.
{{qed}}
Theorem: Upper Darboux Sum Never Smaller than Lower Darboux Sum

Let $\closedint a b$ be a closed interval of the set $\R$ of real numbers.
Let $P = \set {x_0, x_1, x_2, \ldots, x_{n - 1}, x_n}$ be a finite subdivision of $\closedint a b$.
Let $f: \R \to \R$ be a real function.
Let $f$ be bounded on $\closedint a b$.
Let $\map L P$ be the lower Darboux sum of $\map f x$ on $\closedint a b$ belonging to the subdivision $P$.
Let $\map U P$ be the upper Darboux sum of $\map f x$ on $\closedint a b$ belonging to the subdivision $P$.
Then $\map L P \le \map U P$.

Proof:
For all $\nu \in 1, 2, \ldots, n$, let $\closedint {x_{\nu - 1} } {x_\nu}$ be a closed subinterval of $\closedint a b$.
As $f$ is bounded on $\closedint a b$, it is bounded on $\closedint {x_{\nu - 1} } {x_\nu}$.
So, let $m_\nu$ be the infimum and $M_\nu$ be the supremum of $\map f x$ on the interval $\closedint {x_{\nu - 1} } {x_\nu}$.
By definition, $m_\nu \le M_\nu$.
So $m_\nu \paren {x_\nu - x_{\nu - 1} } \le M_{\nu} \paren {x_\nu - x_{\nu - 1} }$.
It follows directly that $\ds \sum_{\nu \mathop = 1}^n m_\nu \paren {x_\nu - x_{\nu - 1} } \le \sum_{\nu \mathop = 1}^n M_\nu \paren {x_\nu - x_{\nu - 1} }$.
{{qed}}
Theorem: Dedekind's Theorem

Let $\tuple {L, R}$ be a Dedekind cut of the set of real numbers $\R$.
Then there exists a unique real number which is a producer of $\tuple {L, R}$.

Proof:
Suppose $P$ and $Q$ are two properties which are mutually exclusive.
Suppose that one of either of $P$ and $Q$ are possessed by every $x \in \R$.
Suppose that any number having $P$ is less than any which have $Q$.
Let us call the numbers with $P$ the ''left hand set'' $L$, and the ones with $Q$ the ''right hand set'' $R$.
There are two possibilities, as follows.
* $L$ has a greatest element, or
* $R$ has a least element.
'''It is not possible that both of the above can happen.'''
Because suppose $l$ is the greatest element of $L$ and $r$ is the least element of $R$.
Then the number $\dfrac {l + r} 2$ is greater than $l$ and less than $r$, so it could not be in either class.
'''However, one of the above ''must'' occur.'''
Because, suppose the following.
Let $L_1$ and $R_1$ be the subsets of $L$ and $R$ respectively consisting of only the rational numbers in $L$ and $R$.
Then $L_1$ and $R_1$ form a section of the set of rational numbers $\Q$.
There are two cases to think about:
'''Maybe $L_1$ has a greatest element $\alpha$.'''
In this case, $\alpha$ must also be the greatest element of $L$.
Because if not, then there's a greater one, which we can call $\beta$.
There are always rational numbers between $\alpha$ and $\beta$ from Rational Numbers are Densely Ordered.
These are less than $\beta$ and thus belong to $L$ and (because they're rational) also to $L_1$.
This is a contradiction, so if $\alpha$ is the greatest element of $L_1$, it's also the greatest element of $L$.
'''On the other hand, $L_1$ may ''not'' have a greatest element.'''
In this case, the section of the rational numbers formed by $L_1$ and $R_1$ is a real number $\alpha$.
{{Explain|Justify the above assertion.}}
It must belong to either $L$ or $R$.
If it belongs to $L$ we can show, like we did before, that it is the greatest element of $L$.
Similarly, if it belongs to $R$ we can show it is the least element of $R$.
So in any case, either $L$ has a greatest element or $R$ has a least element.
Thus, any section of the real numbers corresponds to a real number.
{{qed}}
Theorem: Dedekind's Theorem

Let $\tuple {L, R}$ be a Dedekind cut of the set of real numbers $\R$.
Then there exists a unique real number which is a producer of $\tuple {L, R}$.

Proof:
=== Proof of Uniqueness ===
{{AimForCont}} both $\alpha$ and $\beta$ produce $\tuple {L, R}$.
By the Trichotomy Law for Real Numbers either $\beta < \alpha$ or $\alpha < \beta$.
Suppose that $\beta < \alpha$.
From Real Numbers are Densely Ordered, there exists at least one real number $c$ such that $\beta < c$ and $c < \alpha$.
Because $c < \alpha$, it must be the case that $c \in L$.
Because $\beta < c$, it must be the case that $c \in R$.
That is:
:$c \in L \cap R$
But by the definition of Dedekind Cut, $\tuple {L, R}$ is a partition of $\R$.
That is, $L$ and $R$ are disjoint.
That is:
:$L \cap R = \O$
This is a contradiction.
Similarly, $\alpha < \beta$ also leads to a contradiction.
It follows that $\alpha$ is unique.
{{qed|lemma}}
=== Proof of Existence ===
Let $\alpha = \sup L$.
Let $u_1 \in \R$ such that $u_1 < \alpha$.
{{AimForCont}} $u_1 \in R$.
Suppose there is no real number $s \in L$ such that $u_1 < s \le \alpha$.
Then $u_1$ would be an upper bound of $L$ which is less than $\sup {L}$.
This is a contradiction.
So there exists at least one real number $s \in L$ such that $u_1 < s \le \alpha$.
But this is also a contradiction because all the elements of $R$ are greater than all the elements of $L$.
It follows that $u_1 \in L$.
Let $u_2 \in \R$ such that $\alpha < u_2$.
{{AimForCont}} $u_2 \in L$.
There exists $s' \in \R$ such that $\alpha < s' < u_2$.
But $s' \notin L$ and thus $s' \in R$.
This is a contradiction because all the elements of $R$ are greater than all the elements of $L$.
It follows that $u_2 \in R$.
Hence, $\alpha$ produces the cut $\tuple {L, R}$.
{{qed}}
Theorem: Dedekind's Theorem

Let $\tuple {L, R}$ be a Dedekind cut of the set of real numbers $\R$.
Then there exists a unique real number which is a producer of $\tuple {L, R}$.

Proof:
=== Proof of Uniqueness ===
{{AimForCont}} both $\alpha$ and $\beta$ produce $\tuple {L, R}$.
By the Trichotomy Law for Real Numbers either $\beta < \alpha$ or $\alpha < \beta$.
Suppose that $\beta < \alpha$.
From Real Numbers are Densely Ordered, there exists at least one real number $c$ such that $\beta < c$ and $c < \alpha$.
Because $c < \alpha$, it must be the case that $c \in L$.
Because $\beta < c$, it must be the case that $c \in R$.
That is:
:$c \in L \cap R$
But by the definition of Dedekind Cut, $\tuple {L, R}$ is a partition of $\R$.
That is, $L$ and $R$ are disjoint.
That is:
:$L \cap R = \O$
This is a contradiction.
Similarly, $\alpha < \beta$ also leads to a contradiction.
It follows that $\alpha$ is unique.
{{qed|lemma}}
=== Proof of Existence ===
Let $\gamma$ be the set of all rational numbers $p$ such that $p \in \alpha$ for some $\alpha \in L$.
It is to be verified that $\gamma$ is a cut.
Because $L$ is not empty, neither is $\gamma$.
Suppose $\beta \in \R$ and $q \notin \beta$.
Then because $\alpha < \beta$, we have that $q \notin \alpha$ for any $\alpha \in L$.
Thus $q \notin \gamma$.
Thus $\gamma$ satisfies criterion $(1)$ for being a cut.
Suppose $p \in \gamma$ and $q < p$.
Then $p \in \alpha$ for some $\alpha \in L$.
Hence $q \in \alpha$.
Hence $q \in \gamma$.
Thus $\gamma$ satisfies criterion $(2)$ for being a cut.
Suppose $p \in \gamma$.
Then $p \in \alpha$ for some $\alpha \in L$.
Hence there exists $q > p$ such that $q \in \alpha$.
Hence $q \in \gamma$.
Thus $\gamma$ satisfies criterion $(3)$ for being a cut.
Thus, by definition of the real numbers by identifying them with cuts, $\gamma$ is a real number.
We have that:
:$\alpha \le \gamma$
for all $\alpha \in L$.
{{AimForCont}} there exists $\beta \in R$ such that $\beta < \gamma$.
Then there exists some rational number $p \in\ Q$ such that $p \in \gamma$ and $p \notin beta$.
But if $p \in \gamma$ then $p \in \alpha$ for some $\alpha\ in L$.
This implies that $\beta < \alpha$.
But this contradicts the definition of Dedekind cut:
:$(3): \quad \forall x \in L: \forall y \in R: x < y$
Thus $\gamma \le \beta$ for all $\beta \in R$.
That is, $\gamma$ is a producer of $\tuple {L, R}$.
{{qed}}
Theorem: Complex Addition is Closed

The set of complex numbers $\C$ is closed under addition:
:$\forall z, w \in \C: z + w \in \C$

Proof:
From the informal definition of complex numbers, we define the following:
:$z = x_1 + i y_1$
:$w = x_2 + i y_2$
where $i = \sqrt {-1}$ and $x_1, x_2, y_1, y_2 \in \R$.
Then from the definition of complex addition:
:$z + w = \paren {x_1 + x_2} + i \paren {y_1 + y_2}$
From Real Numbers under Addition form Group, real addition is closed.
So:
:$\paren {x_1 + x_2} \in \R$ and $\paren {y_1 + y_2} \in \R$
Hence the result.
{{qed}}
Theorem: Complex Addition is Closed

The set of complex numbers $\C$ is closed under addition:
:$\forall z, w \in \C: z + w \in \C$

Proof:
From the formal definition of complex numbers, we have:
:$z = \tuple {x_1, y_1}$
:$w = \tuple {x_2, y_2}$
where $x_1, x_2, y_1, y_2 \in \R$.
Then from the definition of complex addition:
:$z + w = \tuple {x_1 + x_2, y_1 + y_2}$
From Real Numbers under Addition form Group, real addition is closed.
So:
:$\paren {x_1 + x_2} \in \R$ and $\paren {y_1 + y_2} \in \R$
and hence the result.
{{qed}}
Theorem: Complex Addition is Associative

The operation of addition on the set of complex numbers $\C$ is associative:
:$\forall z_1, z_2, z_3 \in \C: z_1 + \paren {z_2 + z_3} = \paren {z_1 + z_2} + z_3$

Proof:
From the definition of complex numbers, we define the following:
{{begin-eqn}}
{{eqn | l = z_1
      | o = :=
      | r = \tuple {x_1, y_1}
}}
{{eqn | l = z_2
      | o = :=
      | r = \tuple {x_2, y_2}
}}
{{eqn | l = z_3
      | o = :=
      | r = \tuple {x_3, y_3}
}}
{{end-eqn}}
where $x_1, x_2, x_3, y_1, y_2, y_3 \in \R$.
Thus:
{{begin-eqn}}
{{eqn | l = z_1 + \paren {z_2 + z_3}
      | r = \tuple {x_1, y_1} + \paren {\tuple {x_2, y_2} + \tuple {x_3, y_3} }
      | c = {{Defof|Complex Number|index = 2}}
}}
{{eqn | r = \tuple {x_1, y_1} + \paren {\tuple {x_2 + x_3, y_2 + y_3} }
      | c = {{Defof|Complex Number/Definition 2/Addition|Complex Addition}}
}}
{{eqn | r = \tuple {x_1 + \paren {x_2 + x_3}, y_1 + \paren {y_2 + y_3} }
      | c = {{Defof|Complex Number/Definition 2/Addition|Complex Addition}}
}}
{{eqn | r = \tuple {\paren {x_1 + x_2} + x_3, \paren {y_1 + y_2} + y_3}
      | c = Real Addition is Associative
}}
{{eqn | r = \paren {\tuple {x_1 + x_2, y_1 + y_2} } + \tuple {x_3, y_3}
      | c = {{Defof|Complex Number/Definition 2/Addition|Complex Addition}}
}}
{{eqn | r = \paren {\tuple {x_1, y_1} + \tuple {x_2, y_2} } + \tuple {x_3, y_3}
      | c = {{Defof|Complex Number/Definition 2/Addition|Complex Addition}}
}}
{{eqn | r = \paren {z_1 + z_2} + z_3
      | c = {{Defof|Complex Number|index = 2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Complex Addition is Commutative

The operation of addition on the set of complex numbers is commutative:
:$\forall z, w \in \C: z + w = w + z$

Proof:
From the definition of complex numbers, we define the following:
{{begin-eqn}}
{{eqn | l = z
      | o = :=
      | r = \tuple {x_1, y_1}
}}
{{eqn | l = w
      | o = :=
      | r = \tuple {x_2, y_2}
}}
{{end-eqn}}
where $x_1, x_2, y_1, y_2 \in \R$.
Then:
{{begin-eqn}}
{{eqn | l = z + w
      | r = \tuple {x_1, y_1} + \tuple {x_2, y_2}
      | c = {{Defof|Complex Number|index = 2}}
}}
{{eqn | r = \tuple {x_1 + x_2, y_1 + y_2}
      | c = {{Defof|Complex Number/Definition 2/Addition|Complex Addition}}
}}
{{eqn | r = \tuple {x_2 + x_1, y_2 + y_1}
      | c = Real Addition is Commutative
}}
{{eqn | r = \tuple {x_2, y_2} + \tuple {x_1, y_1}
      | c = {{Defof|Complex Number/Definition 2/Addition|Complex Addition}}
}}
{{eqn | r = w + z
      | c = {{Defof|Complex Number|index = 2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Integers are Countably Infinite

The set $\Z$ of integers is countably infinite.

Proof:
Define the inclusion mapping $i: \N \to \Z$.
From Inclusion Mapping is Injection, $i: \N \to \Z$ is an injection.
Thus there exists an injection from $\N$ to $\Z$.
Hence $\Z$ is infinite.
Next, let us arrange $\Z$ in the following order:
:$\Z = \set {0, 1, -1, 2, -2, 3, -3, \ldots}$
Then we can directly see that we can define a mapping $\phi: \Z \to \N$ as follows:
:$\forall x \in \Z: \map \phi x = \begin{cases} 2 x - 1 & : x > 0 \\ -2 x & : x \le 0 \end{cases}$
This is shown to be an injection as follows:
Let $\map \phi x = \map \phi y$.
Then one of the following applies:
: $(1): \quad -2 x = -2 y$ in which case $x = y$
: $(2): \quad 2 x - 1 = 2 y - 1$ in which case $2 x = 2 y$ and so $x = y$
: $(3): \quad 2 x - 1 = -2 y$ in which case $y = -x + \frac 1 2$ and therefore $y \notin \Z$
: $(4): \quad 2 y - 1 = -2 x$ in which case $x = -y + \frac 1 2$ and therefore $x \notin \Z$.
So $2 x - 1 = -2 y$ and $2 y - 1 = -2 x$ can't happen and so $x = y$.
Thus $\phi$ is injective.
The result follows from Domain of Injection to Countable Set is Countable.
{{qed}}
Theorem: Permutation of Determinant Indices

Let $\mathbf A = \sqbrk a_n$ be a square matrix of order $n$ over a field.
Let $\lambda: \N_{> 0} \to \N_{> 0}$ be any fixed permutation on $\N_{> 0}$.
Let $\map \det {\mathbf A}$ be the determinant of $\mathbf A$.
Let $\struct {S_n, \circ}$ be the symmetric group of $n$ letters. 
Then:
:$\ds \map \det {\mathbf A} = \sum_{\mu \mathop \in S_n} \paren {\map \sgn \mu \map \sgn \lambda \prod_{k \mathop = 1}^n a_{\map \lambda k, \map \mu k} }$
:$\ds \map \det {\mathbf A} = \sum_{\mu \mathop \in S_n} \paren {\map \sgn \mu \map \sgn \lambda \prod_{k \mathop = 1}^n a_{\map \mu k, \map \lambda k} }$
where:
:the summation $\ds \sum_{\mu \mathop \in S_n}$ ranges over all the $n!$ permutations of $\set {1, 2, \ldots, n}$
:$\map \sgn \mu$ is the sign of the permutation $\mu$.

Proof:
First it is shown that:
:$\ds \map \det {\mathbf A} = \sum_{\mu \mathop \in S_n} \paren {\map \sgn \mu \map \sgn \lambda \prod_{k \mathop = 1}^n a_{\map \lambda k, \map \mu k} }$
Let $\nu: \N_{> 0} \to \N_{> 0}$ be a permutation on $\N_{> 0}$ such that $\nu \circ \lambda = \mu$.
The product can be rearranged as:
:$\ds \prod_{k \mathop = 1}^n a_{\map \lambda k, \map \mu k} = a_{\map \lambda 1, \map \mu 1} a_{\map \lambda 2, \map \mu 2} \cdots a_{\map \lambda n, \map \mu n} = a_{1, \map \nu 1} a_{2, \map \nu 2} \cdots a_{n, \map \nu n} = \prod_{k \mathop = 1}^n a_{k, \map \nu k}$
from {{Field-axiom|M2}}.
By Parity Function is Homomorphism:
:$\map \sgn \mu \map \sgn \lambda = \map \sgn \lambda \map \sgn \nu \map \sgn \lambda = \map {\sgn^2} \lambda \map \sgn \nu = \map \sgn \nu$
and so:
:$\ds \map \det {\mathbf A} = \sum_{\nu \mathop \in S_n} \paren {\map \sgn \nu \prod_{k \mathop = 1}^n a_{k, \map \nu k} }$
which is the usual definition for the determinant.
Next it is to be shown:
:$\ds \map \det {\mathbf A} = \sum_{\mu \mathop \in S_n} \paren {\map \sgn \mu \map \sgn \lambda \prod_{k \mathop = 1}^n a_{\map \mu k, \map \lambda k} }$
Let $\nu: \N_{> 0} \to \N_{> 0}$ be a permutation on $\N_{> 0}$ such that $\nu \circ \mu = \lambda$.
The result follows via a similar argument.
{{Qed}}
Category:Determinants
rfhsivi5almvkkmwlywdnizx0lh6vci
Theorem: Determinant of Transpose

Let $\mathbf A = \sqbrk a_n$ be a square matrix of order $n$.
Let $\map \det {\mathbf A}$ be the determinant of $\mathbf A$.
Let $\mathbf A^\intercal$ be the transpose of $\mathbf A$.
Then:
:$\map \det {\mathbf A} = \map \det {\mathbf A^\intercal}$

Proof:
Let $\mathbf A = \begin{bmatrix}
a_{11} & a_{12} & \ldots & a_{1n} \\
a_{21} & a_{22} & \cdots & a_{2n} \\
\vdots & \vdots & \ddots & \vdots \\
a_{n1} & a_{n2} & \cdots & a_{nn} \\
\end{bmatrix}$.
Then $\mathbf A^\intercal = \begin{bmatrix}
a_{11} & a_{21} & \ldots & a_{n1} \\
a_{12} & a_{22} & \cdots & a_{n2} \\
\vdots & \vdots & \ddots & \vdots \\
a_{1n} & a_{2n} & \cdots & a_{nn} \\
\end{bmatrix}$.
Let $b_{r s} = a_{s r}$ for $1 \le r, s \le n$.
We need to show that $\map \det {\sqbrk a_n} = \map \det {\sqbrk b_n}$.
By the definition of determinant and Permutation of Determinant Indices, we have:
{{begin-eqn}}
{{eqn | l = \map \det {\sqbrk b_n}
      | r = \sum_\lambda \map {\sgn} \lambda b_{1 \map \lambda 1} b_{2 \map \lambda 2} \cdots b_{n \map \lambda n}
      | c = 
}}
{{eqn | r = \sum_\lambda \map {\sgn} \lambda a_{\map \lambda 1 1} a_{\map \lambda 2 2} \cdots a_{\map \lambda n n}
      | c = 
}}
{{eqn | r = \map \det {\sqbrk a_n}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Determinant with Rows Transposed

If two rows of a matrix with determinant $D$ are transposed, its determinant becomes $-D$.

Proof:
Let $\mathbf A = \sqbrk a_n$ be a square matrix of order $n$.
Let $1 \le r < s \le n$.
Let $e$ be the elementary row operation that exchanging rows $r$ and $s$.
Let $\mathbf B = \map e {\mathbf A}$.
Let $\mathbf E$ be the elementary row matrix corresponding to $e$.
From Elementary Row Operations as Matrix Multiplications:
:$\mathbf B = \mathbf E \mathbf A$
From Determinant of Elementary Row Matrix: Exchange Rows:
:$\map \det {\mathbf E} = -1$
Then:
{{begin-eqn}}
{{eqn | l = \map \det {\mathbf B}
      | r = \map \det {\mathbf E \mathbf A}
      | c = Determinant of Matrix Product
}}
{{eqn | r = -\map \det {\mathbf A}
      | c = as $\map \det {\mathbf E} = -1$
}}
{{end-eqn}}
Hence the result.
{{qed}}