Theorem sqrtrege0

Description: The square root function must make a choice between the two roots, which differ by a sign change. In the general complex case, the choice of "positive" and "negative" is not so clear. The convention we use is to take the root with positive real part, unless A is a nonpositive real (in which case both roots have 0 real part); in this case we take the one in the positive imaginary direction. Another way to look at this is that we choose the root that is largest with respect to lexicographic order on the complex numbers (sorting by real part first, then by imaginary part as tie-breaker). (Contributed by Mario Carneiro, 10-Jul-2013)

	Ref	Expression
Assertion	sqrtrege0	$$⊢A\in ℂ\to 0\le \Re \left(\sqrt{A}\right)$$

Proof

Step	Hyp	Ref	Expression
1		sqrtthlem	$$⊢A\in ℂ\to \left({\sqrt{A}}^2=A\wedge 0\le \Re \left(\sqrt{A}\right)\wedge \mathrm{i}\sqrt{A}\notin {ℝ}^{+}\right)$$
2	1	simp2d	$$⊢A\in ℂ\to 0\le \Re \left(\sqrt{A}\right)$$