IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrimesSquareRoots
Nuprl Section: PrimesSquareRoots - Stand-alone sample: Primes have no rational square roots.
Here we give formal proofs along with informal glosses of proofs to the effect that 2 has no rational square root, and more generally, that no prime number has a rational square root.
The proof about 2 is simpler, of course, and so is a better approach to the one about primes.
The method is to show that one could always convert a (non-negative) ratio whose square is two (or prime) into another one with a smaller numerator.
(
p:
, q:
. p
p = 2
a:
