I'd like to formalize the proof at
https://en.wikipedia.org/wiki/Square_root_of_2#Constructive_proof and
I'm not sure how to tackle the very first step, which is that given
positive integers a and b , ( 2 x. ( b ^ 2 ) ) =/= ( a ^ 2 ) . The proof
given there relies on valuation (highest power of 2 dividing a number):
do we have that concept in set.mm? Or something else which could prove
this lemma? I didn't see anything relevant but I don't really know the
number theory parts of set.mm super well.
Of course this is for iset.mm but if it exists in set.mm it should be
intuitionizable (being about integers and all).
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/091e76b1-0a93-f116-d15c-b043d8f4c5ae%40panix.com.
