For integers 0
p = 2
q
q
We shall consider only the non-negative integers here, so we must show that
Thm* (
p:
, q:
. p
p = 2
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
p:
, q:
. p
p = 2
q
q
(
p':
. p'<p & q
q = 2
p'
p')
(see hypothesis
Hyp:4 of the proof)
We rewrite
(p top = 2
q
q)
(q q = 2
p'
p')
and then
(q toq = 2
p'
p')
(p' p' = 2
q'
q')
giving us a rational square root with numerator
These rewrites are justified by a special-purpose lemma
Thm* p:
, q:
. p
p = 2
q
q
(
p':
. p'<p & q
q = 2
p'
p')
See the
QED
There is also a proof generalizing from2 to any prime.Thm* with aa:
. prime(a)
![]()
(
p:
, q:
. p
p = a
q
q)
gloss .
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() |