avewright/proofwiki-math huggingface dataset:
Theorem: Sum of Terms of Magic Square

The total of all the entries in a magic square of order $n$ is given by:
:$T_n = \dfrac {n^2 \paren {n^2 + 1} } 2$

Proof:
Let $M_n$ denote a magic square of order $n$.
$M_n$ is by definition a square matrix of order $n$ containing the positive integers from $1$ upwards.
Thus there are $n^2$ entries in $M_n$, going from $1$ to $n^2$.
Thus:
{{begin-eqn}}
{{eqn | l = T_n
      | r = \sum_{k \mathop = 1}^{n^2} k
      | c = 
}}
{{eqn | r = \frac {n^2 \paren {n^2 + 1} } 2
      | c = Closed Form for Triangular Numbers
}}
{{end-eqn}}
{{qed}}
Theorem: Schanuel's Conjecture Implies Transcendence of 2 to the power of Euler's Number

Let Schanuel's Conjecture be true.
Then $2$ to the power of Euler's number $e$:
:$2^e$
is transcendental, where $e$ is Euler's number.

Proof:
Assume the truth of Schanuel's Conjecture.
Let $z_1 = \ln \ln 2$, $z_2 = 1 + \ln \ln 2$, $z_3 = \ln 2$, and $z_4 = e \ln 2$.
By Lemma, they are linearly independent over the rational numbers $\Q$.
Observe that $z_3 = e^{z_1}$ and $z_4 = e^{z_2}$.
By Schanuel's Conjecture, the extension field $\map \Q {z_1, z_2, z_3, z_4, e^{z_1}, e^{z_2}, e^{z_3}, e^{z_4} }$ has transcendence degree at least $4$ over the rational numbers $\Q$.
That is, the extension field $\map \Q {\ln \ln 2, 1 + \ln \ln 2, \ln 2, e \ln 2, \ln 2, e \ln 2, 2, 2^e}$ has transcendence degree at least $4$ over $\Q$.
However, $2$ is algebraic.
Also, $\ln \ln 2$ and $1 + \ln \ln 2$ are not algebraically independent over $\Q$.
Therefore, $\ln \ln 2$, $\ln 2$, $e \ln 2$, and $2^e$ must all be transcendental.
Therefore, if Schanuel's Conjecture holds, then $2^e$ is transcendental.
{{qed}}
Category:Transcendental Numbers
Category:2
Category:Euler's Number
Category:Schanuel's Conjecture
p4yeslr5n0d1ccazm9ubdxffvot025o
Theorem: Schanuel's Conjecture Implies Transcendence of Pi to the power of Euler's Number

Let Schanuel's Conjecture be true.
Then $\pi$(pi) to the power of Euler's number $e$:
:$\pi^e$
is transcendental.

Proof:
Assume the truth of Schanuel's Conjecture.
Let $z_1 = \ln \ln \pi$, $z_2 = 1 + \ln \ln \pi$, $z_3 = \ln \pi$, $z_4 = e \ln \pi$, and $z_5 = i \pi$.
By Lemma, they are linearly independent over the rational numbers $\Q$.
Observe that $z_3 = e^{z_1}$ and $z_4 = e^{z_2}$.
By Schanuel's Conjecture, the extension field $\Q \left({z_1, z_2, z_3, z_4, z_5, e^{z_1}, e^{z_2}, e^{z_3}, e^{z_4}, e^{z_5}}\right)$ has transcendence degree at least $5$ over the rational numbers $\Q$.
That is, the extension field $\Q \left({\ln \ln \pi, 1 + \ln \ln \pi, \ln \pi, e \ln \pi, i \pi, \ln \pi, e \ln \pi, \pi, \pi^e, e^{i \pi}}\right)$ has transcendence degree at least $5$ over $\Q$.
However, by Euler's Identity, $e^{i \pi} = -1$ is algebraic.
Also, $\ln \ln \pi$ and $1 + \ln \ln \pi$ are not algebraically independent over $\Q$.
Also, $\pi$ and $i \pi$ are not algebraically independent over $\Q$.
Therefore, $\ln \ln \pi$, $\ln \pi$, $e \ln \pi$, $\pi$, and $\pi^e$ must all be transcendental.
Therefore, if Schanuel's Conjecture holds, then $\pi^e$ is transcendental.
{{qed}}
Category:Transcendental Numbers
Category:Pi
Category:Euler's Number
Category:Schanuel's Conjecture
kn6giozv3jtiyvbe6njft4bf8fpiznk
Theorem: Schanuel's Conjecture Implies Transcendence of Euler's Number to the power of Euler's Number

