Theorem sqrtcval2

Description: Explicit formula for the complex square root in terms of the square root of non-negative reals. The right side is slightly more compact than sqrtcval . (Contributed by RP, 18-May-2024)

	Ref	Expression
Assertion	sqrtcval2	$$⊢A\in ℂ\to \sqrt{A}=\sqrt{\frac{\left|A\right|+\Re \left(A\right)}{2}}+if\left(\Im \left(A\right)<0,-\mathrm{i},\mathrm{i}\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}$$

Proof

Step	Hyp	Ref	Expression
1		sqrtcval	$$⊢A\in ℂ\to \sqrt{A}=\sqrt{\frac{\left|A\right|+\Re \left(A\right)}{2}}+\mathrm{i}if\left(\Im \left(A\right)<0,-1,1\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}$$
2		ovif2	$$⊢\mathrm{i}if\left(\Im \left(A\right)<0,-1,1\right)=if\left(\Im \left(A\right)<0,\mathrm{i}-1,\mathrm{i}\cdot 1\right)$$
3		neg1cn	$$⊢-1\in ℂ$$
4		ax-icn	$$⊢\mathrm{i}\in ℂ$$
5	4	mulm1i	$$⊢-1\mathrm{i}=-\mathrm{i}$$
6	3 4 5	mulcomli	$$⊢\mathrm{i}-1=-\mathrm{i}$$
7	4	mulid1i	$$⊢\mathrm{i}\cdot 1=\mathrm{i}$$
8		ifeq12	$$⊢\left(\mathrm{i}-1=-\mathrm{i}\wedge \mathrm{i}\cdot 1=\mathrm{i}\right)\to if\left(\Im \left(A\right)<0,\mathrm{i}-1,\mathrm{i}\cdot 1\right)=if\left(\Im \left(A\right)<0,-\mathrm{i},\mathrm{i}\right)$$
9	6 7 8	mp2an	$$⊢if\left(\Im \left(A\right)<0,\mathrm{i}-1,\mathrm{i}\cdot 1\right)=if\left(\Im \left(A\right)<0,-\mathrm{i},\mathrm{i}\right)$$
10	2 9	eqtr2i	$$⊢if\left(\Im \left(A\right)<0,-\mathrm{i},\mathrm{i}\right)=\mathrm{i}if\left(\Im \left(A\right)<0,-1,1\right)$$
11	10	a1i	$$⊢A\in ℂ\to if\left(\Im \left(A\right)<0,-\mathrm{i},\mathrm{i}\right)=\mathrm{i}if\left(\Im \left(A\right)<0,-1,1\right)$$
12	11	oveq1d	$$⊢A\in ℂ\to if\left(\Im \left(A\right)<0,-\mathrm{i},\mathrm{i}\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}=\mathrm{i}if\left(\Im \left(A\right)<0,-1,1\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}$$
13	4	a1i	$$⊢A\in ℂ\to \mathrm{i}\in ℂ$$
14		neg1rr	$$⊢-1\in ℝ$$
15		1re	$$⊢1\in ℝ$$
16	14 15	ifcli	$$⊢if\left(\Im \left(A\right)<0,-1,1\right)\in ℝ$$
17	16	a1i	$$⊢A\in ℂ\to if\left(\Im \left(A\right)<0,-1,1\right)\in ℝ$$
18	17	recnd	$$⊢A\in ℂ\to if\left(\Im \left(A\right)<0,-1,1\right)\in ℂ$$
19		sqrtcvallem3	$$⊢A\in ℂ\to \sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}\in ℝ$$
20	19	recnd	$$⊢A\in ℂ\to \sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}\in ℂ$$
21	13 18 20	mulassd	$$⊢A\in ℂ\to \mathrm{i}if\left(\Im \left(A\right)<0,-1,1\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}=\mathrm{i}if\left(\Im \left(A\right)<0,-1,1\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}$$
22	12 21	eqtrd	$$⊢A\in ℂ\to if\left(\Im \left(A\right)<0,-\mathrm{i},\mathrm{i}\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}=\mathrm{i}if\left(\Im \left(A\right)<0,-1,1\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}$$
23	22	oveq2d	$$⊢A\in ℂ\to \sqrt{\frac{\left|A\right|+\Re \left(A\right)}{2}}+if\left(\Im \left(A\right)<0,-\mathrm{i},\mathrm{i}\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}=\sqrt{\frac{\left|A\right|+\Re \left(A\right)}{2}}+\mathrm{i}if\left(\Im \left(A\right)<0,-1,1\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}$$
24	1 23	eqtr4d	$$⊢A\in ℂ\to \sqrt{A}=\sqrt{\frac{\left|A\right|+\Re \left(A\right)}{2}}+if\left(\Im \left(A\right)<0,-\mathrm{i},\mathrm{i}\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}$$