sqrtthlem is more general than resqrtthlem (sqrt section revision)

[icecream17]

https://us.metamath.org/mpeuni/sqrtthlem.html
https://us.metamath.org/mpeuni/resqrtthlem.html

sqrtthlem   | ⊢ (𝐴 ∈ ℂ           → (((√‘𝐴)↑2) = 𝐴 ∧ 0 ≤ (ℜ‘(√‘𝐴)) ∧ (i · (√‘𝐴)) ∉ ℝ+))
resqrtthlem | ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (((√‘𝐴)↑2) = 𝐴 ∧ 0 ≤ (ℜ‘(√‘𝐴)) ∧ (i · (√‘𝐴)) ∉ ℝ+))

This means that quite a few theorems can either be generalized to complex numbers completely, or a 0 ≤ 𝐴 condition can be removed, like in sqrt00, sqrtsq2, and sqrtmul. However, doing this is somewhat nontrivial, since sqrtthlem comes about 100 theorems after resqrtthlem.

[benjub]

We should probably first prove a theorem that comes before that section on square roots: the analogous generalization of https://us.metamath.org/mpeuni/sq11.html that proves injectivity of the square function on that half-plane.

[jkingdon]

For what it is worth, the decision to develop the real square root first and only later the complex square root is deliberate, per #2142 (comment)

Speaking from an iset.mm point of view, square root on nonnegative reals is a very different beast from complex square roots (with the latter being pretty problematic constructively and even a little weird with excluded middle - the hard part being the selection of one of the two roots). But I suppose you should do what makes sense for set.mm.