Update odd/even so we can move theorems from Alexander van der Vekens mathbox

[jkingdon]

When last we visited the odd/even saga it was at #1682 and here is my attempt to summarize what we discussed there:

• Standard notation for even and odd, respectively, in set.mm is 2 || A and A e. ZZ /\ -. 2 || A. The former implies A e. ZZ by http://us.metamath.org/mpeuni/dvdszrcl.html (and although this discussion isn't primarily about iset.mm, that's also present in iset.mm: http://us.metamath.org/ileuni/dvdszrcl.html )
• Many of the odd/even theorems are in the section http://us.metamath.org/mpeuni/mmtheorems151.html#mm15003s and there is a section header there which summarizes the situation. (That's the section titled "Even and odd numbers" under "Elementary properties of divisibility", starting with http://us.metamath.org/mpeuni/evenelz.html , in case sections have been renumbered by the time you read this).
• Many theorems in Alexander van der Vekens mathbox use classes Even and Odd and at least some of those we'd like to move to main.

As I understand it the choices on the mathbox are:

1. Add Even and Odd to main, mostly because A e. Odd is shorter than A e. ZZ /\ -. 2 || A (if there are contexts where A e. ZZ is not already present), or
2. Modify the theorems in the mathbox (especially whichever ones we want to move to main) to use the 2 || A and A e. ZZ /\ -. 2 || A notation.

I'm not sure I have a strong opinion between those two. There was much discussion when this came up before and although I guess I'm sympathetic to the idea of sticking with the 2 || A notation as a way of reducing the number of notations we introduce, the odd case isn't quite as easy as the even case as described above.

[avekens]

Thierry's remarks in the Google group (https://groups.google.com/g/metamath/c/oOHiy3i-cRw/m/exLZuw-mAgAJ):

Indeed this is a good opportunity to raise (again) the question about the definition of odd integers.

I agree with Norm that2 || N is just as long as N e. Even, and therefore will not bring any database size improvement. Since it also implies 2 e. ZZ, I don't see worth in defining Even. For Odd this does not hold, one cannot just replace it with -. 2 || N but also has to add N e. ZZ to recover a definition of Odd.

To circumvent this, I have been using essential hypotheses in the form of O = { z e. ZZ | -. 2 || z }, like in ~ hgt749d and ~ eulerpart. This allows me to use the local O in the proof just like if it were a definition. We could also use this trick in main without defining a new symbol.

[avekens]

To circumvent this, I have been using essential hypotheses in the form of O = { z e. ZZ | -. 2 || z }, like in ~ hgt749d and ~ eulerpart. This allows me to use the local O in the proof just like if it were a definition. We could also use this trick in main without defining a new symbol.

If it is not accepted to have a dedicated symbol "Odd" (and if we have such a symbol, we also should have a symbol "Even" for symmetry reasons, although it would not really be needed), I already thought of using Thierry's local O. I could revise the theorems in my mathbox accordingly.

But if such a local definition is used very often (and a lot of auxiliary theorems will be useful, but be spread over many places), this would be an indication to have a dedicated symbol/definition for it, wouldn't it? And I expect a lot of auxiliary theorems, especially for the transformation of representations of odd and even numbers, as provided in sections "Even and odd numbers" (in main set.mm and my mathbox).

[digama0]

This is just my opinion, but I think we should use 2 || A and A e. ZZ /\ -. 2 || A respectively for even and odd. It's true that the latter is longer than A e. Odd, but just because it's shorter doesn't make it easier to manipulate: you will need to unpack this assumption to do anything with it, and Odd is not closed under many operations the same way as ZZ. I think most commonly you will already have the A e. ZZ assumption floating around in order to satisfy other theorems being applied on the number, so in context you only really need the -. 2 || A part.

That is, A e. ZZ is a typing assumption while -. 2 || A is a predicate on A, and having a typing assumption for the conjunction does not seem so useful because Odd is not a type that interacts well with other types.

[benjub]

You may also use 2 || ( A + 1 ). That being said, I think there ought to be a typing assumption of the form A e. ZZ, as Mario wrote. In particular, it may not be very safe to rely on "reverse closure" results, such as ( 2 || A -> A e. ZZ ) since we may in the future choose to define || on ( RR* X. RR* ) (with otherwise the same definition with extended integers) in which case we'll have 2 || +infty and 2 || ( +infty + 1 ) for instance. (edit: in this case, I recognize this is a very stretched example, but I still think relying on reverse closure is not very safe.)

For the moment @avekens's use of essential hypotheses of the form O = { n e. NN0 | 2 || ( n + 1 ) } may be a better option.

Rk: now, we also have the longer but more systematic O = ( ( { 2 } ( elmtwise `` x. ) NN0 ) ( elmtwise `` + ) { 1 } ).

[avekens]

Rk: now, we also have the longer but more systematic O = ( ( { 2 } ( elmtwise `` x. ) NN0 ) ( elmtwise `` + ) { 1 } ).

For a definition df-odd of a symbol Odd, I would agree that Odd = ( ( { 2 } ( elmtwise `` x. ) ZZ ) ( elmtwise `` + ) { 1 } ) could be used (together with theorems which show that Odd = { n e. ZZ | 2 || ( n + 1 ) } and Odd = { n e. ZZ | 2 || -. n || 2 } , but not for a local O which would be required as hypothesis many times.