Let Schanuel's Conjecture be true.
Then Euler's number $e$ to the power of itself:
:$e^e$
is transcendental.

Proof:
Assume the truth of Schanuel's Conjecture.
Let $z_1 = 1$, $z_2 = e$.
By Euler's Number is Irrational, $z_1$ and $z_2$ are linearly independent over $\Q$.
By Schanuel's Conjecture, the extension field $\Q \left({z_1, z_2, e^{z_1}, e^{z_2}}\right)$ has transcendence degree at least $2$ over $\Q$.
That is, the extension field $\Q \left({1, e, e, e^e}\right)$ has transcendence degree at least $2$ over $\Q$.
However, $1$ is algebraic.
Therefore, if Schanuel's Conjecture holds, $e^e$ must be transcendental.
{{qed}}
Category:Transcendental Numbers
Category:Euler's Number
Category:Schanuel's Conjecture
o4jst2u7k117zspwek0wwym8z4aolfw
Theorem: Magic Constant of Magic Square

The magic constant of a magic square of order $n$ is given by:
:$S_n = \dfrac {n \paren {n^2 + 1} } 2$

Proof:
Let $M_n$ denote a magic square of order $n$.
By Sum of Terms of Magic Square, the total of all the entries in a magic square of order $n$ is given by:
:$T_n = \dfrac {n^2 \paren {n^2 + 1} } 2$
There are $n$ rows in $M_n$, each one with the same magic constant.
Thus the magic constant $S_n$ of the magic square $M_n$ is given by:
{{begin-eqn}}
{{eqn | l = S_n
      | r = \dfrac {T_n} n
      | c = 
}}
{{eqn | r = \dfrac {n^2 \paren {n^2 + 1} } {2 n}
      | c = Sum of Terms of Magic Square
}}
{{eqn | r = \dfrac {n \paren {n^2 + 1} } 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Magic Square of Order 3 is Unique

Up to rotations and reflections, the magic square of order $3$ is unique:
{{:Magic Square/Examples/Order 3}}

Proof:
Let $M_3$ denote the magic square of order $3$.
Each row, column and diagonal of $M_3$ must be a different set of $3$ elements of $\N_9$, where $\N_9$ denotes the set $\set {1, 2, 3, 4, 5, 6, 7, 8, 9}$.
The sets of $3$ elements of $\N_9$ adding to $15$ can be stated:
:$\set {1, 5, 9}, \set {1, 6, 8}$
:$\set {2, 4, 9}, \set {2, 5, 8}, \set {2, 6, 7}$
:$\set {3, 4, 8}, \set {3, 5, 7}$
:$\set {4, 5, 6}$
The number of rows, columns and diagonals of $M_3$ passing through each cell of $M_3$ depends upon where in $M_3$ that cell is positioned.
:The corner cells are each on one row, one column and one diagonal
:The edge cells are each on one row and one column
:The center cells is on one row, one column and both diagonals.
Thus the center cell has to contain an integer which is in at least $4$ of the $3$-element subsets of $\N^*_9$ above.
There is only one such element, which is $5$.
Thus $5$ goes in the center square of $M_3$.
By a similar analysis, it is seen that:
:the corner cells contain $2, 4, 6, 8$
:the edge cells contain $1, 3, 7, 9$.
{{WLOG}}, let $2$ be placed in the upper left corner of $M_3$.
There is no $3$-element subset of $\N^*_9$ adding to $15$ containing both $1$ and $2$.
It follows that $1$ cannot be placed on either the upper edge or left hand edge.
Thus $1$ must go into the right hand edge or the bottom edge.
{{WLOG}}, let $1$ be placed on the right hand edge.
Up to rotations and reflections, the placements of these three elements is unique.
Hence $M_3$ so far looks like this:
:$\begin {array} {|c|c|c|}
\hline 2 &    &   \\
\hline   &  5 & 1 \\
\hline   &    &   \\
\hline
\end {array}$
The population of the remaining cells is forced:
:$\begin {array} {|c|c|c|}
\hline 2 &   &   \\
\hline 9 & 5 & 1 \\
\hline   &   & 8 \\
\hline
\end {array}$
:$\begin {array} {|c|c|c|}
\hline 2 &   & 6 \\
\hline 9 & 5 & 1 \\
\hline 4 &   & 8 \\
\hline
\end {array}$
:$\begin {array} {|c|c|c|}
\hline 2 & 7 & 6 \\
\hline 9 & 5 & 1 \\
\hline 4 & 3 & 8 \\
\hline
\end {array}$
{{qed}}
Theorem: Wholly Real Number and Wholly Imaginary Number are Linearly Independent over the Rationals

Let $z_1$ be a non-zero wholly real number.
Let $z_2$ be a non-zero wholly imaginary number.
Then, $z_1$ and $z_2$ are linearly independent over the rational numbers $\Q$, where the group is the complex numbers $\C$.

Proof:
From Rational Numbers form Subfield of Complex Numbers, the unitary module $\struct {\C, +, \times}_\Q$ over $\Q$ satisfies the unitary module axioms:
* Ring Action: $\C$ is closed under multiplication, so $\Q \times \C \subset \C$.
* Distributive: $\times$ distributes over $+$.
* Associativity: $\times$ is associative.
* Multiplicative Identity: $1$ is the multiplicative identity in $\C$.
Let $a, b \in \Q$ such that:
:$a z_1 + b z_2 = 0$
By the definition of wholly imaginary, there is a real number $c$ such that:
:$c i = z_2$
where $i$ is the imaginary unit.
Therefore:
:$a z_1 + b c i = 0$
Equating real parts and imaginary parts:
:$a z_1 = 0$
:$b c = 0$
Since $z_1$ and $c$ are both non-zero, $a$ and $b$ must be zero.
The result follows from the definition of linear independence.
{{qed}}
Category:Complex Analysis
h6891ybvubvreqkw6jcere9hu30w7m6
Theorem: Schanuel's Conjecture Implies Algebraic Independence of Pi and Log of Pi over the Rationals

Let Schanuel's Conjecture be true.
Then $\pi$ (pi) and the logarithm of $\pi$ (pi):
:$\ln \pi$
are algebraically independent over the rational numbers $\Q$.

Proof:
Assume the truth of Schanuel's Conjecture.
Let $z_1 = \ln \pi$, $z_2 = i \pi$.
Note that $z_1$ is wholly real and $z_2$ is wholly imaginary.
Hence, by Wholly Real Number and Wholly Imaginary Number are Linearly Independent over the Rationals, they are linearly independent over $\Q$.
By Schanuel's Conjecture, the extension field $\Q \left({z_1, z_2, e^{z_1}, e^{z_2}}\right)$ has transcendence degree at least $2$ over $\Q$.
That is, the extension field $\Q \left({\ln \pi, i \pi, \pi, e^{i \pi}}\right)$ has transcendence degree at least $2$ over $\Q$.
However, by Euler's Identity, $e^{i \pi} = -1$ is algebraic.
Also, $i \pi$ and $\pi$ are not algebraically independent, as they satisfy $x^2 + y^2 = 0$, where $x = i \pi$ and $y = \pi$.
Therefore, if Schanuel's Conjecture holds, then $\ln \pi$ and $\pi$ are algebraically independent.
{{qed}}
Category:Transcendental Numbers
Category:Pi
Category:Logarithms
Category:Schanuel's Conjecture
sibv8slqarxunibd8j24sjrfl6cl59o
Theorem: Hermite-Lindemann-Weierstrass Theorem/Weaker/Corollary

Let $a$ be a algebraic number (possibly complex) which is neither $0$ nor $1$.
Then:
:every value of $\ln a$ is transcendental
where $\ln$ denotes complex natural logarithm.

Proof:
{{AimForCont}} $\ln a$ is not transcendental.
Hence, by definition, it is algebraic.
Since $a$ is not $1$, $\ln a$ cannot be $0$.
Hence, by the Weaker Hermite-Lindemann-Weierstrass Theorem, $e^{\ln a} = a$ is transcendental.
This contradicts the assumption that $a$ is algebraic.
Hence, $\ln a$ must be transcendental.
{{qed}}
Category:Hermite-Lindemann-Weierstrass Theorem
g7fciwjchom01kgukhmg6qe3es0oh56
Theorem: Lines through Center Square of Order 3 Magic Square are in Arithmetic Sequence

Consider the order 3 magic square:
{{:Magic Square/Examples/Order 3}}
Each of the lines through the center cell contain $3$ integers in arithmetic sequence.

Proof:
By observation:
:$\tuple {1, 5, 9}$: common difference $4$
:$\tuple {2, 5, 8}$: common difference $3$
:$\tuple {3, 5, 7}$: common difference $2$
:$\tuple {4, 5, 6}$: common difference $1$
{{qed}}
Theorem: Sums of Squares in Lines of Order 3 Magic Square

Consider the order 3 magic square:
{{:Magic Square/Examples/Order 3}}
: The sums of the squares of the top and bottom rows are equal, and differ by $18$ from the sums of the squares of the middle row
: The sums of the squares of the left and right columns are equal , and differ by $18$ from the sums of the squares of the middle column.

Proof:
For the rows:
{{begin-eqn}}
{{eqn | l = 2^2 + 7^2 + 6^2
      | r = 4 + 49 + 36
      | c = 
}}
{{eqn | r = 89
      | c = 
}}
{{eqn | l = 4^2 + 3^2 + 8^2
      | r = 16 + 9 + 64
      | c = 
}}
{{eqn | r = 89
      | c = 
}}
{{eqn | l = 9^2 + 5^2 + 1^2
      | r = 81 + 25 + 1
      | c = 
}}
{{eqn | r = 107
      | c = 
}}
{{eqn | r = 89 + 18
      | c = 
}}
{{end-eqn}}
For the colums:
{{begin-eqn}}
{{eqn | l = 2^2 + 9^2 + 4^2
      | r = 4 + 81 + 16
      | c = 
}}
{{eqn | r = 101
      | c = 
}}
{{eqn | l = 6^2 + 1^2 + 8^2
      | r = 36 + 1 + 64
      | c = 
}}
{{eqn | r = 101
      | c = 
}}
{{eqn | l = 7^2 + 5^2 + 3^2
      | r = 49 + 25 + 9
      | c = 
}}
{{eqn | r = 83
      | c = 
}}
{{eqn | r = 101 - 18
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Omega Constant is Transcendental

The omega constant is transcendental.

Proof:
From the definition of omega constant, it is the real number $\Omega$ such that:
:$\Omega \, e^\Omega = 1$
where $e$ denotes Euler's number.
{{AimForCont}} $\Omega$ is not transcendental.
Hence, by definition, $\Omega$ is algebraic.
Then $e^\Omega$ is also algebraic, because:
:$e^\Omega = \dfrac 1 \Omega$
However, by the Weaker Hermite-Lindemann-Weierstrass Theorem, $e^\Omega$ is transcendental.
From this contradiction it follows that $\Omega$ is transcendental.
{{qed}}
Category:Omega Constant
Category:Lambert W Function
Category:Transcendental Number Theory
k5z126q2n04njifgv61c9lih661rz93
Theorem: Lambert W of Zero is Zero

Let $W_0$ denote principal branch of the Lambert W function.
Then:
:$W_0 \left({0}\right) = 0$

Proof:
From the definition of the principal branch of the Lambert W function:
:$y = W_0 \left({x}\right) \iff x = y e^y$
where $x \in \left[{-\dfrac 1 e \,.\,.\, \to}\right)$ and $y \in \left[{-1 \,.\,.\, \to}\right)$.
The result follows from substituting $x = 0$ and $y = 0$.
{{qed}}
Category:Lambert W Function
eqh9slzcxvkfb6vlmfhrna606w7srbu
Theorem: Sums of Squares of Lines of Order 3 Magic Square

Consider the order 3 magic square:
{{:Magic Square/Examples/Order 3}}
: The sums of the squares of the rows, when expressed as $3$-digit decimal numbers, are equal to the sums of the squares of those same rows of that same order 3 magic square when reflected in a vertical axis:
$\quad\begin{array}{|c|c|c|}
\hline 6 & 7 & 2 \\
\hline 1 & 5 & 9 \\
\hline 8 & 3 & 4 \\
\hline
\end{array}$
Similarly:
: The sums of the squares of the columns, when expressed as $3$-digit decimal numbers, are equal to the sums of the squares of those same columns of that same order 3 magic square when reflected in a horizontal axis:
$\quad\begin{array}{|c|c|c|}
\hline 4 & 3 & 8 \\
\hline 9 & 5 & 1 \\
\hline 2 & 7 & 6 \\
\hline
\end{array}$

Proof:
For the rows:
{{begin-eqn}}
{{eqn | l = 276^2 + 951^2 + 438^2
      | r = 76176 + 904401 + 191844
      | c = 
}}
{{eqn | r = 1172421
      | c = 
}}
{{eqn | l = 672^2 + 159^2 + 834^2
      | r = 451584 + 25281 + 695556
      | c = 
}}
{{eqn | r = 1172421
      | c = 
}}
{{end-eqn}}
For the columns:
{{begin-eqn}}
{{eqn | l = 492^2 + 357^2 + 816^2
      | r = 242064 + 127449 + 665856
      | c = 
}}
{{eqn | r = 1035369
      | c = 
}}
{{eqn | l = 294^2 + 753^2 + 618^2
      | r = 86436 + 567009 + 381924
      | c = 
}}
{{eqn | r = 1035369
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: 123456789 x 8 + 9 = 987654321

{{begin-eqn}}
{{eqn | l = 1 \times 8 + 1
      | r = 9
}}
{{eqn | l = 12 \times 8 + 2
      | r = 98
}}
{{eqn | l = 123 \times 8 + 3
      | r = 987
}}
{{eqn | l = 1234 \times 8 + 4
      | r = 9876
}}
{{eqn | l = 12345 \times 8 + 5
      | r = 98765
}}
{{eqn | l = 123456 \times 8 + 6
      | r = 987654
}}
{{eqn | l = 1234567 \times 8 + 7
      | r = 9876543
}}
{{eqn | l = 12345678 \times 8 + 8
      | r = 98765432
}}
{{eqn | l = 123456789 \times 8 + 9
      | r = 987654321
}}
{{end-eqn}}
The above pattern is an instance of the identity:
:$\ds \paren {b - 2} \sum_{j \mathop = 1}^n j b^{n - j} + n = \sum_{j \mathop = 1}^n \paren {b - j} b^{n - j}$
where $b = 10$ and $n$ goes from $1$ to $9$.

Proof:
The proof proceeds by induction.
Let $n, b \in \Z_{>0}$, where $b \ge 3$.
For all $n \in \Z_{\ge 1}$, let $\map P n$ be the proposition:
:$\ds \paren {b - 2} \sum_{j \mathop = 1}^n j b^{n - j} + n = \sum_{j \mathop = 1}^n \paren {b - j} b^{n - j}$
Theorem: 123456789 x 9 + 10 = 1111111111

{{begin-eqn}}
{{eqn | l = 1 \times 9 + 2
      | r = 11
}}
{{eqn | l = 12 \times 9 + 3
      | r = 111
}}
{{eqn | l = 123 \times 9 + 4
      | r = 1111
}}
{{eqn | l = 1234 \times 9 + 5
      | r = 11111
}}
{{eqn | l = 12345 \times 9 + 6
      | r = 111111
}}
{{eqn | l = 123456 \times 9 + 7
      | r = 1111111
}}
{{eqn | l = 1234567 \times 9 + 8
      | r = 11111111
}}
{{eqn | l = 12345678 \times 9 + 9
      | r = 111111111
}}
{{eqn | l = 123456789 \times 9 + 10
      | r = 1111111111
}}
{{end-eqn}}
The above pattern is an instance of the identity:
:$\ds \paren {b - 1} \sum_{j \mathop = 1}^n j b^{n - j} + n + 1 = \sum_{j \mathop = 0}^n b^j$
where $b = 10$ and $n$ goes from $1$ to $9$.

Proof:
The proof proceeds by induction.
Let $n, b \in \Z_{>0}$, where $b \ge 3$.
For all $n \in \Z_{\ge 1}$, let $\map P n$ be the proposition:
:$\ds \paren {b - 1} \sum_{j \mathop = 1}^n j b^{n - j} + n + 1 = \sum_{j \mathop = 0}^n b^j$
Theorem: Algebraic Numbers form Field

Let $\Bbb A$ denote the set of algebraic numbers in $\C$.
Then the algebraic structure $\struct {\Bbb A, +, \times}$ is a field.
In the above, $+$ and $\times$ denote complex addition and complex multiplication respectively.

Proof:
{{ProofWanted}}
Category:Algebraic Numbers
Category:Examples of Fields
Category:Algebraic Number Theory
fq9uwwnem55uakz1yx3fs8skplq2ko0
Theorem: Linearly Independent over the Rational Numbers iff Linearly Independent over the Integers

Let $z_1, z_2, \ldots, z_n$ be complex numbers.
Then:
:$z_1, z_2, \ldots, z_n$ are linearly independent over the rational numbers $\Q$
{{iff}}:
:$z_1, z_2, \ldots, z_n$ are linearly independent over the integers $\Z$.

Proof:
=== Forward implication ===
Let $z_1, z_2, \ldots, z_n$ be linearly independent over the rational numbers $\Q$.
That is, if $q_1, q_2, \ldots, q_n$ are rational numbers such that:
:$q_1 z_1 + q_2 z_2 + \cdots + q_n z_n = 0$
then:
:$q_1 = q_2 = \cdots = q_n = 0$
Let $a_1, a_2, \ldots, a_n$ be integers such that:
:$a_1 z_1 + a_2 z_2 + \cdots + a_n z_n = 0$
Then, by Integers form Subdomain of Rationals and the assumption, it follows that:
:$a_1 = a_2 = \cdots = a_n = 0$
Hence it follows by definition that $z_1, z_2, \ldots, z_n$ are linearly independent over the integers $\Z$.
{{qed|lemma}}
Theorem: Sums of Squares of Diagonals of Order 3 Magic Square

Consider the order 3 magic square:
{{:Magic Square/Examples/Order 3}}
The sums of the squares of the diagonals, when expressed as $3$-digit decimal numbers, are equal to the sums of the squares of those same diagonals of that same order 3 magic square when reversed.
{{improve|Find a way to describe the "diagonals" accurately, as what is being demonstrated here does not match the description.}}

Proof:
For the top-left to bottom-right diagonals:
{{begin-eqn}}
{{eqn | l = 258^2 + 714^2 + 693^2
      | r = 66564 + 509796 + 480249
      | c = 
}}
{{eqn | r = 1056609
      | c = 
}}
{{eqn | l = 852^2 + 417^2 + 396^2
      | r = 725904 + 173889 + 156816
      | c = 
}}
{{eqn | r = 1056609
      | c = 
}}
{{end-eqn}}
For the bottom-left to top-right diagonals:
{{begin-eqn}}
{{eqn | l = 456^2 + 312^2 + 897^2
      | r = 207936 + 97344 + 804609
      | c = 
}}
{{eqn | r = 1109889
      | c = 
}}
{{eqn | l = 654^2 + 213^2 + 798^2
      | r = 427716 + 45369 + 636804
      | c = 
}}
{{eqn | r = 1109889
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Lambert W of Non-Zero Algebraic Number is Transcendental

Let $W$ denote the (general) Lambert $W$ function.
Let $a$ be a non-zero algebraic number.
Then $\map W a$ is transcendental.

Proof:
From the definition of Lambert $W$ function:
:$a = \map W a e^{\map W a}$
{{AimForCont}} $\map W a$ is not transcendental.
Hence, $\map W a$ is algebraic.
From the Weaker Hermite-Lindemann-Weierstrass Theorem, $e^{\map W a}$ is transcendental.
However, from the equation above, it is also equal to:
:$\dfrac a {\map W a}$
which must be algebraic, considering the fact that $a$ and $\map W a$ are both algebraic.
It follows from this contradiction that $\map W a$ must be transcendental whenever $a$ is a non-zero algebraic number.
{{qed}}
Category:Lambert W Function
Category:Transcendental Number Theory
1xp6tjq7n8s3pv5af951b8onu4j8mpw
Theorem: Pi Squared is Irrational

Pi squared ($\pi^2$) is irrational.

Proof:
{{AimForCont}} $\pi^2$ is rational.
We establish a lemma:
=== Lemma ===
{{:Pi Squared is Irrational/Proof 1/Lemma}}{{qed|lemma}}
We will use the definition of $A_n$ from the lemma.
Then we will deduce that $A_n$ is an integer for all $n$.
First we confirm by direct integration that $A_0$ and $A_1$ are integers:
{{begin-eqn}}
{{eqn | l = A_0
      | r = \int_0^\pi \sin x \rd x
      | c = 
}}
{{eqn | r = 2
      | c = Area under Arc of Sine Function
}}
{{end-eqn}}
and 
{{begin-eqn}}
{{eqn | l = A_1
      | r = q \int_0^\pi x \paren {\pi - x} \sin x \rd x
      | c = 
}}
{{eqn | r = q \paren {\pi \int_0^\pi x \sin x \rd x - \int_0^\pi x^2 \sin x \rd x }
      | c = Linear Combination of Integrals
}}
{{eqn | r = q \paren {\pi \bigintlimits {- x \cos x + \sin x} 0 \pi - \bigintlimits {- x^2 \cos x + 2 x \sin x + 2 \cos x} 0 \pi }
      | c = Primitive of $x^n \sin a x$
}}
{{eqn | r = q \paren {\pi^2 - \pi^2 + 2 + 2}
      | c = Cosine of $\pi$, {{cos|0}}, Sine of $\pi$, {{sin|0}}
}}
{{eqn | r = 4 q
      | c = 
}}
{{end-eqn}}
Suppose $A_{k - 2}$ and $A_{k - 1}$ are integers. 
By our lemma:
:$A_k = \paren {4 n - 2} q A_{k - 1} - p q A_{k - 2}$
As $n$, $p$ and $q$ are all integers {{hypothesis}}, $A_k$ is also an integer.
So $A_n$ is an integer for all $n$ by Second Principle of Mathematical Induction.
{{qed|lemma}}
Let $x \in \closedint 0 \pi$.
From Shape of Sine Function and Real Sine Function is Bounded, we have:
:$0 \le \sin x \le 1$
From the Interior Extremum Theorem, we have:
{{begin-eqn}}
{{eqn | l = \map f x
      | r = x \paren {\pi - x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {f'} x
      | r = \pi - 2 x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 0
      | r = \pi - 2 x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \frac \pi 2
      | c = 
}}
{{end-eqn}}
Therefore, plugging $\dfrac \pi 2$ into $\map f x$, we obtain:
:$0 \le x \paren {\pi - x} \le \dfrac {\pi^2} 4$
Since $A_n$ is clearly positive and the length of the interval is $\pi$ and the integrand is bounded at $\paren {\pi^2 / 4}^n$, from Darboux's Theorem, we have:
:$0 < A_n < \pi \times \dfrac {q^n} {n!} \times \paren {\pi^2 / 4}^n$
From Power over Factorial:
:$\ds \lim_{n \mathop \to \infty} \frac {\paren {q \pi^2 / 4}^n} {n!} = 0$
It follows from the Squeeze Theorem that:
:$\ds \lim_{n \mathop \to \infty} A_n = 0$
Hence for sufficiently large $n$, $A_n$ is strictly between $0$ and $1$.
This contradicts the deduction that $A_n$ is an integer.
This depends on our supposition that $\pi^2$ is a rational number,
Hence by Proof by Contradiction it follows that $\pi^2$ is irrational.
{{qed}}
Theorem: Way Below in Lattice of Power Set

Let $X$ be a set.
Let $L = \struct {\powerset X, \cup, \cap, \preceq}$ be a lattice of power set of $X$ where $\mathord\preceq = \mathord\subseteq \cap \paren {\powerset X \times \powerset X}$
Let $x, y \in \powerset X$.
Then $x \ll y$ {{iff}}
:for every a set $Y$ of subsets of $X$ such that $y \subseteq \bigcup Y$
::then there exists a finite subset $Z$ of $Y$: $x \subseteq \bigcup Z$
where $\ll$ denotes the way below relation.

Proof:
=== Sufficient Condition ===
Let $x \ll y$
Let $Y$ be a set of subsets of $X$ such that
:$y \subseteq \bigcup Y$
By definitions of power set and subset:
:$Y \subseteq \powerset X$
By Power Set is Complete Lattice:
:$\bigcup Y = \sup Y$
By definition of $\preceq$:
:$y \preceq \sup Y$
By Way Below in Complete Lattice:
:there exists a finite subset $Z$ of $Y$: $x \preceq \sup Z$
By the proof of Power Set is Complete Lattice:
:$\bigcup Z = \sup Z$
Thus by definition of $\preceq$:
:there exists a finite subset $Z$ of $Y$: $x \subseteq \bigcup Z$
{{qed|lemma}}
Theorem: Divisibility by 10

An integer $N$ expressed in decimal notation is divisible by $10$ {{iff}} the {{LSD}} of $N$ is $0$.
That is:
:$N = \sqbrk {a_n \ldots a_2 a_1 a_0}_{10} = a_0 + a_1 10 + a_2 10^2 + \cdots + a_n 10^n$ is divisible by $10$ 
{{iff}}:
:$a_0 = 0$

Proof:
Let $N$ be divisible by $10$.
Then:
{{begin-eqn}}
{{eqn | l = N
      | o = \equiv
      | r = 0 \pmod {10}
}}
{{eqn | ll= \leadstoandfrom
      | l = \sum_{k \mathop = 0}^n a_k 10^k
      | o = \equiv
      | r = 0 \pmod {10}
}}
{{eqn | ll= \leadstoandfrom
      | l = a_0 + 10 \sum_{k \mathop = 1}^n a_k 10^{k - 1}
      | o = \equiv
      | r = 0 \pmod {10}
}}
{{eqn | ll= \leadstoandfrom
      | l = a_0
      | o = \equiv
      | r = 0 \pmod {10}
      | c = as $10 \equiv 0 \pmod {10}$
}}
{{end-eqn}}
{{qed}}