Add existence of real square roots to iset.mm

[jkingdon]

Most of the details are at #2101 ; here is a summary of what is in this pull request:

• Add Jia Ming to authors list as described in Shorten pm3.2 from iset.mm #1877 (comment)
• Add some theorems about if and about the A. j e. NN E. k e. ( ZZ>= ` j ) idiom (based pretty closely on theorems from set.mm)
• Add divmuldivapd and rpap0d which are just two of the usual ones about negated equality versus apartness (apparently these two had slipped through the cracks earlier)
• Add cvg1n which is like http://us.metamath.org/ileuni/caucvgre.html but changes 1 / n to C / n (that is, adjusts the rate of convergence by a constant multiplier).
• Add resqrex (including many lemmas) - this is described in How should we show square roots exist in iset.mm? #2101 in a decent amount of detail.

Even more than usual, this is one which I would have a very hard time doing without the help of @digama0 who is basically the author of the proof of square root existence (that is, the comments in #2101 form a relatively detailed informal proof which is formalized in this pull request).

This is super exciting because it is the first time that we actually are making RR behave like the reals (in terms of both having a completeness axiom and using it to do the usual sorts of mathematics that we expect from real numbers). This will unlock a whole bunch of things - in the near term things like real and complex absolute value, maximum (#2115 ), the ability to more easily express sequence convergence, and maybe a bunch of convergence results (although that's a bit of a big one in the sense that a bunch of convergence theorems need to be modified or omitted without excluded middle). Once some of those are in place, we should be able to proceed to complex exponentiation and trigonometry which is of course important because it puts http://us.metamath.org/mpeuni/taupi.html within range <wink>.

Fixes #2101

[jkingdon]

The tests were not run on this branch (at least yet), presumably because of "GitHub Actions is now experiencing degraded availability" as noted at https://www.githubstatus.com/

@nmegill You might want to refrain from merging until github is fully back up, to avoid the situation where code is merged which doesn't pass the tests. I'll leave it to you to decide.

[nmegill]

@nmegill You might want to refrain from merging until github is fully back up, to avoid the situation where code is merged which doesn't pass the tests. I'll leave it to you to decide.

I'll wait until the tests can be run. Post a message to ping me when it is done.

BTW congrats on this milestone!

[jkingdon]

I'll wait until the tests can be run. Post a message to ping me when it is done.

@nmegill The test runner is back and the tests have run and passed.

BTW congrats on this milestone!

Thanks! A happy milestone indeed 🎉

[benjub]

@jkingdon This is nitpicking, but the two conjuncts in resqrex and rsqrmo are swapped, so that rersqreu has to use ancom (and http://us2.metamath.org/ileuni/mmtheorems94.html#resqrex looks less nice than it could). Also, is there a reason for the label discrepancies (as opposed to resqr* for the three of them) ? (same with rersqrtthlem)

[jkingdon]

@jkingdon This is nitpicking, but the two conjuncts in resqrex and rsqrmo are swapped, so that rersqreu has to use ancom (and http://us2.metamath.org/ileuni/mmtheorems94.html#resqrex looks less nice than it could). Also, is there a reason for the label discrepancies (as opposed to resqr* for the three of them) ? (same with rersqrtthlem)

I'll start with the easy one. resqrex in iset.mm is the same as http://us.metamath.org/mpeuni/resqrex.html (in terms of the conclusion of the theorem - the proof is different of course) because (according to a policy which I think is generally agreed upon if occasionally controversial) we like to keep iset.mm and set.mm the same (in terms of theorem names, naming of variables, order of hypotheses, etc) where we can. The combination of this principle and its variation - "change the name if it is different from set.mm" - is part of what leads to the funny naming. I have generally found these two principles to be valuable (a) when copying proofs between set.mm and iset.mm, either wholesale when possible, or also step-by-step in a more manual way, and also (b) just in terms of making it easier to read set.mm and iset.mm, understand how they differ, etc. Having said that we can discuss either how absolute the principles are, or whether there is a way to improve sqrt names even if we follow those principles. I think @digama0 may have a different perspective and I try to accomodate his ideas too (e.g. in fvex where we accepted some changes which are more about making iset.mm coherent with itself).

As for http://us.metamath.org/mpeuni/sqrmo.html versus http://us.metamath.org/ileuni/rsqrmo.html well those are different because complex square roots are tough as described at http://us.metamath.org/ileuni/df-rsqrt.html . So then the question is what order to use in the iset.mm one. The order right now is based on http://us.metamath.org/ileuni/df-rsqrt.html which is (sort of loosely, given their differences) based on http://us.metamath.org/mpeuni/df-sqrt.html . I guess maybe it is better to keep them a little similar? But I'm not sure I have a strong opinion on this one.

Thanks for taking a look at these sorts of questions. I hope none of my explanations come across as "we shouldn't change anything no matter what" because one of the things which has made set.mm good is that we aren't afraid to revisit old decisions and improve things. So I hope that spirit of ongoing improvement motivates the ongoing development of iset.mm.

[digama0]

Since I was mentioned, I will just mention my preference for naming:

• I agree that when it is possible to prove a theorem in set.mm with the same statement in iset.mm, we should definitely do so and it should get the same name as the original.
• When this is not possible, but there is a unique nearest equivalent that adds some relatively unimportant hypothesis (like a set existence or closure condition on some variables), then it should still be named the same as the original, as an aid to translations.
• When there are multiple variations, none of which is a clear best match for the original, they should all get different names, or possibly the "most preferred" version should get the original name. Again, this is intended as an aid to translations, since it functions as a "did you mean X?" when referencing set.mm theorems in iset.mm.

That is, I agree with @jkingdon 's first principle, but am more inclined to overlap set.mm names than in his converse principle "change the name if it is different from set.mm", because it makes iset.mm naming make sense on its own, even without the set.mm names as a point of reference.

[digama0]

By the way, it should be possible to define the complex square root function on all complex numbers satisfying ( Im ` x ) # 0 \/ 0 <_ ( Re ` x ), using a similar construction to the one used in set.mm. You need the real square root as a basis for the construction, but then there is a trick using the complex number x + |x| (see sqreu) that yields the complex square root whenever it is apart from zero (you need to divide by it at one point IIRC), which is exactly on the negative real line. You can either live with this constraint, which gives you the complex square root except on the negative real line (which puts a hole at zero), or you can extend it by continuity to zero as well by joining it with the real square root. The disjunctive domain of the resulting function might not be so useful though.

[jkingdon]

Since I was mentioned, I will just mention my preference for naming

Sounds like there is more agreement than I thought (and, hopefully, enough to keep working without getting too tangled up on names). We can continue to update the "1. Naming" section near the top of iset.mm if we want to express more of this in an "official" way, but perhaps this provides you with at least as much as you wanted to know about how things are named, @benjub ?

By the way, it should be possible to define the complex square root function . . .

I've copy-pasted this comment to the df-sqrt entry in the missing theorems list on the branch I'm currently working on - https://github.com/jkingdon/set.mm/blob/iset-seqfeq/mmil.raw.html which will end up at http://us.metamath.org/ileuni/mmil.html#setmm once that branch is merged.

I would totally agree with the concept that we can do something with complex square roots, and whatever we say on the topic should acknowledge that. But "we haven't needed them yet" is also true (at least so far). For example, absolute value on all complex numbers only needs square root on nonnegative reals.

[digama0]

In set.mm, that's the order of development as well: real square root -> absolute value -> complex square root. That's why the square root section is split into two parts, because sqreu requires facts about the absolute value function. (The definition using iota is a trick to avoid having to define two square root functions.) As for uses of the complex square root function, it's true that those probably won't come up for a long time (if ever); it will start being useful around the same time as the complex logarithm and complex power function.

[benjub]

Thanks for the explanations.