avewright/proofwiki-math huggingface dataset:
Theorem: Tangent of Half Side for Spherical Triangles

:$\tan \dfrac a 2 = \sqrt {\dfrac {-\cos S \, \map \cos {S - A} } {\map \cos {S - B} \, \map \cos {S - C} } }$
where $S = \dfrac {a + b + c} 2$.

Proof:
{{begin-eqn}}
{{eqn | l = \tan \dfrac a 2
      | r = \dfrac {\sqrt {\dfrac {-\cos S \, \map \cos {S - A} } {\sin B \sin C} } } {\sqrt {\dfrac {\map \cos {S - B} \, \map \cos {S - C} } {\sin B \sin C} } }
      | c = Sine of Half Angle for Spherical Triangles, Cosine of Half Angle for Spherical Triangles
}}
{{eqn | r = \sqrt {\dfrac {-\cos S \, \map \cos {S - A} } {\map \cos {S - B} \, \map \cos {S - C} } }
      | c = simplification
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Zenith Distance is Complement of Celestial Altitude

Let $X$ be the position of a star (or other celestial body) on the celestial sphere.
The zenith distance $z$ of $X$ is the complement of the altitude $a$ of $X$:
:$z = 90 \degrees - a$

Proof:
The vertical circle through $X$ is defined as the great circle that passes through $Z$.
By definition, the angle of the arc from $Z$ to the horizon is a right angle.
Hence $z + a = 90 \degrees$.
The result follows.
{{qed}}
Theorem: P-adic Metric on P-adic Numbers is Non-Archimedean Metric/Corollary 1

Then:
:$\forall x, y, z \in R: \norm {x - y}_p \le \max \set {\norm {x - z}_p, \norm {y - z}_p}$

Proof:
Let $d_p$ be the $p$-adic metric on $\Q_p$:
:$\forall x, y \in \Q_p: \map {d_p} {x, y} = \norm {x - y}_p$
From P-adic Metric on P-adic Numbers is Non-Archimedean Metric, $d_p$ is a non-Archimedean norm.
By definition of a non-Archimedean norm:
:$\forall x, y, z \in R: \norm {x - y}_p \le \max \set {\norm {x - z}_p, \norm {y - z}_p}$
{{qed}}
Category:Normed Division Rings
Category:Non-Archimedean Norms
1e7q3jo9peculpq4312zmcnl4pkeh2g
Theorem: Zenith Distance of North Celestial Pole equals Colatitude of Observer

Let $O$ be an observer of the celestial sphere.
Let $P$ be the position of the north celestial pole with respect to $O$.
Let $z$ denote the zenith distance of $P$.
Let $\psi$ denote the (terrestrial) colatitude of $O$.
Then:
:$z = \psi$

Proof:
Let $Z$ denote the zenith.
The zenith distance $z$ of $P$ is by definition the length of the arc $PZ$ of the prime vertical.
This in turn is defined as the angle $\angle POZ$ subtended by $PZ$ at $O$.
This is equivalent to the angle between the radius of Earth through $O$ and Earth's axis.
This is by definition the (terrestrial) colatitude of $O$.
Hence the result.
{{qed}}
Theorem: Altitude of North Celestial Pole equals Latitude of Observer

Let $O$ be an observer of the celestial sphere.
Let $P$ be the position of the north celestial pole with respect to $O$.
Let $a$ denote the altitude of $P$.
Let $\phi$ denote the (terrestrial) latitude of $O$.
Then:
:$a = \phi$

Proof:
Let $z$ denote the zenith distance of $P$.
Let $\psi$ denote the (terrestrial) colatitude of $O$.
By definition we have:
:$a = 90 \degrees - z$
:$\phi - 90 \degrees - \psi$
Then:
{{begin-eqn}}
{{eqn | l = z
      | r = \psi
      | c = Zenith Distance of North Celestial Pole equals Colatitude of Observer
}}
{{eqn | ll= \leadsto
      | l = 90 \degrees - z
      | r = 90 \degrees - \psi
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a
      | r = \phi
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Celestial Equator is Parallel to Geographical Equator

Consider the celestial sphere with observer $O$.
The plane of the celestial equator is parallel to the plane of the geographical equator.

Proof:
Let $P$ denote the north celestial pole.
The celestial equator is by definition perpendicular to $OP$.
Also by definition, $OP$ is parallel to Earth's axis.
Also by definition, Earth's axis is perpendicular to the geographical equator.
Hence $OP$ is also perpendicular to the geographical equator.
The result follows from Planes Perpendicular to same Straight Line are Parallel.
{{qed}}
Theorem: Celestial Body moves along Parallel of Declination

Consider the celestial sphere $C$ whose observer is $O$.
Let $B$ be a celestial body on $C$.
Let $\delta$ be the declination of $B$.
Let $P_\delta$ be the parallel of declination whose declination is $\delta$.
Then $B$ appears to move along the path of $P_\delta$, in the direction from the north to east to south to west.
It takes $1$ sidereal day for $B$ to travel around $P_\delta$.

Proof:
The apparent movement of $C$ is caused by the rotation of Earth about its axis.
This rotation takes $1$ sidereal day, by definition, for the principal vertical circle to be in the same position again.
As the Earth rotates, the observer $O$ moves in an easterly direction.
Hence the celestial sphere $C$ appears to move in the opposite direction, so from north to east and so on.
$B$ remains at the same distance from the north celestial pole as it did.
Hence its declination $\delta$ stays the same.
Hence the result.
{{qed}}
Theorem: Closed Ball is Disjoint Union of Smaller Closed Balls in P-adic Numbers

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $a \in \Q_p$.
For all $\epsilon \in \R_{>0}$, let $\map { {B_\epsilon}^-} a$ denote the closed $\epsilon$-ball of $a$. 
Let $n, m \in Z$, such that $n < m$.
Then:
:$(1) \quad \map {B^-_{p^{-n} } } a = \ds \bigcup_{i \mathop = 0}^{p^{\paren {m - n} } - 1} \map {B^-_{p^{-m} } } {a + i p^n}$
:$(2) \quad \set {\map {B^-_{p^{-m} } } {a + i p^n} : i = 0, \dots, p^{\paren {m - n} } - 1}$ is a set of pairwise disjoint closed balls

Proof:
=== Condition $(1)$ ===
{{:Closed Ball is Disjoint Union of Smaller Closed Balls in P-adic Numbers/Union of Closed Balls}}{{qed|lemma}}
Theorem: Closed Ball is Disjoint Union of Smaller Closed Balls in P-adic Numbers/Union of Closed Balls

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $a \in \Q_p$.
For all $\epsilon \in \R_{>0}$, let $\map { {B_\epsilon}^-} a$ denote the closed $\epsilon$-ball of $a$. 
Let $n, m \in Z$, such that $n < m$.
Then:
:$\map {B^-_{p^{-n} } } a = \ds \bigcup_{i \mathop = 0}^{p^{\paren {m - n}} - 1} \map {B^-_{p^{-m} } } {a + i p^{\paren {m - n} } }$

Proof:
==== Lemma ====
{{:Closed Ball is Disjoint Union of Smaller Closed Balls in P-adic Numbers/Lemma 1}}{{qed|lemma}}
Let $0 \le i \le p^{\paren{m - n}} - 1$.
Let $x \in \map {B^{\,-}_{p^{-m} } } {a + i p^{-n} }$
By definition of a closed ball:
:$\norm {x - a - i p^{-n} } \le p^{-m}$
From Lemma:
:$\norm {x - a}_p \le p^{-n}$
By definition of a closed ball:
:$x \in \map {B^-_{p^{-n} } } a$
Since $x$ was arbitrary:
:$\map {B^-_{p^{-m} } } {a + i p^{-n} } \subseteq \map {B^-_{p^{-n} } } a$
Since $i$ was arbitrary: 
:$\ds \bigcup_{i \mathop = 0}^{p^{\paren {m - n}} - 1} \map {B^-_{p^{-m} } } {a + i p^{-n} } \subseteq \map {B^-_{p^{-n} } } a$
Let $x \in \map {B^-_{p^{-n} } } a$.
By definition of a closed ball:
:$\norm {x - a}_p \le p^{-n}$
From Lemma:
:$\exists i \in \N : 0 \le i \le p^{\paren {m - n}} - 1: \norm {x - a - i p^{-n} } \le p^{-m}$
By definition of a closed ball:
:$\exists i \in \N : 0 \le i \le p^{\paren {m - n}} - 1 : x \in \map {B^-_{p^{-m} } } {a + i p^{-n} }$
Hence:
:$\map {B^-_{p^{-n} } } a \subseteq \ds \bigcup_{i \mathop = 0}^{p^{\paren {m - n}} - 1} \map {B^-_{p^{-m} } } {a + i p^{-n} }$
It follows that:
:$\map {B^-_{p^{-n} } } a = \ds \bigcup_{i \mathop = 0}^{p^{\paren {m - n}} - 1} \map {B^-_{p^{-m} } } {a + i p^{-n} }$
Theorem: Closed Ball is Disjoint Union of Smaller Closed Balls in P-adic Numbers/Disjoint Closed Balls

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $a \in \Q_p$.
For all $\epsilon \in \R_{>0}$, let $\map {B_\epsilon} a$ denote the open $\epsilon$-ball of $a$. 
Then:
:$\forall n \in Z : \set{\map {B^-_{p^{-m} } } {a + i p^n} : i = 0, \dotsc, p^{\paren {m - n}} - 1}$ is a set of pairwise disjoint open balls.

Proof:
Let $0 \le i, j \le p^{\paren {m - n}} - 1$.
Let $x \in \map {B^-_{p^{-m} } } {a + i p^n} \cap \map {B^-_{p^{-m} } } {a + j p^n}$
From Characterization of Open Ball in $p$-adic Numbers:
:$\norm {\paren {x -a} - i p^n}_p \le p^{-m}$
and:
:$\norm {\paren {x -a} - j p^n}_p \le p^{-m}$
We have that $p$-adic Norm satisfies Non-Archimedean Norm Axioms.
Then:
{{begin-eqn}}
{{eqn | l = \norm {i p^n - j p^n}_p
      | o = \le
      | r = p^{-m}
      | c = {{Corollary|P-adic Metric on P-adic Numbers is Non-Archimedean Metric| 1|disp = $p$-adic Metric on $p$-adic Numbers is Non-Archimedean Metric}}
}}
{{eqn | ll= \leadsto
      | l = \norm {p^n}_p \norm {i - j}_p
      | o = \le
      | r = p^{-m}
      | c = {{NormAxiomNonArch|2}}
}}
{{eqn | ll= \leadsto
      | l = p^{-n} \norm {i - j}_p
      | o = \le
      | r = p^{-m}
      | c = {{Defof|P-adic Norm|$p$-adic norm}}
}}
{{eqn | ll= \leadsto
      | l = \norm {i - j}_p
      | o = \le
      | r = p^{n - m}
      | c = multiplying both sides by $p^n$.
}}
{{eqn | ll= \leadsto
      | l = p^{\paren {m - n} }
      | o = \divides
      | r = \paren {i - j}
      | c = {{Defof|P-adic Norm|$p$-adic norm}}
}}
{{eqn | ll= \leadsto
      | l = j
      | o = \equiv
      | r = i
      | rr= \pmod {p^{m - n} }
      | c = {{Defof|Congruence Modulo Integer|Congruence Modulo $p$}}
}}
{{eqn | ll= \leadsto
      | l = i
      | r = j 
      | c = Integer is Congruent to Integer less than Modulus
}}
{{eqn | ll= \leadsto
      | l = \map {B^-_{p^{-m} } } {a + i p^n}
      | r = \map {B^-_{p^{-m} } } {a + j p^n} 
      | c =
}}
{{end-eqn}}
The result follows.
Theorem: Closed Ball is Disjoint Union of Smaller Closed Balls in P-adic Numbers/Lemma 1

:$\forall y \in \Q_p: \norm y_p \le p^{-n}$ {{iff}} there exists $i \in \Z$ such that:
::$(1)\quad 0 \le i \le p^{\paren {m - n}} - 1$
::$(2)\quad \norm {y - i p^n}_p \le p^{-m}$

Proof:
=== Necessary Condition ===
Let $y \in \Q_p$.
Let $\norm y_p \le p^{-n}$.
{{:Closed Ball is Disjoint Union of Smaller Closed Balls in P-adic Numbers/Lemma 1/Necessary Condition}}{{qed|lemma}}
Theorem: Closed Ball is Disjoint Union of Smaller Closed Balls in P-adic Numbers/Lemma 1/Necessary Condition

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $n, m \in Z$, such that $n < m$.
Let $y \in \Q_p$.
Let $\norm{y}_p \le p^{-n}$.
Then there exists $i \in \Z$ such that:
{{begin-itemize}}
{{item|(1):|$0 \le i \le p^\paren {m - n} - 1$}}
{{item|(2):|$\norm {y - i p^n}_p \le p^{-m}$}}
{{end-itemize}}

Proof:
We have that $p$-adic Norm satisfies Non-Archimedean Norm Axioms.
Hence:
{{begin-eqn}}
{{eqn | l = \norm y_p  
      | o = \le
      | r = p^{-n}
}}
{{eqn | ll= \leadsto
      | l = p^n \norm{y}_p 
      | o = \le
      | r = 1
      | c = multiplying both sides by $p^n$
}}
{{eqn | ll= \leadsto
      | l = \norm{p^{-n} }_p \norm{y}_p
      | o = \le
      | r = 1
      | c = {{Defof|P-adic Norm|$p$-adic norm}}
}}
{{eqn | ll= \leadsto
      | l = \norm{p^{-n} y}_p
      | o = \le
      | r = 1
      | c = {{NormAxiomNonArch|2}}
}}
{{eqn | ll= \leadsto
      | l = \map {B_1^-} {p^{-n}y}
      | r = \map {B_1^-} 0
      | c = Characterization of Closed Ball in $p$-adic Numbers
}}
{{end-eqn}}
From Integers are Dense in Unit Ball of $p$-adic Numbers:
:$\exists \mathop k \in \Z : \norm{p^{-n} y - k}_p \le p^\paren {n - m}$
From Residue Classes form Partition of Integers:
:$\exists \mathop 0 \le i \le p^\paren {m - n} - 1: p^\paren {m - n} \divides k - i$
By definition of the $p$-adic norm:
:$\norm {k - i}_p  \le p^\paren {n - m}$
It follows that:
{{begin-eqn}}
{{eqn | l = \norm {p^{-n} y - i}_p
      | o = \le 
      | r = \max \set {\norm {p^{-n} y - k}_p, \norm {i - k}_p}
      | c = {{Corollary|P-adic Metric on P-adic Numbers is Non-Archimedean Metric|1|disp = $p$-adic Metric on $p$-adic Numbers is Non-Archimedean Metric}}
}}
{{eqn | o = \le
      | r = p^\paren {n - m}
      | c = 
}}
{{eqn | ll= \leadsto 
      | l = \norm {p^{-n} }_p \norm {y - i p^n}_p 
      | o = \le
      | r = p^\paren {n - m}
      | c = {{NormAxiomNonArch|2}}
}}
{{eqn | ll= \leadsto 
      | l = p^n \norm {y - i p^n}_p
      | o = \le 
      | r = p^\paren {n - m}
      | c = {{Defof|P-adic Norm|$p$-adic norm}}
}}
{{eqn | ll= \leadsto 
      | l = \norm {y - i p^n}_p
      | o = \le
      | r = p^{-m}
      | c = dividing both sides by $p^{-n}$
}}
{{end-eqn}}
Theorem: Closed Ball is Disjoint Union of Smaller Closed Balls in P-adic Numbers/Lemma 1/Sufficient Condition

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $y \in \Q_p$
Let $n, m \in Z$, such that $n < m$.
Let there exist $i \in \Z$:
:$(1): \quad 0 \le i \le p^\paren {m - n} - 1$
:$(2): \quad \norm {y - i p^n}_p \le p^{-m}$
Then:
:$\norm y_p \le p^{-n}$

Proof:
We have that P-adic Norm satisfies Non-Archimedean Norm Axioms:.
Hence:
{{begin-eqn}}
{{eqn | l = \norm y_p
      | r = \norm {y - i p^n + i p^n}_p
}}
{{eqn | o = \le
      | r = \max \set {\norm {y - i p^n}_p, \norm {i p^n}_p}
      | c = {{NormAxiomNonArch|4}}
}}
{{end-eqn}}
By assumption:
:$\norm {y - i p^n} \le p^{-m} \le p^{-n}$
and:
{{begin-eqn}}
{{eqn | l = \norm {i p^n}_p
      | r = \norm i_p \norm {p^n}_p
      | c = {{NormAxiomNonArch|2}}
}}
{{eqn | o = \le
      | r = 1 \cdot p^{-n}
      | c = As $i \in \Z \subseteq \Z_p$
}}
{{eqn | r = p^{-n}
}}
{{end-eqn}}
Hence:
:$\max \set {\norm {y - i p^n}_p, \norm {i p^n}_p} \le p^{-n}$
So:
:$\norm y_p \le p^{-n}$
Theorem: Open and Closed Balls in P-adic Numbers are Totally Bounded

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $a \in \Q_p$.
Let $n \in \Z$.
Then the open ball $\map {B_{p^{-n} } } a$ and closed ball $\map {B^-_{p^{-n} } } a$ are totally bounded subspaces.

Proof:
We begin by proving the theorem for the closed ball $\map {B^-_{p^{-n} } } a$.
From Open Ball in P-adic Numbers is Closed Ball then the theorem will be proved.
Let $d$ denote the subspace metric induced by the norm $\norm {\,\cdot\,}_p$ on $\map {B^-_{p^{-n} } } a$.
That is, $d: \map {B^-_{p^{-n} } } a \times \map {B^-_{p^{-n} } } a \to \R_{>0}$ is the metric defined by:
::$\forall x, y \in \map {B^-_{p^{-n} } } a: \map d {x, y} = \norm {x - y}_p$
By the definition of totally bounded it needs to be shown that:
:for every $\epsilon \in \R_{>0}$ there exist finitely many points $x_0, \dots, x_k \in \map {B^-_{p^{-n} } } a$ such that:
::$\ds \inf_{0 \mathop \le i \mathop \le k} \norm {x_i - x}_p \le \epsilon$
:for all $x \in \map {B^-_{p^{-n} } } a$. 
From Sequence of Powers of Reciprocals is Null Sequence:
:$\exists N \in \N: \forall k > N: p^{-k} \le \epsilon$.
Let $m = \max \set {n + 1, N}$.
Then $m > n$.
From Closed Ball is Disjoint Union of Smaller Closed Balls in P-adic Numbers:
:$\map {B^-_{p^{-n} } } a = \ds \bigcup_{i \mathop = 0}^{p^{\paren {m - n} } - 1} \map {B^-_{p^{-m} } } {a + i p^n}$
Let $x \in \map {B^-_{p^{-n} } } a$.
Let $k = p^{\paren {m - n} } - 1$.
Then there exists $0 \le j \le k$ such that:
:$x \in \map {B^-_{p^{-m} } } {a + j p^n}$
That is:
:$\norm {x - a + j p^n}_p \le p^{-m} \le \epsilon$
Hence:
:$\ds \inf_{0 \mathop \le i \mathop \le k} \norm {a + i p^n - x}_p \le \norm {x - a + j p^n}_p \le \epsilon$
Since $x \in \map {B^-_{p^{-n} } } a$ was arbitrary, then: 
:$\forall x \in \map {B^-_{p^{-n} } } a : \ds \inf_{0 \mathop \le i \mathop \le k} \norm {a + i p^n - x}_p \le \epsilon$
The result follows.
{{qed}}
Theorem: Cofactor Sum Identity

Let $J_n$ be the $n \times n$ matrix of all ones.
Let $A$ be a square matrix of order $n$.
Let $A_{ij}$ denote the cofactor of element $\tuple {i, j}$ in $\map \det A$, $1 \le i, j \le n$.
Then:
:$\ds \map \det {A - J_n} = \map \det A - \sum_{i \mathop  = 1}^n \sum_{j \mathop = 1}^n A_{i j} $

Proof:
Let $P_j$ equal matrix $A$ with column $j$ replaced by ones, $1\le j \le n$.
Then by the Laplace Expansion Theorem for Determinants applied to column $j$ of $P_j$:
:$\ds \sum_{j \mathop = 1}^n \map \det {P_j} = \sum_{j \mathop = 1}^n \sum_{i \mathop = 1}^n A_{ij}$
To complete the proof, it suffices to prove the equivalent identity:
:$\ds \map \det {A - J_n} = \map \det A - \sum_{j \mathop = 1}^n \map \det {P_j}$
Expansion of {{LHS}} $\map \det {A - J_n}$ for the $2 \times 2$ case illustrates how determinant theorems will be used:
{{begin-eqn}}
{{eqn | l = A
      | r = \begin {pmatrix} a & b \\ c & d \end {pmatrix}
      | c = where $A$ is an arbitrary $2 \times 2$ matrix
}}
{{eqn | l = J_2
      | r = \begin {pmatrix} 1 & 1 \\ 1 & 1 \end {pmatrix}
      | c = $J_2$ is the $2 \times 2$ ones matrix
}}
{{eqn | l = \map \det {A -J_2}
      | r = \map \det {\begin {matrix} a - 1 & b - 1 \\ c - 1 & d - 1 \end {matrix} }
      | c = Matrix Addition and Negative Matrix
}}
{{eqn | r = \map \det {\begin {matrix} a & b - 1 \\ c & d - 1 \end {matrix} } - \map \det {\begin {matrix} 1 & b - 1 \\ 1 & d - 1 \end {matrix} }
      | c = Determinant as Sum of Determinants
}}
{{eqn | r = \map \det {\begin {matrix} a & b - 1 \\ c & d - 1 \end {matrix} } - \map \det {\begin {matrix} 1 & b \\ 1 & d \end {matrix} }
      | c = Multiple of Row Added to Row of Determinant
}}
{{eqn | r = \map \det {\begin {matrix} a & b \\ c & d \end {matrix} } - \map \det {\begin {matrix} a & 1 \\ c & 1 \end {matrix} } - \map \det {\begin {matrix} 1 & b \\ 1 & d \end {matrix} }
      | c = Determinant as Sum of Determinants
}}
{{eqn | r = \map \det A - \map \det {P_2} - \map \det {P_1}
      | c = Definition of $P_1$ and $P_2$
}}
{{eqn | r = \map \det A - \sum_{j \mathop = 1}^2 \map \det {P_j}
      | c = equivalent identity verified for $n = 2$
}}
{{end-eqn}}
Let $A$ be a square matrix of order $n$
Let matrix $Q_m$ equal ones matrix $J_n$ with zeros replacing all entries in columns $1$ to $m$. 
For example, for $n = 5$ and $m = 2$:
:<nowiki>$Q_2 = \begin {pmatrix}
0 & 0 & 1 & 1 & 1 \\
0 & 0 & 1 & 1 & 1 \\
0 & 0 & 1 & 1 & 1 \\
0 & 0 & 1 & 1 & 1 \\
0 & 0 & 1 & 1 & 1 \\
\end {pmatrix}$</nowiki>
Induction on $m$ will be applied to prove the '''induction identity''':
:$\ds \map \det {A - J_n} = \map \det {A - Q_m} - \sum_{j \mathop = 1}^m \map \det {P_j}$
for $1 \le m \le n$.
Theorem: Sum of Elements of Nonsingular Matrix

Let $\mathbf J_n$ be the $n \times n$ square ones matrix.
Let $\mathbf B$ be an $n \times n$ nonsingular matrix with entries $b_{i j}$, $1 \le i, j \le n$.
Then:
:$\ds \sum_{i \mathop = 1}^n \sum_{j \mathop = 1}^n b_{i j} = 1 -  \map \det {\mathbf B} \map \det {\mathbf B^{-1} - \mathbf J_n}$

Proof:
=== Lemma ===
Let$\mathbf J_n$ be the $n \times n$ square ones matrix.
Let $\mathbf A$ be an $n \times n$ matrix.
Let $\mathbf A_{ij}$ denote the cofactor of element $a_{ij}$ in $\map \det {\mathbf A}$, $1 \le i, j \le n$.
Then:
{{begin-eqn}}
{{eqn | l = \map \det {\mathbf A - \mathbf J_n}
      | r = \map \det {\mathbf A} - \sum_{i \mathop = 1}^n \sum_{j \mathop = 1}^n \mathbf A_{i j}
      | c = Cofactor Sum Identity
}}
{{end-eqn}}
{{qed|lemma}}
Let $\mathbf A = \mathbf B^{-1}$.
Then:
{{begin-eqn}}
{{eqn | l = \mathbf A \mathbf B
      | r = \mathbf I
      | c = {{Defof|Nonsingular Matrix}}
}}
{{eqn | l = \mathbf B 
      | r = \dfrac {\adj {\mathbf A} } {\map \det {\mathbf A} }
      | c = Matrix Product with Adjugate Matrix with $\mathbf B = \mathbf A^{-1}$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 1}^n \sum_{j \mathop = 1}^n b_{ij}
      | r = \dfrac 1 {\map \det {\mathbf A} } \sum_{i \mathop = 1}^n \sum_{j \mathop = 1}^n \mathbf A_{ij}
}}
{{eqn | r = \map \det {\mathbf B} \sum_{i \mathop = 1}^n \sum_{j \mathop = 1}^n \mathbf A_{ij}
      | c = Determinant of Matrix Product and $A B = I$
}}
{{eqn | r = \map \det {\mathbf B} \paren {\map \det {\mathbf A} - \map \det {\mathbf A - \mathbf J_n} }
      | c = Apply the '''Lemma'''
}}
{{eqn | r = \map \det {\mathbf B} \map \det {\mathbf A} - \map \det {\mathbf B} \map \det {\mathbf B^{-1} - \mathbf J_n}
      | c = Definition $A = B^{-1}$
}}
{{eqn | r = 1 - \map \det {\mathbf B} \map \det {\mathbf B^{-1} - \mathbf J_n}
      | c = Determinant of Matrix Product and $\mathbf B \mathbf A = \mathbf I$
}}
{{end-eqn}}
{{qed}}
Category:Nonsingular Matrices
3vy0tqt6oc7pmaduzx9cf62dlk7xnrv
Theorem: Open and Closed Balls in P-adic Numbers are Clopen in P-adic Metric

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $a \in \Q_p$.
Let $n \in \Z$.
Then the open ball $\map {B_{p^{-n}}} a$ and closed ball $\map {B^-_{p^{-n}}} a$ are clopen in the $p$-adic metric.

Proof:
We begin by proving the theorem for the closed ball $\map {B^-_{p^{-n}}} a$.
From Open Ball in P-adic Numbers is Closed Ball then the theorem will be proved.
From P-adic Numbers form Non-Archimedean Valued Field::
:$\norm {\,\cdot\,}_p$ is a non-Archimedean division ring norm.
By definition the $p$-adic closed ball:
:$\map {B^-_{p^{-n} } } a$ is a closed ball in a normed division ring.  
From Closed Ball of Non-Archimedean Division Ring is Clopen:
:$\map {B^-_{p^{-n} } } a$ is clopen in the $p$-adic metric.
The result follows.
{{qed}}
Theorem: Closed Balls Centered on P-adic Number is Countable

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $a \in \Q_p$.
Then the set of all closed balls centered on $a$ is the countable set:
:$\BB^- = \set {\map {B^-_{p^{-n} } } a: n \in \Z}$

Proof:
Let $\epsilon \in \R_{>0}$.
Theorem: Closed Balls Centered on P-adic Number is Countable/Open Balls

Then the set of all open balls centered on $a$ is the countable set:
:$\BB = \set {\map {B_{p^{-n} } } a : n \in \Z}$

Proof:
Let $\epsilon \in \R_{\ge 0}$.
Theorem: Closed Balls Centered on P-adic Number is Countable/Lemma

:$\exists n \in \Z : p^{-n} \le \epsilon < p^{-\paren {n - 1} }$

Proof:
From Sequence of Powers of Reciprocals is Null Sequence:
:$\exists n_1 \in \N: \forall k \ge n_1 : p^{-k} < \epsilon$
Similarly:
:$\exists n_2 \in \N: \forall k \ge n_2 : p^{-k} < \dfrac 1 \epsilon$
Hence: 
:$p^{-n_1} < \epsilon$ and $ p^{-n_2} < \dfrac 1 \epsilon$
That is:
:$p^{-n_1} < \epsilon < p^{n_2}$
From Power Function on Integer between Zero and One is Strictly Decreasing:
:$-n_2 < n_1$.
Let:
:$n = \min \set {k : -n_2 \mathop \le k \mathop \le n_1 \text{ and } p^{-k} \le \epsilon}$
By choice of $n$:
:$p^{-n} \le \epsilon < p^{n_2}$
From Power Function on Integer between Zero and One is Strictly Decreasing:
:$n > -n_2$
Also by the choice of $n$:
:$n \le n_1$
So:
:$n_1 > n - 1 \ge -n_2$
{{AimForCont}}:
:$p^{-\paren {n - 1} } \le \epsilon$
Then:
:$n - 1 \in \set {k: -n_2 \le k \le n_1 \text{ and } p^{-k} \le \epsilon}$
So:
:$n = \min \set {k: -n_2 \le k \le n_1 \text { and } p^{-k} \le \epsilon} \le n - 1$
which is a contradiction.
Hence:
:$\epsilon < p^{-\paren {n - 1} }$
The result follows.
{{qed}}
Category:Closed Balls Centered on P-adic Number is Countable
fvc5hobq613kwnxyja592u2yufpzmhy
Theorem: Closed Balls Centered on P-adic Number is Countable/Open Balls/Lemma

:$\exists n \in \Z : p^{-\paren {n + 1} } < \epsilon \le p^{-n}$

Proof:
From Lemma for Closed Balls:
:$\exists m \in \Z : p^{-m} \le \epsilon < p^{-\paren {m - 1} }$
Suppose $\epsilon \ne p^{-m}$.
Then:
:$p^{-m} < \epsilon < p^{-\paren {m - 1} }$
and the theorem is proved with $n = m - 1$.
Now suppose $\epsilon = p^{-m}$.
From Power Function on Integer between Zero and One is Strictly Decreasing:
:$p^{-\paren{m + 1}} < p^{-m}$
So:
:$p^{-\paren{m + 1}} < \epsilon \le p^{-m}$
and the theorem is proved with $n = m$.
{{qed}}
Category:Closed Balls Centered on P-adic Number is Countable
5fwt3hebucebf4emyo7z8a55wobq4wq
Theorem: Open Ball contains Smaller Open Ball

Let $M = \struct{A, d}$ be a metric space.
Let $a \in A$.
Let $\epsilon, \delta \in \R_{>0}$ such that $\epsilon \le \delta$.
Let $\map {B_\epsilon} a$ be the open $\epsilon$-ball on $a$.
Let $\map {B_\delta} a$ be the open $\delta$-ball on $a$.
Then:
:$\map {B_\epsilon} a \subseteq \map {B_\delta} a$

Proof:
{{begin-eqn}}
{{eqn | l = x \in \map {B_\epsilon} a 
      | o = \leadstoandfrom
      | r = \map d {x, a} < \epsilon
      | c = {{Defof|Open Ball of Metric Space}}
}}
{{eqn | o = \leadsto
      | r = \map d {x, a} < \delta
      | c = As $\epsilon \le \delta$
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \map {B_\delta} a 
      | c = {{Defof|Open Ball of Metric Space}}
}}
{{end-eqn}}
By definition of subset:
:$\map {B_\epsilon} a \subseteq \map {B_\delta} a$
{{qed}}
Category:Open Balls
tb2kiexofbsr1wwepb0maidrucoez76