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 3/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 = \frac \pi 2 \frac {p^0} {0!}  \int_0^1 \paren {1 - x^2 }^0 \map \cos {\dfrac {\pi x} 2} \rd x
      | c = 
}}
{{eqn | r = \frac \pi 2 \int_0^1 \map \cos {\dfrac {\pi x} 2} \rd x
      | c = Zeroth Power of Real Number equals One, Factorial of Zero
}}
{{eqn | r = \frac \pi 2 \times \frac 2 \pi \times \bigintlimits {\map \sin {\dfrac {\pi x} 2} } 0 1
      | c = {{Corollary|Primitive of Cosine Function}}
}}
{{eqn | r = 1
      | c = {{sin|0}}, {{sin|90}}
}}
{{end-eqn}}
and 
{{begin-eqn}}
{{eqn | l = A_1
      | r = \frac \pi 2 \frac {p^1} {1!}  \int_0^1 \paren {1 - x^2 }^1 \map \cos {\dfrac {\pi x} 2} \rd x
      | c = 
}}
{{eqn | r = p \paren {\frac \pi 2 \int_0^1 \map \cos {\dfrac {\pi x} 2} \rd x - \frac \pi 2 \int_0^1 x^2 \map \cos {\dfrac {\pi x} 2} \rd x }
      | c = Linear Combination of Integrals
}}
{{eqn | r = p \paren {\frac \pi 2 \times \frac 2 \pi \times \bigintlimits {\map \sin {\dfrac {\pi x} 2} } 0 1 - \frac \pi 2 \bigintlimits {\frac 2 \pi x^2 \map \sin {\dfrac {\pi x} 2} + \paren {\frac 4 {\pi^2} } 2 x \map \cos {\dfrac {\pi x} 2} - 2 \paren {\frac 2 \pi }^3 \map \sin {\dfrac {\pi x} 2} } 0 1 }
      | c = {{Corollary|Primitive of Cosine Function}}, Primitive of $x^n \cos a x$
}}
{{eqn | r = p \paren {1 - \paren {1 - \frac 8 {\pi^2} } }
      | c = {{sin|0}}, {{sin|90}}, {{cos|0}}, {{cos|90}}
}}
{{eqn | r = p \paren {\frac 8 {p / q} }
      | c = assuming $\pi^2 = \dfrac p q$
}}
{{eqn | r = 8 q
      | c = 
}}
{{end-eqn}}
Suppose $A_{k - 2}$ and $A_{k - 1}$ are integers. 
By our lemma:
:$A_k = \paren {16 n - 8} q A_{k - 1} - 16 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 1$.
From Shape of Cosine Function and Real Cosine Function is Bounded, we have:
:$0 \le \map \cos {\dfrac {\pi x} 2} \le 1$
From the Interior Extremum Theorem, we have:
{{begin-eqn}}
{{eqn | l = \map f x
      | r = \paren {1 - x^2}^n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {f'} x
      | r = n \paren {1 - x^2}^{n - 1} \paren {-2 x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 0
      | r = n \paren {1 - x^2}^{n - 1} \paren {-2 x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = 0
      | c = $0$ is the maximum $\map f 0 = 1$ and $\pm 1$ is the minimum $\map f {\pm 1} = 0$
}}
{{end-eqn}}
Therefore, plugging $0$ into $\map f x$, we obtain:
:$0 \le \paren {1 - x^2}^n \le 1$
Since $A_n$ is clearly positive and the length of the interval is $1$ and the integrand is bounded at $\paren {1}^n$, from Darboux's Theorem, we have:
:$0 < A_n < 1 \times \dfrac \pi 2 \times \dfrac {p^n} {n!} \times \paren {1}^n$
From Power over Factorial:
:$\ds \lim_{n \mathop \to \infty} \dfrac {p^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}}