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 hgsgm on Thursday January 19, 2023 @08:39AM (#34440097)

Doesn't work, because in

    k * (3/2 - 1)(3/2) = k'(9/4) - k(3/2)

(3/2)^2 = 9/4 is not an integer, you don't get k' < K so there is no contradiction.

You'd only get an integer if 4 divides k', which doesn't happen, because

    k = 2

and

    k' = k(3/2 -1) = k/2 = 1

[ Parent | on HN ]

Re:Formalising a new proof that the square root of two is ir... by rhn_mk1 on Thursday January 19, 2023 @09:03AM (#34440353)

Thanks, you're right. I missed that there was supposed to be a √2*√2 in the expansion of the last line.

[ Parent | on HN ]