avewright/proofwiki-math huggingface dataset:
Theorem: Pell's Equation/Examples/8

:$x^2 - 8 y^2 = 1$
has the positive integral solutions:
{{begin-eqn}}
{{eqn | l = \tuple {x, y}
      | r = \tuple {3, 1}
}}
{{eqn | l = \tuple {x, y}
      | r = \tuple {17, 6}
}}
{{eqn | l = \tuple {x, y}
      | r = \tuple {99, 35}
}}
{{eqn | l = \tuple {x, y}
      | r = \tuple {577, 204}
}}
{{eqn | l = \tuple {x, y}
      | r = \tuple {3363, 1189}
}}
{{end-eqn}}
and so on.

Proof:
From Continued Fraction Expansion of $\sqrt 8$:
:$\sqrt 8 = \sqbrk {2, \sequence {1, 4} }$
The cycle is of length $2$.
By Solution of Pell's Equation, the only solutions of $x^2 - 8 y^2 = 1$ are:
:${p_{2 r} }^2 - 8 {q_{2 r} }^2 = \paren {-1}^{2 r}$
for $r = 1, 2, 3, \ldots$
When $r = 1$ this gives:
:${p_2}^2 - 8 {q_2}^2 = 1$
which is the solution required.
From Convergents of Continued Fraction Expansion of $\sqrt 8$:
:$p_2 = 3$
:$q_2 = 1$
although on that page the numbering goes from $p_0$ to $p_9$, and $q_0$ to $q_9$.
{{qed}}
Category:Pell's Equation
Category:8
olzyyt27ls46mzypmozi1zsznlvcmyl
Theorem: Digital Root of Square

Let $n^2$ be a square number.
Then the digital root of $n^2$ is $1$, $4$, $7$ or $9$.

