We argue that prime numbers have no rational square roots.

For integers *p**q* 0*p**q**a**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:.pp=aqq)

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* *p**p'**p'**q'*

p:,q:.pp=aqq(p':.p'<p& (q':.p'p'=aq'q'))(see hypothesis

Hyp:6 of the proof)

We rewrite

( topp=aqq)( qq=ap'p')

and then

( toqq=ap'p')( p'p'=aq'q')

giving us a rational square root with numerator *p'*<*p**q'*

These rewrites are justified by a special-purpose lemma

Thm* a:.

Thm* prime(a) (p:,q:.pp=aqq(p':.p'<p&qq=ap'p'))

See the

QED

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

About: