This is a long section which needs noticeable intuitionizing (most notably, complex logarithms won't work, or at least won't work easily, in a way more or less analogous to complex square root). Therefore, it seems wise to split the section into several pull requests.
We adopt a definition which agrees with the set.mm definition for positive real numbers, and prove those set.mm theorems which follow from that.
Also includes reeff1o which is based on the set.mm proof but needs two innovations:
show that the exponential function is strictly monotonic and use that in iset.mm's version of the intermediate value theorem, and
instead of proving the theorem for (0,1) and (1,+oo) and using real number trichotomy to glue those together, prove it for (0,_e) and (1,+oo) - gluing together two ranges in iset.mm is no problem as long as they overlap (in the 1 < _e sense, in this case).
Includes explanations in mmil.html of missing theorems in the previous section.
This is a long section which needs noticeable intuitionizing (most notably, complex logarithms won't work, or at least won't work easily, in a way more or less analogous to complex square root). Therefore, it seems wise to split the section into several pull requests.
We adopt a definition which agrees with the set.mm definition for positive real numbers, and prove those set.mm theorems which follow from that.
Also includes
reeff1owhich is based on the set.mm proof but needs two innovations:Includes explanations in mmil.html of missing theorems in the previous section.