A proof of the irrationality of $\protect\sqrt{2}$

Leslie Lamport

December 1, 1993

Abstract:

HTML version of a sample proof that uses Lamport's proof style [1], illustrating how structured proofs can be converted to HTML pages via L^ATEX2HTML enriched with extensions for Lamport's proof style.

Theorem There does not exist $r$ in Q such that $r^{2}=2$.

show proof

hide proof

Proof Sketch: We assume $r^{2}=2$ for $r\in{\bf Q}$ and obtain a contradiction. Writing $r=m/n$, where $m$ and $n$ have no common divisors (step <1>1), we deduce from $(m/n)^{2}=2$ and the lemma that both $m$ and $n$ must be divisible by 2 (<1>2 and <1>3). Assume:

1. $r\in{\bf Q}$
2. $r^{2}=2$

Prove:False
<1>1: Choose $m$, $n$ in Z such that

1. $\gcd(m,n) =1$
2. $r = (m/n)$

show proof

hide proof

<2>1: Choose $p$, $q$ in Z such that $q\neq 0$ and $r=p/q$.

show proof

hide proof

Proof: By assumption <0>:1.

Let: $m$ $\mathrel{\stackrel{\scriptscriptstyle\Delta}{=}}$ $p/\gcd(p,q)$
$n$ $\mathrel{\stackrel{\scriptscriptstyle\Delta}{=}}$ $q/\gcd(p,q)$
<2>2: $m,n\in {\bf Z}$

show proof

hide proof

Proof: <2>1 and definition of $m$ and $n$.

<2>3: $r=m/n$

show proof

hide proof

Proof: $m/n$ $=$ $$\frac{p/\gcd(p,q)}{q/\gcd(p,q)}$$ [Definition of $m$ and $n$] = $p/q$ [Simple algebra] = $r$ [By <2>1]

<2>4: $\gcd(m,n) =1$ Proof: By the definition of the gcd, it suffices to: Assume:

1. $s$ divides $m$
2. $s$ divides $n$

Prove:$s=\pm 1$

show proof

hide proof

<3>1: $s\cdot\gcd(p,q)$ divides $p$.

show proof

hide proof

Proof: <2>:1 and the definition of $m$.

<3>2: $s\cdot\gcd(p,q)$ divides $q$.

show proof

hide proof

Proof: <2>:2 and definition of $n$.

<3>3Q.E.D.

show proof

hide proof

Proof: <3>1, <3>2, and the definition of gcd.

<2>5Q.E.D.

<1>2: 2 divides $m$.

show proof

hide proof

<2>1: $m^{2}=2n^{2}$

show proof

hide proof

Proof: <1>1.1 implies $(m/n)^{2}=2$.

<2>2Q.E.D.

show proof

hide proof

Proof: By <2>1 and the lemma.

<1>3: 2 divides $n$.

show proof

hide proof

<2>1: Choose $p$ in Z such that $m=2p$.

show proof

hide proof

Proof: By <1>2.

<2>2: $n^{2}=2p^{2}$

show proof

hide proof

Proof: 2 = $(m/n)^{2}$ [<1>1.2 and <0>:2] = $(2p/n)^{2}$ [<2>1] = $4p^{2}/n^{2}$ [Algebra] from which the result follows easily by algebra.

<2>3Q.E.D.

show proof

hide proof

Proof: By <2>2 and the lemma.

<1>4Q.E.D.

show proof

hide proof

Proof: <1>1.1, <1>2, <1>3, and definition of gcd.

Bibliography

1

Leslie Lamport, 1993, How to write a proof. In Global Analysis of Modern Mathematics, pp. 311-321. Publish or Perish, Houston, Texas, February 1993. A symposium in honor of Richard Palais' sixtieth birthday (also published as SRC Research Report 94). http://research.microsoft.com/users/lamport/proofs/src94.ps.Z

About this document ...

A proof of the irrationality of $\protect\sqrt{2}$

This document was generated using the LaTeX2HTML translator Version 2K.1beta (1.56)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.

The command line arguments were:
latex2html ll1

The translation was initiated by Glowacki Martin / TU Wien Studenten Account Kopie on 2002-10-01

URL of this proof as currently expanded for referencing and bookmarking purposes.

This HTML file was generated using the pf2html extension, version 0.03.
LaTeX2HTML + pf.sty (hypertext proofs).

Project homepage at http://www.dbai.tuwien.ac.at/proj/pf2html