IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
We argue that prime numbers have no rational square roots.

For integers p, and q 0, the ratio of p to q is the square root of an integer a just when p p = a q q.

We shall consider only the non-negative integers here, so we must show that

Thm* a: . prime(a   ( p: q:  p p = a q q)

It is impossible to build an infinite decreasing sequence of natural numbers, as is expressed by our principle

Thm* P:(   Prop). ( x: P(x  ( x': x'<x & P(x')))   ( x: P(x))

So, to show that a prime number a  has no rational square root, it is enough to show that if you could find a ratio "p/q", expressed with a non-negative numerator, whose square was a, then you could find a smaller such numerator p' of a rational root "p'/q'" i.e., p: q:  p p = a q q  ( p': p'<p & ( q':  p' p' = a q' q'))

(see hypothesis Hyp:6 of the proof)

We rewrite

(p p = a q q) to (q q = a p' p')

and then

(q q = a p' p') to (p' p' = a q' q')

giving us a rational square root with numerator p'<p and denominator q'. EXAMPLE

These rewrites are justified by a special-purpose lemma

Thm* a: Thm*  prime(a  ( p: q:  p p = a q q  ( p':  p'<p & q q = a p' p'))

See the GLOSS of the lemma.

QED

There is also a specialized proof for a = 2. It is simpler but similar.
Thm* ( p: q:  p p = 2 q q) with a gloss. 