Formalising a new proof that the square root of two is irrational

Re:Formalising a new proof that the square root of two is ir... by scotty79 on Thursday January 19, 2023 @07:58AM (#34439816)

Let K be the set of positive integers k such that k * 3 is an integer.

Suppose K is non-empty, denote its minimum as k.

Consider the positive integer k' = k 3 - k = k (3 - 1).

Then k' < k (?!) and k' is also in K since k' 3 = 2 k - k 3, contradicting non-emptyness of K.

I guess my questions are why k' < k and why k'√2 is positive?

[ Parent | on HN ]

Re:Formalising a new proof that the square root of two is ir... by pfortuny on Thursday January 19, 2023 @08:04AM (#34439850)

Notice thay you know sqrt(2)<2 (this is easy), which does not happen in your case.

[ Parent | on HN ]