Ah, thanks for looking at this in that much detail.
To go down the list of what isn't in iset.mm:
* ~dvdsle <http://us2.metamath.org:88/mpeuni/dvdsle.html> , ~1dvds
<http://us2.metamath.org:88/mpeuni/1dvds.html> , ~dvds0lem ,
<http://us2.metamath.org:88/mpeuni/dvds0lem.html>~dvdsmultr2
<http://us2.metamath.org:88/mpeuni/dvdsmultr2.html>, ~iddvdsexp
<http://us2.metamath.org:88/mpeuni/iddvdsexp.html> - I had been planning
to formalize http://us.metamath.org/mpeuni/df-dvds.html and related
theorems and I'm guessing they'll intuitionize. This might be my next
project - certainly one I assumed I'd take on before taking up that
square root of two is irrational.
* ~uzsupss <http://us2.metamath.org:88/mpeuni/uzsupss.html> This, as
well as some of the others you couldn't find, is listed at the "Metamath
Proof Explorer cross reference" at
http://us.metamath.org/ileuni/mmil.html#setmm . The big issue with
supremum, even for sets of integers, is.... I guess I can sum it up with
http://us.metamath.org/ileuni/nnregexmid.html . Likewise ~supcl
<http://us2.metamath.org:88/mpeuni/supcl.html> and ~supub
<http://us2.metamath.org:88/mpeuni/supub.html>
* ~fzfi <http://us2.metamath.org:88/mpeuni/fzfi.html> As listed in
mmil.html, this is standard intuitionizing of the "add a condition we
are within the domain" sort - http://us.metamath.org/ileuni/fzfig.html
* ~ssfi <http://us2.metamath.org:88/mpeuni/ssfi.html> Famously not
possible - http://us.metamath.org/ileuni/ssfiexmid.html . But I think we
probably can prove the particular set in this proof is finite.
* ~divmul2 <http://us2.metamath.org:88/mpeuni/divmul2.html> , ~mulcanad
<http://us2.metamath.org:88/mpeuni/mulcanad.html> , ~divcld
<http://us2.metamath.org:88/mpeuni/divcld.html> These are all listed in
mmil.html and have equivalents which use "apart from zero" rather than
"not equal to zero". The distinction isn't an issue for integers given
http://us.metamath.org/ileuni/zapne.html .
* ~expne0d <http://us2.metamath.org:88/mpeuni/expne0d.html> Likewise
this exists as http://us.metamath.org/ileuni/expap0d.html
> It would seem like using this would require a significant amount of
library building, all of which may or may not be intuitionizable.
Hmm, yeah, I'm in the business of library building but because this
looks a bit difficult/large I've put a version of these thoughts into
https://github.com/metamath/set.mm/issues/2298 which may be an easier
way to keep track of what is done or not done than an email thread.
On 11/5/21 5:57 AM, Kyle Wyonch wrote:
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 <http://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
<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
<http://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 <http://set.mm> super well.
Of course this is for iset.mm <http://iset.mm> but if it exists
in set.mm <http://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]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/98de7f4c-3e3a-408c-a733-a098e2de8ae2n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/98de7f4c-3e3a-408c-a733-a098e2de8ae2n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/4af97277-d2f3-e0dc-eee4-37273899ab5a%40panix.com.
