Hi Jim, I've used this concept in my proof of Euler's partition theorem, see ~oddpwdc <http://us2.metamath.org:88/mpeuni/oddpwdc.html>.
It states that the function mapping an odd integer `x` and a non-negative integer `y` to ` ( 2 ^ y ) x. x ` is a bijection to the positive integers. In other terms, any positive integer can be uniquely decomposed into the product of a power of two and an odd integer. I think that may be what you're looking for. I'm not sure if this is intuitionizable though (I could not find ~f1od in iset.mm) BR, _ Thierry On 05/11/2021 13:43, Jim Kingdon wrote:
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/c1f4ea4e-6b90-9f5e-344e-30dd4b18063e%40gmx.net.
