We argue that

For integers *p**q* 0*p**q**p**p* = 2*q**q*

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

Thm* ( p:,q:.pp= 2qq)

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

p:,q:.pp= 2qq(p':.p'<p&qq= 2p'p')(see hypothesis

Hyp:4 of the proof)

We rewrite

( topp= 2qq)( qq= 2p'p')

and then

( toqq= 2p'p')( p'p'= 2q'q')

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

These rewrites are justified by a special-purpose lemma

Thm* p:,q:.pp= 2qq(p':.p'<p&qq= 2p'p')

See the

QED

There is also a proof generalizing from2 to any prime.Thm* with aa:. prime(a) (p:,q:.pp=aqq)gloss .

About: