A proof of the irrationality
of
Leslie Lamport
December 1, 1993
Abstract:
Theorem There does not exist in Q such that .

Proof Sketch: We assume for and obtain a contradiction.
Writing , where and have no common divisors (step
<1>1),
we deduce from and the lemma that both and
must be divisible by 2 (<1>2 and <1>3).
Assume:


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



<2>1: Choose , in Z such that and .

Proof: By assumption <0>:1.

Let:
<2>2:

Proof: <2>1 and definition of and .

<2>3:

Proof: [Definition of and ]
= [Simple algebra]
= [By <2>1]

<2>4:
Proof: By the definition of the gcd, it suffices
to:
Assume:
 divides
 divides
Prove:

<3>1:
divides .

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

<3>2:
divides .

Proof: <2>:2 and definition of .

<3>3Q.E.D.

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


<2>5Q.E.D.

<1>2: 2 divides .

<2>1:

Proof: <1>1.1 implies .

<2>2Q.E.D.

Proof: By <2>1 and the lemma.


<1>3: 2 divides .

<2>1: Choose in Z such that .
<2>2:

Proof: 2 = [<1>1.2 and <0>:2]
= [<2>1]
= [Algebra]
from which the result follows easily by algebra.

<2>3Q.E.D.

Proof: By <2>2 and the lemma.


<1>4Q.E.D.

 1
 Leslie Lamport, 1993, How to write a proof. In
Global Analysis of Modern Mathematics, pp. 311321. 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
A proof of the irrationality
of
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 20021025
URL of this proof as currently expanded for referencing
and bookmarking purposes.
open all
close all
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
Glowacki Martin / TU Wien Studenten Account Kopie
20021025