A Constructive Proof of

The following is a simple proof that 2 cannot be expressed as the ratio of two integers; that is, for every two integers p and q, (p/q)2 ≠ 2. This is a simplified version of a similar proof by Milad Niqui.

Use Alt+/ to step through the proof, and observe the proof state on the right panel.

First, we simplify the goal a bit by inlining the definition of 2.

The proof proceeds by complete induction on q, generalizing over p.

The gist of the proof is realizing that it can be obtained by instantiating the induction hypothesis with values 3q2p and 3p4q.

The rest follows from simpler inequalities, 2p < 3q < 2p+q and 4q < 3p. These are not included in the example; for details, see the full proof below.

Special thanks to Karl Palmskog for writing up this version.
{{the-document}}