I was able to find ~f1od <http://us.metamath.org/ileuni/f1od.html> in iset.mm. However for ~oddpwdc <http://us2.metamath.org:88/mpeuni/oddpwdc.html>, I wasn't able to find ~dvdsle <http://us2.metamath.org:88/mpeuni/dvdsle.html>, ~uzsupss <http://us2.metamath.org:88/mpeuni/uzsupss.html>, ~supcl <http://us2.metamath.org:88/mpeuni/supcl.html>, ~fzfi <http://us2.metamath.org:88/mpeuni/fzfi.html>, ~ssfi <http://us2.metamath.org:88/mpeuni/ssfi.html>, ~1dvds <http://us2.metamath.org:88/mpeuni/1dvds.html>, ~divmul2 <http://us2.metamath.org:88/mpeuni/divmul2.html>, ~supub <http://us2.metamath.org:88/mpeuni/supub.html>, ~dvds0lem <http://us2.metamath.org:88/mpeuni/dvds0lem.html>, ~mulcanad <http://us2.metamath.org:88/mpeuni/mulcanad.html>, ~expne0d <http://us2.metamath.org:88/mpeuni/expne0d.html>, ~divcld <http://us2.metamath.org:88/mpeuni/divcld.html>, ~dvdsmultr2 <http://us2.metamath.org:88/mpeuni/dvdsmultr2.html>, ~iddvdsexp <http://us2.metamath.org:88/mpeuni/iddvdsexp.html>. As well, it would require recreating the four other theorems in Thierry's mathbox: ~nexple <http://us2.metamath.org:88/mpeuni/nexple.html>, ~f1od2 <http://us2.metamath.org:88/mpeuni/f1od2.html>, ~cnvoprab <http://us2.metamath.org:88/mpeuni/cnvoprab.html>, and ~spc2ed <http://us2.metamath.org:88/mpeuni/spc2ed.html>. It would seem like using this would require a significant amount of library building, all of which may or may not be intuitionizable.
On Friday, November 5, 2021 at 3:04:24 AM UTC-4 Thierry Arnoux wrote: > 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/98de7f4c-3e3a-408c-a733-a098e2de8ae2n%40googlegroups.com.