Proof:
Let $\map d n$ denote the digital root base $10$ of $n$.
From Digital Root is Congruent to Number Modulo Base minus 1, $\map d n \equiv n \pmod 9$.
So, let $n = 9 k + m$ where $1 \le m \le 9$.
Thus:
{{begin-eqn}}
{{eqn | l = n^2
      | r = \paren {9 k + m}^2
      | c = 
}}
{{eqn | r = 81 k^2 + 18 k m + m^2
      | c = 
}}
{{eqn | r = 9 \paren {9 k^2 + 2 k m} + m^2
      | c = 
}}
{{eqn | o = \equiv
      | r = m^2
      | rr= \pmod 9
      | c = 
}}
{{end-eqn}}
We enumerate the squares of the digits:
{{begin-eqn}}
{{eqn | l = 1^2
      | r = 1
      | c = 
}}
{{eqn | o = \equiv
      | r = 1
      | rr= \pmod 9
      | c = 
}}
{{eqn | l = 2^2
      | r = 4
      | c = 
}}
{{eqn | o = \equiv
      | r = 4
      | rr= \pmod 9
      | c = 
}}
{{eqn | l = 3^2
      | r = 9
      | c = 
}}
{{eqn | o = \equiv
      | r = 9
      | rr= \pmod 9
      | c = 
}}
{{eqn | l = 4^2
      | r = 16
      | c = 
}}
{{eqn | o = \equiv
      | r = 7
      | rr= \pmod 9
      | c = 
}}
{{eqn | l = 5^2
      | r = 25
      | c = 
}}
{{eqn | o = \equiv
      | r = 7
      | rr= \pmod 9
      | c = 
}}
{{eqn | l = 6^2
      | r = 36
      | c = 
}}
{{eqn | o = \equiv
      | r = 9
      | rr= \pmod 9
      | c = 
}}
{{eqn | l = 7^2
      | r = 49
      | c = 
}}
{{eqn | o = \equiv
      | r = 4
      | rr= \pmod 9
      | c = 
}}
{{eqn | l = 8^2
      | r = 64
      | c = 
}}
{{eqn | o = \equiv
      | r = 1
      | rr= \pmod 9
      | c = 
}}
{{eqn | l = 9^2
      | r = 81
      | c = 
}}
{{eqn | o = \equiv
      | r = 9
      | rr= \pmod 9
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Digital Roots
Category:Square Numbers
92wy9bkvf2ebhdsh114xsylqy6vj6uj
Theorem: Count of All Permutations on n Objects

Let $S$ be a set of $n$ objects.
Let $N$ be the number of permutations of $k$ objects from $S$, where $1 \le k \le N$.
Then:
:$\ds N = n! \sum_{k \mathop = 0}^{n - 1} \dfrac 1 {k!}$

Proof:
The number of permutations on $k$ objects, from $n$ is denoted ${}^n P_k$.
From Number of Permutations:
:${}^n P_k = \dfrac {n!} {\paren {n - k}!}$
Hence:
{{begin-eqn}}
{{eqn | q = 
      | l = N
      | r = \sum_{k \mathop = 1}^n {}^n P_k
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^n \dfrac {n!} {\paren {n - k}!}
      | c = 
}}
{{eqn | r = \dfrac {n!} {\paren {n - 1}!} + \dfrac {n!} {\paren {n - 2}!} + \cdots + \dfrac {n!} {\paren {n - \paren {n - 1} }!} + \dfrac {n!} {\paren {n - n}!}
      | c = 
}}
{{eqn | r = \dfrac {n!} {\paren {n - 1}!} + \dfrac {n!} {\paren {n - 2}!} + \cdots + \dfrac {n!} {1!} + \dfrac {n!} {0!}
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 0}^{n - 1} \dfrac {n!} {k!}
      | c = 
}}
{{eqn | r = n! \sum_{k \mathop = 0}^{n - 1} \dfrac 1 {k!}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Time when Hour Hand and Minute Hand at Right Angle

Let the time of day be such that the hour hand and minute hand are at a right angle to each other.
Then the time happens $22$ times in every $12$ hour period:
:when the minute hand is $15$ minutes ahead of the hour hand
:when the minute hand is $15$ minutes behind the hour hand.
In the first case, this happens at $09:00$ and every $1$ hour, $5$ minutes and $27 . \dot 2 \dot 7$ seconds after
In the second case, this happens at $03:00$ and every $1$ hour, $5$ minutes and $27 . \dot 2 \dot 7$ seconds after.
Thus the times are, to the nearest second:
$\begin {array}
09:00:00 & 03:00:00 \\ 
10:05:27 & 04:05:27 \\
11:10:55 & 05:10:55 \\
12:16:22 & 06:16:22 \\
13:21:49 & 07:21:49 \\
14:27:16 & 08:27:16 \\
15:32:44 & 09:32:44 \\
16:38:11 & 10:38:11 \\
17:43:38 & 11:43:38 \\
18:49:05 & 12:49:05 \\
19:54:33 & 13:54:33 \\
\end{array}$
and times $12$ hours different.

Proof:
Obviously the hands are at right angles at $3$ and $9$ o'clock.
Thus we only need to show that the angle between the hands will be the same after every $1$ hour, $5$ minutes and $27 . \dot 2 \dot 7$ seconds.
Note that:
{{begin-eqn}}
{{eqn | l = 1 h \ 5 m \ 27. \dot 2 \dot 7 s
      | r = 65 m \ 27 \tfrac {27}{99} s 
}}
{{eqn | r = 65 m \ 27 \tfrac 3 {11} s
}}
{{eqn | r = 65 m \ \frac {300} {11} s
}}
{{eqn | r = 65 m + \frac 5 {11} m
}}
{{eqn | r = \frac {720} {11} m
}}
{{eqn | r = \frac {12} {11} h
}}
{{end-eqn}}
In $\dfrac {12} {11}$ hours:
:The minute hand has rotated $\dfrac {12} {11} \times 360^\circ$
:The hour hand has rotated $\dfrac {12} {11} \times 30^\circ$
Thus the angle between the hands has changed by:
{{begin-eqn}}
{{eqn | l = \frac {12} {11} \times 360^\circ - \frac {12} {11} \times 30^\circ
      | r = \frac {12} {11} \times 330^\circ
}}
{{eqn | r = 360^\circ
}}
{{end-eqn}}
which is a full rotation.
Hence after $\dfrac {12} {11}$ hours the angle between the hands would remain unchanged.
{{qed}}
Category:Clocks
6yn9te301sh9ah9f621x6bh9pom8ll7
Theorem: Convergence in Normed Dual Space implies Weak-* Convergence

Let $\struct {X, \norm {\, \cdot \,}_X}$ be a normed vector space.
Let $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$ be the normed dual space of $\struct {X, \norm {\, \cdot \,}_X}$.
Let $\sequence {f_n}_{n \mathop \in \N}$ be a convergent sequence in $X^\ast$.
Then $\sequence {f_n}_{n \mathop \in \N}$ converges weakly-$\ast$.

Proof:
From Convergent Sequence in Normed Vector Space is Weakly Convergent, $\sequence {f_n}_{n \mathop \in \N}$ converges weakly.
From Weakly Convergent Sequence in Normed Dual Space is Weakly-* Convergent, $\sequence {f_n}_{n \mathop \in \N}$ converges weakly-$\ast$.
{{qed}}
Theorem: Convergence in Normed Dual Space implies Weak-* Convergence

Let $\struct {X, \norm {\, \cdot \,}_X}$ be a normed vector space.
Let $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$ be the normed dual space of $\struct {X, \norm {\, \cdot \,}_X}$.
Let $\sequence {f_n}_{n \mathop \in \N}$ be a convergent sequence in $X^\ast$.
Then $\sequence {f_n}_{n \mathop \in \N}$ converges weakly-$\ast$.

Proof:
Let $f \in X^\ast$ be the limit of $\sequence {f_n}_{n \mathop \in \N}$.
That is:
:$\norm {f_n - f}_{X^\ast} \stackrel {n \mathop \to \infty} \longrightarrow 0$
Thus, for each $x \in X$:
{{begin-eqn}}
{{eqn | l = \size {\map {f_n} x - \map f x}
      | r = \size {\map {\paren {f_n - f} } x}
      | c = {{Defof|Vector Space of Bounded Linear Functionals}}
}}
{{eqn | o = \le
      | r = \norm {f_n - f}_{X^\ast} \norm x_X
      | c = Fundamental Property of Norm on Bounded Linear Functional
}}
{{eqn | o = 
      | r = \stackrel {n \mathop \to \infty} \longrightarrow 0
}}
{{end-eqn}}
{{qed}}
Theorem: Weakly Convergent Sequence in Normed Dual Space is Weakly-* Convergent

Let $\mathbb F$ be a subfield of $\C$. 
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a normed vector space over $\mathbb F$.
Let $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$ be the normed dual space of $\struct {X, \norm {\, \cdot \,}_X}$.
Let $f \in X^\ast$. 
Let $\sequence {f_n}_{n \mathop \in \N}$ be a sequence in $X^\ast$ converging weakly to $f$. 
Then $\sequence {f_n}_{n \mathop \in \N}$ converges weakly-$\ast$ to $f$.

Proof:
Let $x \in X$.
We aim to show that: 
:$\map {f_n} x \to \map f x$
Then, since $x \in X$ was arbitrary, we will obtain that $\sequence {f_n}_{n \mathop \in \N}$ converges weakly-$\ast$ to $f$.
Since $\sequence {f_n}_{n \mathop \in \N}$ converges weakly to $f$, we have: 
:$\map F {f_n} \to \map F f$ for each $F \in \paren {X^\ast}^\ast$.
Define $x^\wedge : X^\ast \to \mathbb F$ by: 
:$\map {x^\wedge} f = \map f x$
for each $f \in X^\ast$.
From Evaluation Linear Transformation on Normed Vector Space is Linear Transformation from Space to Second Normed Dual, we have: 
:$x^\wedge \in \paren {X^\ast}^\ast$
So, setting $F = x^\wedge$, we obtain: 
:$\map {x^\wedge} {f_n} \to \map {x^\wedge} f$
That is: 
:$\map {f_n} x \to \map f x$
{{qed}}
Theorem: Weakly Convergent Sequence in Normed Dual Space is Weakly-* Convergent

Let $\mathbb F$ be a subfield of $\C$. 
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a normed vector space over $\mathbb F$.
Let $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$ be the normed dual space of $\struct {X, \norm {\, \cdot \,}_X}$.
Let $f \in X^\ast$. 
Let $\sequence {f_n}_{n \mathop \in \N}$ be a sequence in $X^\ast$ converging weakly to $f$. 
Then $\sequence {f_n}_{n \mathop \in \N}$ converges weakly-$\ast$ to $f$.

Proof:
Let $J$ be the evaluation linear transformation on $X$.
By Evaluation Linear Transformation on Normed Vector Space is Linear Transformation from Space to Second Normed Dual:
:$J : X \to X^{\ast \ast}$
Thus, for each $x \in X$:
{{begin-eqn}}
{{eqn | l = \map {f_n} x
      | r = \map {\map J x} {f_n}
}}
{{eqn | o =\stackrel {n \to \infty} {\longrightarrow}
      | r = \map {\map J x} f
}}
{{eqn | o =
      | ro = =
      | r = \map f x
}}
{{end-eqn}}
{{qed}}
Theorem: Weak Convergence in Normed Dual Space of Reflexive Normed Vector Space is Equivalent to Weak-* Convergence

Let $\mathbb F$ be a subfield of $\C$. 
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a reflexive normed vector space over $\mathbb F$.
Let $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$ be the normed dual space of $\struct {X, \norm {\, \cdot \,}_X}$.
Let $f \in X^\ast$. 
Then:
:$\sequence {f_n}_{n \mathop \in \N}$ converges weakly to $f$ {{iff}} $\sequence {f_n}_{n \mathop \in \N}$ converges weakly-$\ast$ to $f$.

Proof:
Let $J : X \to X^{**}$ be the evaluation linear transformation.
In view of {{Defof|Reflexive Space}}, $J$ is especially a surjection.
Therefore:
{{begin-eqn}}
{{eqn | l = f_n
      | o = \weakconv
      | r = f
}}
{{eqn | ll = \leadstoandfrom
      | q = \forall x' ' \in X^{**}
      | l = \map {x' '} {f_n}
      | o = \to
      | r = \map {x' '} f
      | c = {{Defof|Weak Convergence (Normed Vector Space)|Weak Convergence}}
}}
{{eqn | ll = \leadstoandfrom
      | q = \forall x \in X
      | l = \map {\map J x} {f_n}
      | o = \to
      | r = \map {\map J x} f
      | c = as $J : X \to X^{**}$ is a surjection
}}
{{eqn | ll = \leadstoandfrom
      | q = \forall x \in X
      | l = \map {f_n} x
      | o = \to
      | r = \map f x
      | c = {{Defof|Evaluation Linear Transformation on Normed Vector Space|$J$}}
}}
{{eqn | ll = \leadstoandfrom
      | l = f_n
      | o = \weakstarconv
      | r = f
      | c = {{Defof|Weak-* Convergence (Normed Vector Space)|Weak-* Convergence }}
}}
{{end-eqn}}
{{qed}}
Theorem: Power Structure Operation on Set of Singleton Subsets is Closed

Let $\struct {S, \circ}$ be a magma.
Let $\struct {\powerset S, \circ_\PP}$ be the power structure of $S$.
Let $S'$ denote the set of singleton elements of $\powerset S$.
Then the algebraic structure $\struct {S', \circ_\PP}$ is closed.

Proof:
{{Recall|Magma}}
{{:Definition:Magma}}
{{Recall|Singleton}}
{{:Definition:Singleton}}
Let $A, B \in S'$.
Then:
:$\exists a, b \in S: A = \set a, B = \set b$
Hence:
{{begin-eqn}}
{{eqn | l = A \circ_\PP B
      | r = \set {x \circ y: x \in A, y \in B}
      | c = {{Defof|Subset Product}}
}}
{{eqn | r = \set {a \circ b}
      | c = {{Defof|Magma}}
}}
{{eqn | o = \in
      | r = S'
      | c = Definition of $S'$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Operation is Isomorphic to Power Structure Operation on Set of Singleton Subsets

Let $\struct {S, \circ}$ be a magma.
Let $\struct {\powerset S, \circ_\PP}$ be the power structure of $\struct {S, \circ}$.
Let $S'$ denote the set of singleton elements of $\powerset S$.
Then $\struct {S, \circ}$ is isomorphic to $\struct {S', \circ_\PP}$.

Proof:
Let $\phi: S \to S'$ be the mapping defined as:
:$\forall x \in S: \map \phi x = \set x$
We have that:
{{begin-eqn}}
{{eqn | q = \forall a, b \in S
      | l = \map \phi a
      | r = \map \phi b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \set a
      | r = \set b
      | c = Definition of $\phi$
}}
{{eqn | ll= \leadsto
      | l = a
      | r = b
      | c = Singleton Equality
}}
{{end-eqn}}
demonstrating that $\phi$ is an injection.
Then we have:
{{begin-eqn}}
{{eqn | q = \forall A \in S': \exists a \in S
      | l = A
      | r = \set a
      | c = {{Defof|Singleton}}
}}
{{eqn | ll= \leadsto
      | l = A
      | r = \map \phi a
      | c = Definition of $\phi$
}}
{{end-eqn}}
demonstrating that $\phi$ is a surjection.
Hence by definition $\phi$ is a bijection.
By the definition of a magma, $S$ is closed under $\circ$.
That is:
:$\forall a, b \in S, a \circ b \in S$
Hence:
:$a \circ b \in \Dom \phi$
Also, by Power Structure of Magma is Magma, $S'$ is closed under $\circ_\PP$.
Hence:
:$\set a \circ_\PP \set b \in S'$
Now:
{{begin-eqn}}
{{eqn | q = \forall a, b \in S
      | l = \map \phi {a \circ b}
      | r = \set {a \circ b}
      | c = Definition of $\phi$
}}
{{eqn | r = \set a \circ_\PP \set b
      | c = {{Defof|Subset Product}}
}}
{{eqn | r = \map \phi a \circ_\PP \map \phi b
      | c = Definition of $\phi$
}}
{{end-eqn}}
That is, $\phi$ is a homomorphism.
So $\phi$ is a bijective homomorphism.
Hence the result by definition of isomorphism.
{{qed}}
Theorem: Power Structure Operation on Set of Singleton Subsets preserves Associativity

Let $\struct {S, \circ}$ be a magma.
Let $\struct {\powerset S, \circ_\PP}$ be the power structure of $\struct {S, \circ}$.
Let $S'$ denote the set of singleton elements of $\powerset S$.
Then $\circ_\PP$ is associative {{iff}} $\circ$ is associative.

Proof:
From Operation is Isomorphic to Power Structure Operation on Set of Singleton Subsets:
:$\struct {S, \circ}$ is isomorphic to $\struct {S', \circ_\PP}$
The result follows from Isomorphism Preserves Associativity.
{{qed}}
Theorem: Power Structure Operation on Set of Singleton Subsets preserves Commutativity

Let $\struct {S, \circ}$ be a magma.
Let $\struct {\powerset S, \circ_\PP}$ be the power structure of $\struct {S, \circ}$.
Let $S'$ denote the set of singleton elements of $\powerset S$.
Then $\circ_\PP$ is commutative {{iff}} $\circ$ is commutative.

Proof:
From Operation is Isomorphic to Power Structure Operation on Set of Singleton Subsets:
:$\struct {S, \circ}$ is isomorphic to $\struct {S', \circ_\PP}$
The result follows from Isomorphism Preserves Commutativity.
{{qed}}
Theorem: Identity Element for Power Structure

Let $\struct {S, \circ}$ be a magma whose underlying set $S$ is non-empty.
Let $\struct {\powerset S, \circ_\PP}$ be the power structure of $\struct {S, \circ}$.
Then:
:a subset $J$ of $S$ is an identity element of $\struct {\powerset S, \circ_\PP}$
{{iff}}:
:there exists an identity element $e$ of $\struct {S, \circ}$, such that $J = \set e$.

Proof:
=== Sufficient Condition ===
Let $J \subseteq S$ such that $J$ is an identity element of $\struct {\powerset S, \circ_\PP}$.
We have:
{{begin-eqn}}
{{eqn | q = \forall A \in \powerset S
      | l = J \circ_\PP A
      | r = A
      | c = {{Defof|Identity Element}}
}}
{{eqn | ll= \leadsto
      | l = \set {j \circ a: j \in J, a \in A}
      | r = A
      | c = {{Defof|Operation Induced on Power Set}}
}}
{{eqn | ll= \leadsto
      | q = \forall a \in A: \forall j \in J
      | l = j \circ a
      | r = a
      | c = 
}}
{{end-eqn}}
That is, the elements of $J$ are all left identities for $\circ$.
Similarly:
{{begin-eqn}}
{{eqn | q = \forall A \in \powerset S
      | l = A \circ_\PP J
      | r = A
      | c = {{Defof|Identity Element}}
}}
{{eqn | ll= \leadsto
      | l = \set {a \circ j: j \in J, a \in A}
      | r = A
      | c = {{Defof|Operation Induced on Power Set}}
}}
{{eqn | ll= \leadsto
      | q = \forall a \in A: \forall j \in J
      | l = a \circ j
      | r = a
      | c = 
}}
{{end-eqn}}
That is, the elements of $J$ are all right identities for $\circ$.
So we have established that $J$ contains at least one element which is both a left identity and a right identity.
From Left and Right Identity are the Same, there is only one element of $J$, and it is the necessarily unique identity element for $\circ$.
That is:
:there exists an identity element $e$ of $\struct {S, \circ}$, such that $J = \set e$.
{{qed|lemma}}
Theorem: Invertible Element containing Identity in Power Structure

Let $\struct {S, \circ}$ be a magma.
Let identity element $e \in S$ be an identity element of $\struct {S, \circ}$.
Let $\struct {\powerset S, \circ_\PP}$ be the power structure of $\struct {S, \circ}$.
Let $X \subseteq S$ such that:
:$e \in X$
:$X$ is invertible for $\circ_PP$.
Then $X = \set e$.

Proof:
Let $X \subseteq S$ be invertible for $\circ_PP$ and such that $e \in X$.
From Identity Element for Power Structure, $\struct {\powerset S, \circ_\PP}$ has an identity element $J = \set e$.
We have:
{{begin-eqn}}
{{eqn | n = 1
      | q = \exists Y \in \powerset S
      | l = X \circ_\PP Y
      | r = J
      | c = {{Defof|Invertible Element}}: here $Y$ is the inverse of $X$
}}
{{eqn | ll= \leadsto
      | l = \set {x \circ y: x \in X, y \in Y}
      | r = \set e
      | c = {{Defof|Operation Induced on Power Set}}, Definition of $J$
}}
{{eqn | ll= \leadsto
      | q = \forall y \in Y
      | l = e \circ y
      | r = e
      | c = applying the above to $e$ as an element of $X$
}}
{{eqn | ll= \leadsto
      | q = \forall y \in Y
      | l = y
      | r = e
      | c = {{Defof|Identity Element}}
}}
{{eqn | ll= \leadsto
      | l = Y
      | r = \set e
      | c = 
}}
{{eqn | ll= \leadsto
      | l = X \circ_\PP \set e
      | r = \set e
      | c = substituting for $Y$ and $J$ in $(1)$
}}
{{eqn | ll= \leadsto
      | q = \forall x \in X
      | l = x
      | r = e
      | c = {{Defof|Identity Element}}
}}
{{eqn | ll= \leadsto
      | l = X
      | r = \set e
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Condition for Invertibility in Power Structure on Associative or Cancellable Operation

Let $\struct {S, \circ}$ be a unital magma.
Let $\struct {\powerset S, \circ_\PP}$ denote the power structure of $\struct {S, \circ}$.
Let identity element $e \in S$ be an identity element of $\struct {S, \circ}$.
Let $\circ$ be either:
:an associative operation
:a cancellable operation.
Let $X \subseteq S$ be a subset of $S$.
Then:
:$X$ is invertible for $\circ_PP$
{{iff}}:
:there exists an element $x \in S$ which is invertible for $\circ$ such that $X = \set x$.

Proof:
First we note that from Identity Element for Power Structure, the algebraic structure $\struct {\powerset S, \circ_\PP}$ has an identity element $J = \set e$.
Theorem: Set of Finite Subsets under Induced Operation is Closed

Let $\struct {S, \circ}$ be a magma.
Let $\struct {\powerset S, \circ_\PP}$ be the power structure of $\struct {S, \circ}$
Let $T \subseteq \powerset S$ be the set of all finite subsets of $S$.
Then the algebraic structure $\struct {T, \circ_\PP}$ is closed.

Proof:
Let $X, Y \in T$.
Then:
{{begin-eqn}}
{{eqn | q = 
      | l = X \circ_\PP Y
      | r = \set {x \circ y: x \in X, y \in Y}
      | c = {{Defof|Operation Induced on Power Set}}
}}
{{eqn | ll= \leadsto
      | l = \card {X \circ_\PP Y}
      | o = \le
      | r = \card X \times \card Y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = X \circ_\PP Y
      | o = \in
      | r = T
      | c = 
}}
{{end-eqn}}
{{handwaving|Between step $1$ and step $2$ we really need a result Order of Subset Product is not Greater than Cardinality of Cartesian Product which is straightforward but tedious, and I lack patience.}}
{{qed}}
Theorem: Power Structure of Subset is Closed iff Subset is Closed

Let $\struct {S, \circ}$ be a magma.
Let $\circ_\PP$ be the operation induced on $\powerset S$, the power set of $S$.
Let $T \subseteq S$.
Then:
:the algebraic structure $\struct {\powerset T, \circ_\PP}$ is closed
{{iff}}:
:the algebraic structure $\struct {T, \circ}$ is closed.

Proof:
=== Sufficient Condition ===
Let $\struct {\powerset T, \circ_\PP}$ be closed.
Then:
{{begin-eqn}}
{{eqn | q = \forall X, Y \in \powerset T
      | l = X \circ_\PP Y
      | o = \in
      | r = \powerset T
      | c = {{Defof|Closed Algebraic Structure}}
}}
{{eqn | l = \set {x \circ y: x \in X, y \in Y}
      | o = \subseteq
      | r = T
      | c = {{Defof|Operation Induced on Power Set}}
}}
{{eqn | ll= \leadsto
      | q = \forall x \in X, y \in Y
      | l = x \circ y
      | o = \in
      | r = T
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
That is, $\struct {T, \circ}$ is closed.
{{qed|lemma}}
Theorem: Pell Number as Sum of Squares

Let $P_n$ be a Pell Number:
:$P_n = \begin{cases} 0 & : n = 0 \\  1 & : n = 1 \\  2 P_{n - 1} + P_{n - 2} & : \text {otherwise}\end{cases}$
Then:
:$P_{2 n + 1} = P_{n + 1}^2 + P_n^2$

Proof:
This proof proceeds by induction.
Theorem: Multiple of Repdigit Base minus 1/Generalization

Let $b \in \Z_{>1}$ be an integer greater than $1$.
Let $n$ be a repdigit number of $k$ instances of the digit $b - 1$ for some integer $k$ such that $k \ge 1$.
Let $m \in \N$ be an integer such that $1 \le m \le b^k$.
Then $m \times n$, when expressed in base $b$, is the concatenation of $m - 1$ with $b^k - m$, that is:
:$m n = \sqbrk {\paren {m - 1} \paren {b^k - m} }_b$
If $b^k - m$ has less than $k$ digits, leading zeros are added to it until it has $k$ digits.

Proof:
{{begin-eqn}}
{{eqn | l = n
      | r = \sum_{j \mathop = 0}^{k - 1} \paren {b - 1} b^j
      | c = Basis Representation Theorem
}}
{{eqn | r = b^k - 1
      | c = Sum of Geometric Sequence
}}
{{eqn | ll= \leadsto
      | l = m n
      | r = m \paren {b^k - 1}
      | c = 
}}
{{eqn | r = \paren {m - 1} b^k + b^k - m
      | c = 
}}
{{end-eqn}}
which is exactly the representation $\sqbrk {\paren {m - 1} \paren {b^k - m} }_b$ with leading zeroes for $b^k - m$, as defined.
{{qed}}
Theorem: Set of Subsemigroups of Commutative Semigroup form Subsemigroup of Power Structure

Let $\struct {S, \circ}$ be a commutative semigroup.
Let $\struct {\powerset S, \circ_\PP}$ denote the power structure of $\struct {S, \circ}$.
Let $\TT$ be the set of all subsemigroups of $S$.
Then $\struct {\TT, \circ_\PP}$ is a subsemigroup of $\struct {\powerset S, \circ_\PP}$.

Proof:
First we establish that from Power Structure of Semigroup is Semigroup:
:$\struct {\powerset S, \circ_\PP}$ is a semigroup.
From Subset Product within Commutative Structure is Commutative:
:$\struct {\powerset S, \circ_\PP}$ is a commutative semigroup.
Let $A$ and $B$ be arbitrary subsemigroups of $S$.
As $A$ and $B$ are subsemigroups of $S$, they themselves are closed for $\circ$.
That is:
:$\forall x, y \in A: x \circ y \in A$
and:
:$\forall x, y \in B: x \circ y \in B$
By definition of operation induced on $\powerset S$:
:$A \circ_\PP B = \set {a \circ b: a \in A, b \in B}$
We are to show that:
:$\forall x, y \in A \circ_\PP B: x \circ y \in A \circ_\PP B$
Let $x, y \in A \circ_\PP B$ such that $x = a_x \circ b_x$, $y = a_y \circ b_y$.
We have:
{{begin-eqn}}
{{eqn | l = x \circ y
      | r = \paren {a_x \circ b_x} \circ \paren {a_y \circ b_y}
      | c = 
}}
{{eqn | r = a_x \circ \paren {b_x \circ a_y} \circ b_y
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = a_x \circ \paren {a_y \circ b_x} \circ b_y
      | c = $\circ$ is commutative
}}
{{eqn | r = \paren {a_x \circ a_y} \circ \paren {b_x \circ b_y}
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | o = \in
      | r = A \circ_\PP B
      | c = {{Semigroup-axiom|0}}: both $A$ and $B$ are closed for $\circ$
}}
{{end-eqn}}
That is:
:$x, y \in A \circ_\PP B \implies x \circ y \in A \circ_\PP B$
and $A \circ_\PP B$ is seen to be $\struct {\TT, \circ_\PP}$.
Hence the result.
{{qed}}