Definition of complex number apartness looks too strong

[benjub]

...though it turns out to be correct !

Indeed, the current definition https://us.metamath.org/ileuni/df-ap.html defines two complex numbers as being apart from each other if their real parts are apart or their imaginary parts are apart. This is the intuitionistic "or", which is "strong": this implies that if two complex numbers are apart, you can prove that their real parts are apart or you can prove that their imaginary parts are apart.

A more cautious definition seems to be in terms of their distance being (strictly) positive. Depending on how you express that distance at that point of the development, something like

$z\not\neq w \leftrightarrow 0 < (z-w)^* (z-w)$

Then, this implies the current definition, because $\mathbb{C}$ is finite-dimensional as an $\mathbb{R}$-vector space: if $0 < a < (z-w)^* (z-w)$ then you can prove $a/4 < (\Re(z-w))^2 \vee a/4 < (\Im(z-w))^2$, etc. But formalizing that in iset.mm looks like it would involve sizeable changes since for instance theorems about the archimedean property use tightness of real apartness ~ax-pre-apti, so there would be some re-ordering of theorems.

(To a lesser extent, this applies to real apartness itself: define $x \not\neq y$ as $0<(x-y)^2$, and from $0<(x-y)^2$ you deduce $x < y \vee y < x$... but here, it would probably become almost tautological, since we will use ~ax-pre-apti.)

Still, it is the practice in (i)set.mm to have the "official" definition df-xxx be minimal, and then prove "alternate definitions" dfxxx2, etc., suited to later applications

Any thoughts ? (FYI @jkingdon @digama0)

[jkingdon]

I'm more concerned with showing equivalences (as we do with many dfxxxxn type theorems) than I am in worrying too much about which one is the $a and which one is the $p derived from it.

The df-ap we have now is taken directly from the cited source, and at least so far seems to have all the expected properties (irreflexivity, symmetry, cotransitivity, tightness, interaction with addition, multiplication, recirpocal, etc).

Adding some equivalences of the form x =//= y <-> .... seems like a good next step to me. It also means having the chance to work out various alternatives, ensure they really are equivalent, etc, before getting into the harder work of digging deeply into what we define in what order and what depends on what (which we can still do later if we want, I'm mostly saying don't start with that part).