Metamath Proof Explorer


Theorem sqrtcval2

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

Ref Expression
Assertion sqrtcval2 A A = A + A 2 + if A < 0 i i A A 2

Proof

Step Hyp Ref Expression
1 sqrtcval A A = A + A 2 + i if A < 0 1 1 A A 2
2 ovif2 i if A < 0 1 1 = if A < 0 i -1 i 1
3 neg1cn 1
4 ax-icn i
5 4 mulm1i -1 i = i
6 3 4 5 mulcomli i -1 = i
7 4 mulid1i i 1 = i
8 ifeq12 i -1 = i i 1 = i if A < 0 i -1 i 1 = if A < 0 i i
9 6 7 8 mp2an if A < 0 i -1 i 1 = if A < 0 i i
10 2 9 eqtr2i if A < 0 i i = i if A < 0 1 1
11 10 a1i A if A < 0 i i = i if A < 0 1 1
12 11 oveq1d A if A < 0 i i A A 2 = i if A < 0 1 1 A A 2
13 4 a1i A i
14 neg1rr 1
15 1re 1
16 14 15 ifcli if A < 0 1 1
17 16 a1i A if A < 0 1 1
18 17 recnd A if A < 0 1 1
19 sqrtcvallem3 A A A 2
20 19 recnd A A A 2
21 13 18 20 mulassd A i if A < 0 1 1 A A 2 = i if A < 0 1 1 A A 2
22 12 21 eqtrd A if A < 0 i i A A 2 = i if A < 0 1 1 A A 2
23 22 oveq2d A A + A 2 + if A < 0 i i A A 2 = A + A 2 + i if A < 0 1 1 A A 2
24 1 23 eqtr4d A A = A + A 2 + if A < 0 i i A A 2