Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sqrtcval Structured version   Visualization version   GIF version

Theorem sqrtcval 42695
Description: Explicit formula for the complex square root in terms of the square root of nonnegative reals. The right-hand side is decomposed into real and imaginary parts in the format expected by crrei 15144 and crimi 15145. This formula can be found in section 3.7.27 of Handbook of Mathematical Functions, ed. M. Abramowitz and I. A. Stegun (1965, Dover Press). (Contributed by RP, 18-May-2024.)
Assertion
Ref Expression
sqrtcval (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜๐ด) = ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))

Proof of Theorem sqrtcval
StepHypRef Expression
1 sqrtcvallem5 42694 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) โˆˆ โ„)
21recnd 11247 . . . 4 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) โˆˆ โ„‚)
3 ax-icn 11172 . . . . . 6 i โˆˆ โ„‚
43a1i 11 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ i โˆˆ โ„‚)
5 neg1rr 12332 . . . . . . . . 9 -1 โˆˆ โ„
6 1re 11219 . . . . . . . . 9 1 โˆˆ โ„
75, 6ifcli 4576 . . . . . . . 8 if((โ„‘โ€˜๐ด) < 0, -1, 1) โˆˆ โ„
87a1i 11 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ if((โ„‘โ€˜๐ด) < 0, -1, 1) โˆˆ โ„)
9 sqrtcvallem3 42692 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) โˆˆ โ„)
108, 9remulcld 11249 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))) โˆˆ โ„)
1110recnd 11247 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))) โˆˆ โ„‚)
124, 11mulcld 11239 . . . 4 (๐ด โˆˆ โ„‚ โ†’ (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) โˆˆ โ„‚)
132, 12addcld 11238 . . 3 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) โˆˆ โ„‚)
14 id 22 . . 3 (๐ด โˆˆ โ„‚ โ†’ ๐ด โˆˆ โ„‚)
15 binom2 14186 . . . . 5 (((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) โˆˆ โ„‚ โˆง (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) โˆˆ โ„‚) โ†’ (((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))โ†‘2) = ((((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) + (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) + ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2)))
162, 12, 15syl2anc 583 . . . 4 (๐ด โˆˆ โ„‚ โ†’ (((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))โ†‘2) = ((((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) + (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) + ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2)))
17 abscl 15230 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ (absโ€˜๐ด) โˆˆ โ„)
18 recl 15062 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ (โ„œโ€˜๐ด) โˆˆ โ„)
1917, 18readdcld 11248 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆˆ โ„)
2019rehalfcld 12464 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) โˆˆ โ„)
2120recnd 11247 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) โˆˆ โ„‚)
2221sqsqrtd 15391 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) = (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))
234, 11sqmuld 14128 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2) = ((iโ†‘2) ยท ((if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))โ†‘2)))
24 i2 14171 . . . . . . . . . . 11 (iโ†‘2) = -1
2524a1i 11 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (iโ†‘2) = -1)
268recnd 11247 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ if((โ„‘โ€˜๐ด) < 0, -1, 1) โˆˆ โ„‚)
279recnd 11247 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) โˆˆ โ„‚)
2826, 27sqmuld 14128 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ ((if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))โ†‘2) = ((if((โ„‘โ€˜๐ด) < 0, -1, 1)โ†‘2) ยท ((โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))โ†‘2)))
29 ovif 7509 . . . . . . . . . . . . . 14 (if((โ„‘โ€˜๐ด) < 0, -1, 1)โ†‘2) = if((โ„‘โ€˜๐ด) < 0, (-1โ†‘2), (1โ†‘2))
30 neg1sqe1 14165 . . . . . . . . . . . . . . 15 (-1โ†‘2) = 1
31 sq1 14164 . . . . . . . . . . . . . . 15 (1โ†‘2) = 1
32 ifeq12 4547 . . . . . . . . . . . . . . 15 (((-1โ†‘2) = 1 โˆง (1โ†‘2) = 1) โ†’ if((โ„‘โ€˜๐ด) < 0, (-1โ†‘2), (1โ†‘2)) = if((โ„‘โ€˜๐ด) < 0, 1, 1))
3330, 31, 32mp2an 689 . . . . . . . . . . . . . 14 if((โ„‘โ€˜๐ด) < 0, (-1โ†‘2), (1โ†‘2)) = if((โ„‘โ€˜๐ด) < 0, 1, 1)
34 ifid 4569 . . . . . . . . . . . . . 14 if((โ„‘โ€˜๐ด) < 0, 1, 1) = 1
3529, 33, 343eqtri 2763 . . . . . . . . . . . . 13 (if((โ„‘โ€˜๐ด) < 0, -1, 1)โ†‘2) = 1
3635a1i 11 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1)โ†‘2) = 1)
3717, 18resubcld 11647 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) โˆˆ โ„)
3837rehalfcld 12464 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2) โˆˆ โ„)
3938recnd 11247 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2) โˆˆ โ„‚)
4039sqsqrtd 15391 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))โ†‘2) = (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))
4136, 40oveq12d 7430 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ ((if((โ„‘โ€˜๐ด) < 0, -1, 1)โ†‘2) ยท ((โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))โ†‘2)) = (1 ยท (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))
4239mullidd 11237 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ (1 ยท (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) = (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))
4328, 41, 423eqtrd 2775 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ ((if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))โ†‘2) = (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))
4425, 43oveq12d 7430 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ ((iโ†‘2) ยท ((if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))โ†‘2)) = (-1 ยท (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))
4539mulm1d 11671 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (-1 ยท (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) = -(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))
4623, 44, 453eqtrd 2775 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2) = -(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))
4722, 46oveq12d 7430 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ (((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) + ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2)) = ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) + -(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))
4821, 39negsubd 11582 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) + -(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) = ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) โˆ’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))
4917recnd 11247 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ (absโ€˜๐ด) โˆˆ โ„‚)
5018recnd 11247 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ (โ„œโ€˜๐ด) โˆˆ โ„‚)
5149, 50, 50pnncand 11615 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆ’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) = ((โ„œโ€˜๐ด) + (โ„œโ€˜๐ด)))
52502timesd 12460 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (2 ยท (โ„œโ€˜๐ด)) = ((โ„œโ€˜๐ด) + (โ„œโ€˜๐ด)))
5351, 52eqtr4d 2774 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆ’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) = (2 ยท (โ„œโ€˜๐ด)))
5453oveq1d 7427 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆ’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) / 2) = ((2 ยท (โ„œโ€˜๐ด)) / 2))
5519recnd 11247 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆˆ โ„‚)
5637recnd 11247 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) โˆˆ โ„‚)
57 2cnd 12295 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ 2 โˆˆ โ„‚)
58 2ne0 12321 . . . . . . . . . 10 2 โ‰  0
5958a1i 11 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ 2 โ‰  0)
6055, 56, 57, 59divsubdird 12034 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆ’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) / 2) = ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) โˆ’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))
6150, 57, 59divcan3d 12000 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((2 ยท (โ„œโ€˜๐ด)) / 2) = (โ„œโ€˜๐ด))
6254, 60, 613eqtr3d 2779 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) โˆ’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) = (โ„œโ€˜๐ด))
6347, 48, 623eqtrd 2775 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ (((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) + ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2)) = (โ„œโ€˜๐ด))
6457, 2mulcld 11239 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ (2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) โˆˆ โ„‚)
6564, 4, 11mul12d 11428 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (i ยท ((2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))
6657, 2, 12mulassd 11242 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))))
6757, 2, 11mulassd 11242 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ ((2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) = (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))
682, 26, 27mul12d 11428 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) = (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))
69 sqrtcvallem4 42693 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))
70 halfnneg2 12448 . . . . . . . . . . . . . . . . 17 (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆˆ โ„ โ†’ (0 โ‰ค ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โ†” 0 โ‰ค (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)))
7119, 70syl 17 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ (0 โ‰ค ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โ†” 0 โ‰ค (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)))
7269, 71mpbird 256 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค ((absโ€˜๐ด) + (โ„œโ€˜๐ด)))
73 2rp 12984 . . . . . . . . . . . . . . . 16 2 โˆˆ โ„+
7473a1i 11 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ 2 โˆˆ โ„+)
7519, 72, 74sqrtdivd 15375 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) = ((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) / (โˆšโ€˜2)))
76 sqrtcvallem2 42691 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))
77 halfnneg2 12448 . . . . . . . . . . . . . . . . 17 (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) โˆˆ โ„ โ†’ (0 โ‰ค ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) โ†” 0 โ‰ค (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))
7837, 77syl 17 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ (0 โ‰ค ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) โ†” 0 โ‰ค (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))
7976, 78mpbird 256 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))
8037, 79, 74sqrtdivd 15375 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) = ((โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) / (โˆšโ€˜2)))
8175, 80oveq12d 7430 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))) = (((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) / (โˆšโ€˜2)) ยท ((โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) / (โˆšโ€˜2))))
8219, 72resqrtcld 15369 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) โˆˆ โ„)
8382recnd 11247 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) โˆˆ โ„‚)
84 2re 12291 . . . . . . . . . . . . . . . . 17 2 โˆˆ โ„
8584a1i 11 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ 2 โˆˆ โ„)
86 0le2 12319 . . . . . . . . . . . . . . . . 17 0 โ‰ค 2
8786a1i 11 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค 2)
8885, 87resqrtcld 15369 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜2) โˆˆ โ„)
8988recnd 11247 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜2) โˆˆ โ„‚)
9037, 79resqrtcld 15369 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) โˆˆ โ„)
9190recnd 11247 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) โˆˆ โ„‚)
92 sqrt00 15215 . . . . . . . . . . . . . . . . . 18 ((2 โˆˆ โ„ โˆง 0 โ‰ค 2) โ†’ ((โˆšโ€˜2) = 0 โ†” 2 = 0))
9384, 86, 92mp2an 689 . . . . . . . . . . . . . . . . 17 ((โˆšโ€˜2) = 0 โ†” 2 = 0)
9493necon3bii 2992 . . . . . . . . . . . . . . . 16 ((โˆšโ€˜2) โ‰  0 โ†” 2 โ‰  0)
9558, 94mpbir 230 . . . . . . . . . . . . . . 15 (โˆšโ€˜2) โ‰  0
9695a1i 11 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜2) โ‰  0)
9783, 89, 91, 89, 96, 96divmuldivd 12036 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ (((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) / (โˆšโ€˜2)) ยท ((โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) / (โˆšโ€˜2))) = (((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) ยท (โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))) / ((โˆšโ€˜2) ยท (โˆšโ€˜2))))
9818resqcld 14095 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„‚ โ†’ ((โ„œโ€˜๐ด)โ†‘2) โˆˆ โ„)
9998recnd 11247 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ ((โ„œโ€˜๐ด)โ†‘2) โˆˆ โ„‚)
100 imcl 15063 . . . . . . . . . . . . . . . . . . . 20 (๐ด โˆˆ โ„‚ โ†’ (โ„‘โ€˜๐ด) โˆˆ โ„)
101100resqcld 14095 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„‚ โ†’ ((โ„‘โ€˜๐ด)โ†‘2) โˆˆ โ„)
102101recnd 11247 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ ((โ„‘โ€˜๐ด)โ†‘2) โˆˆ โ„‚)
103 absvalsq2 15233 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด)โ†‘2) = (((โ„œโ€˜๐ด)โ†‘2) + ((โ„‘โ€˜๐ด)โ†‘2)))
10499, 102, 103mvrladdd 11632 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด)โ†‘2) โˆ’ ((โ„œโ€˜๐ด)โ†‘2)) = ((โ„‘โ€˜๐ด)โ†‘2))
105 subsq 14179 . . . . . . . . . . . . . . . . . 18 (((absโ€˜๐ด) โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) โˆˆ โ„‚) โ†’ (((absโ€˜๐ด)โ†‘2) โˆ’ ((โ„œโ€˜๐ด)โ†‘2)) = (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) ยท ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))))
10649, 50, 105syl2anc 583 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด)โ†‘2) โˆ’ ((โ„œโ€˜๐ด)โ†‘2)) = (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) ยท ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))))
107104, 106eqtr3d 2773 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ ((โ„‘โ€˜๐ด)โ†‘2) = (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) ยท ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))))
108107fveq2d 6896 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜((โ„‘โ€˜๐ด)โ†‘2)) = (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) ยท ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))))
109100absred 15368 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ (absโ€˜(โ„‘โ€˜๐ด)) = (โˆšโ€˜((โ„‘โ€˜๐ด)โ†‘2)))
110 reabsifneg 42686 . . . . . . . . . . . . . . . . 17 ((โ„‘โ€˜๐ด) โˆˆ โ„ โ†’ (absโ€˜(โ„‘โ€˜๐ด)) = if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)))
111100, 110syl 17 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ (absโ€˜(โ„‘โ€˜๐ด)) = if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)))
112109, 111eqtr3d 2773 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜((โ„‘โ€˜๐ด)โ†‘2)) = if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)))
11319, 72, 37, 79sqrtmuld 15376 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) ยท ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))) = ((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) ยท (โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))))
114108, 112, 1133eqtr3rd 2780 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) ยท (โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))) = if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)))
115 remsqsqrt 15208 . . . . . . . . . . . . . . . 16 ((2 โˆˆ โ„ โˆง 0 โ‰ค 2) โ†’ ((โˆšโ€˜2) ยท (โˆšโ€˜2)) = 2)
11684, 86, 115mp2an 689 . . . . . . . . . . . . . . 15 ((โˆšโ€˜2) ยท (โˆšโ€˜2)) = 2
117116a1i 11 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜2) ยท (โˆšโ€˜2)) = 2)
118114, 117oveq12d 7430 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ (((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) ยท (โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))) / ((โˆšโ€˜2) ยท (โˆšโ€˜2))) = (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2))
11981, 97, 1183eqtrd 2775 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))) = (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2))
120119oveq2d 7428 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) = (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2)))
12168, 120eqtrd 2771 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) = (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2)))
122121oveq2d 7428 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (2 ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2))))
123100renegcld 11646 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ -(โ„‘โ€˜๐ด) โˆˆ โ„)
124123, 100ifcld 4575 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) โˆˆ โ„)
125124recnd 11247 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) โˆˆ โ„‚)
12626, 125, 57, 59divassd 12030 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ ((if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด))) / 2) = (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2)))
127 ovif12 7511 . . . . . . . . . . . . . 14 (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด))) = if((โ„‘โ€˜๐ด) < 0, (-1 ยท -(โ„‘โ€˜๐ด)), (1 ยท (โ„‘โ€˜๐ด)))
1285a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„‚ โ†’ -1 โˆˆ โ„)
129128recnd 11247 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ -1 โˆˆ โ„‚)
130100recnd 11247 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ (โ„‘โ€˜๐ด) โˆˆ โ„‚)
131129, 129, 130mulassd 11242 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„‚ โ†’ ((-1 ยท -1) ยท (โ„‘โ€˜๐ด)) = (-1 ยท (-1 ยท (โ„‘โ€˜๐ด))))
132 neg1mulneg1e1 12430 . . . . . . . . . . . . . . . . . . . 20 (-1 ยท -1) = 1
133132a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„‚ โ†’ (-1 ยท -1) = 1)
134133oveq1d 7427 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ ((-1 ยท -1) ยท (โ„‘โ€˜๐ด)) = (1 ยท (โ„‘โ€˜๐ด)))
135130mullidd 11237 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ (1 ยท (โ„‘โ€˜๐ด)) = (โ„‘โ€˜๐ด))
136134, 135eqtrd 2771 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„‚ โ†’ ((-1 ยท -1) ยท (โ„‘โ€˜๐ด)) = (โ„‘โ€˜๐ด))
137130mulm1d 11671 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ (-1 ยท (โ„‘โ€˜๐ด)) = -(โ„‘โ€˜๐ด))
138137oveq2d 7428 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„‚ โ†’ (-1 ยท (-1 ยท (โ„‘โ€˜๐ด))) = (-1 ยท -(โ„‘โ€˜๐ด)))
139131, 136, 1383eqtr3rd 2780 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ (-1 ยท -(โ„‘โ€˜๐ด)) = (โ„‘โ€˜๐ด))
140139adantr 480 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‚ โˆง (โ„‘โ€˜๐ด) < 0) โ†’ (-1 ยท -(โ„‘โ€˜๐ด)) = (โ„‘โ€˜๐ด))
141135adantr 480 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‚ โˆง ยฌ (โ„‘โ€˜๐ด) < 0) โ†’ (1 ยท (โ„‘โ€˜๐ด)) = (โ„‘โ€˜๐ด))
142140, 141ifeqda 4565 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ if((โ„‘โ€˜๐ด) < 0, (-1 ยท -(โ„‘โ€˜๐ด)), (1 ยท (โ„‘โ€˜๐ด))) = (โ„‘โ€˜๐ด))
143127, 142eqtrid 2783 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด))) = (โ„‘โ€˜๐ด))
144143oveq1d 7427 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ ((if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด))) / 2) = ((โ„‘โ€˜๐ด) / 2))
145126, 144eqtr3d 2773 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2)) = ((โ„‘โ€˜๐ด) / 2))
146145oveq2d 7428 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (2 ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2))) = (2 ยท ((โ„‘โ€˜๐ด) / 2)))
147130, 57, 59divcan2d 11997 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (2 ยท ((โ„‘โ€˜๐ด) / 2)) = (โ„‘โ€˜๐ด))
148146, 147eqtrd 2771 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (2 ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2))) = (โ„‘โ€˜๐ด))
14967, 122, 1483eqtrd 2775 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) = (โ„‘โ€˜๐ด))
150149oveq2d 7428 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ (i ยท ((2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (i ยท (โ„‘โ€˜๐ด)))
15165, 66, 1503eqtr3d 2779 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) = (i ยท (โ„‘โ€˜๐ด)))
15263, 151oveq12d 7430 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ ((((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) + ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2)) + (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = ((โ„œโ€˜๐ด) + (i ยท (โ„‘โ€˜๐ด))))
1531resqcld 14095 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) โˆˆ โ„)
154153recnd 11247 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) โˆˆ โ„‚)
1552, 12mulcld 11239 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) โˆˆ โ„‚)
15657, 155mulcld 11239 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) โˆˆ โ„‚)
15712sqcld 14114 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2) โˆˆ โ„‚)
158154, 156, 157add32d 11446 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ ((((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) + (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) + ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2)) = ((((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) + ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2)) + (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))))
159 replim 15068 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ ๐ด = ((โ„œโ€˜๐ด) + (i ยท (โ„‘โ€˜๐ด))))
160152, 158, 1593eqtr4d 2781 . . . 4 (๐ด โˆˆ โ„‚ โ†’ ((((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) + (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) + ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2)) = ๐ด)
16116, 160eqtrd 2771 . . 3 (๐ด โˆˆ โ„‚ โ†’ (((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))โ†‘2) = ๐ด)
16220, 69sqrtge0d 15372 . . . 4 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)))
1631, 10crred 15183 . . . 4 (๐ด โˆˆ โ„‚ โ†’ (โ„œโ€˜((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) = (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)))
164162, 163breqtrrd 5177 . . 3 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (โ„œโ€˜((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))))
165 reim 15061 . . . . . . . . . 10 (((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) โˆˆ โ„‚ โ†’ (โ„œโ€˜((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) = (โ„‘โ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))))
16613, 165syl 17 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (โ„œโ€˜((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) = (โ„‘โ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))))
167166, 163eqtr3d 2773 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ (โ„‘โ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)))
168167eqeq1d 2733 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((โ„‘โ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = 0 โ†” (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) = 0))
169 cnsqrt00 15344 . . . . . . . 8 ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) = 0 โ†” (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = 0))
17021, 169syl 17 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) = 0 โ†” (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = 0))
171 half0 12444 . . . . . . . . 9 (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = 0 โ†” ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) = 0))
17255, 171syl 17 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = 0 โ†” ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) = 0))
17349, 50addcomd 11421 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) = ((โ„œโ€˜๐ด) + (absโ€˜๐ด)))
174173eqeq1d 2733 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) = 0 โ†” ((โ„œโ€˜๐ด) + (absโ€˜๐ด)) = 0))
175 addeq0 11642 . . . . . . . . 9 (((โ„œโ€˜๐ด) โˆˆ โ„‚ โˆง (absโ€˜๐ด) โˆˆ โ„‚) โ†’ (((โ„œโ€˜๐ด) + (absโ€˜๐ด)) = 0 โ†” (โ„œโ€˜๐ด) = -(absโ€˜๐ด)))
17650, 49, 175syl2anc 583 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ (((โ„œโ€˜๐ด) + (absโ€˜๐ด)) = 0 โ†” (โ„œโ€˜๐ด) = -(absโ€˜๐ด)))
177172, 174, 1763bitrd 304 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = 0 โ†” (โ„œโ€˜๐ด) = -(absโ€˜๐ด)))
178168, 170, 1773bitrd 304 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ ((โ„‘โ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = 0 โ†” (โ„œโ€˜๐ด) = -(absโ€˜๐ด)))
179 olc 865 . . . . . . . 8 ((โ„œโ€˜๐ด) = -(absโ€˜๐ด) โ†’ ((โ„œโ€˜๐ด) = (absโ€˜๐ด) โˆจ (โ„œโ€˜๐ด) = -(absโ€˜๐ด)))
180 eqcom 2738 . . . . . . . . . 10 (((โ„œโ€˜๐ด)โ†‘2) = ((absโ€˜๐ด)โ†‘2) โ†” ((absโ€˜๐ด)โ†‘2) = ((โ„œโ€˜๐ด)โ†‘2))
181180a1i 11 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (((โ„œโ€˜๐ด)โ†‘2) = ((absโ€˜๐ด)โ†‘2) โ†” ((absโ€˜๐ด)โ†‘2) = ((โ„œโ€˜๐ด)โ†‘2)))
182 sqeqor 14185 . . . . . . . . . 10 (((โ„œโ€˜๐ด) โˆˆ โ„‚ โˆง (absโ€˜๐ด) โˆˆ โ„‚) โ†’ (((โ„œโ€˜๐ด)โ†‘2) = ((absโ€˜๐ด)โ†‘2) โ†” ((โ„œโ€˜๐ด) = (absโ€˜๐ด) โˆจ (โ„œโ€˜๐ด) = -(absโ€˜๐ด))))
18350, 49, 182syl2anc 583 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (((โ„œโ€˜๐ด)โ†‘2) = ((absโ€˜๐ด)โ†‘2) โ†” ((โ„œโ€˜๐ด) = (absโ€˜๐ด) โˆจ (โ„œโ€˜๐ด) = -(absโ€˜๐ด))))
184103eqeq1d 2733 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด)โ†‘2) = ((โ„œโ€˜๐ด)โ†‘2) โ†” (((โ„œโ€˜๐ด)โ†‘2) + ((โ„‘โ€˜๐ด)โ†‘2)) = ((โ„œโ€˜๐ด)โ†‘2)))
185 addid0 11638 . . . . . . . . . . 11 ((((โ„œโ€˜๐ด)โ†‘2) โˆˆ โ„‚ โˆง ((โ„‘โ€˜๐ด)โ†‘2) โˆˆ โ„‚) โ†’ ((((โ„œโ€˜๐ด)โ†‘2) + ((โ„‘โ€˜๐ด)โ†‘2)) = ((โ„œโ€˜๐ด)โ†‘2) โ†” ((โ„‘โ€˜๐ด)โ†‘2) = 0))
18699, 102, 185syl2anc 583 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ ((((โ„œโ€˜๐ด)โ†‘2) + ((โ„‘โ€˜๐ด)โ†‘2)) = ((โ„œโ€˜๐ด)โ†‘2) โ†” ((โ„‘โ€˜๐ด)โ†‘2) = 0))
187 sqeq0 14090 . . . . . . . . . . 11 ((โ„‘โ€˜๐ด) โˆˆ โ„‚ โ†’ (((โ„‘โ€˜๐ด)โ†‘2) = 0 โ†” (โ„‘โ€˜๐ด) = 0))
188130, 187syl 17 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (((โ„‘โ€˜๐ด)โ†‘2) = 0 โ†” (โ„‘โ€˜๐ด) = 0))
189184, 186, 1883bitrd 304 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด)โ†‘2) = ((โ„œโ€˜๐ด)โ†‘2) โ†” (โ„‘โ€˜๐ด) = 0))
190181, 183, 1893bitr3d 308 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ (((โ„œโ€˜๐ด) = (absโ€˜๐ด) โˆจ (โ„œโ€˜๐ด) = -(absโ€˜๐ด)) โ†” (โ„‘โ€˜๐ด) = 0))
191179, 190imbitrid 243 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((โ„œโ€˜๐ด) = -(absโ€˜๐ด) โ†’ (โ„‘โ€˜๐ด) = 0))
192191ancld 550 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ ((โ„œโ€˜๐ด) = -(absโ€˜๐ด) โ†’ ((โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0)))
193178, 192sylbid 239 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ ((โ„‘โ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = 0 โ†’ ((โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0)))
194 simp2 1136 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„œโ€˜๐ด) = -(absโ€˜๐ด))
195194oveq2d 7428 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) = ((absโ€˜๐ด) + -(absโ€˜๐ด)))
196493ad2ant1 1132 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (absโ€˜๐ด) โˆˆ โ„‚)
197196negidd 11566 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((absโ€˜๐ด) + -(absโ€˜๐ด)) = 0)
198195, 197eqtrd 2771 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) = 0)
199198oveq1d 7427 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = (0 / 2))
200 2cn 12292 . . . . . . . . . . . . . . . . 17 2 โˆˆ โ„‚
201200, 58div0i 11953 . . . . . . . . . . . . . . . 16 (0 / 2) = 0
202199, 201eqtrdi 2787 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = 0)
203202fveq2d 6896 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) = (โˆšโ€˜0))
204 sqrt0 15193 . . . . . . . . . . . . . 14 (โˆšโ€˜0) = 0
205203, 204eqtrdi 2787 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) = 0)
206 simp3 1137 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„‘โ€˜๐ด) = 0)
207 0red 11222 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ 0 โˆˆ โ„)
208207ltnrd 11353 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ยฌ 0 < 0)
209206, 208eqnbrtrd 5167 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ยฌ (โ„‘โ€˜๐ด) < 0)
210209iffalsed 4540 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ if((โ„‘โ€˜๐ด) < 0, -1, 1) = 1)
211194oveq2d 7428 . . . . . . . . . . . . . . . . . . . 20 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) = ((absโ€˜๐ด) โˆ’ -(absโ€˜๐ด)))
21249, 49subnegd 11583 . . . . . . . . . . . . . . . . . . . . . 22 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) โˆ’ -(absโ€˜๐ด)) = ((absโ€˜๐ด) + (absโ€˜๐ด)))
213492timesd 12460 . . . . . . . . . . . . . . . . . . . . . 22 (๐ด โˆˆ โ„‚ โ†’ (2 ยท (absโ€˜๐ด)) = ((absโ€˜๐ด) + (absโ€˜๐ด)))
214212, 213eqtr4d 2774 . . . . . . . . . . . . . . . . . . . . 21 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) โˆ’ -(absโ€˜๐ด)) = (2 ยท (absโ€˜๐ด)))
2152143ad2ant1 1132 . . . . . . . . . . . . . . . . . . . 20 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((absโ€˜๐ด) โˆ’ -(absโ€˜๐ด)) = (2 ยท (absโ€˜๐ด)))
216211, 215eqtrd 2771 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) = (2 ยท (absโ€˜๐ด)))
217216oveq1d 7427 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2) = ((2 ยท (absโ€˜๐ด)) / 2))
21849, 57, 59divcan3d 12000 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„‚ โ†’ ((2 ยท (absโ€˜๐ด)) / 2) = (absโ€˜๐ด))
2192183ad2ant1 1132 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((2 ยท (absโ€˜๐ด)) / 2) = (absโ€˜๐ด))
220217, 219eqtrd 2771 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2) = (absโ€˜๐ด))
221220fveq2d 6896 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) = (โˆšโ€˜(absโ€˜๐ด)))
222210, 221oveq12d 7430 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))) = (1 ยท (โˆšโ€˜(absโ€˜๐ด))))
223 absge0 15239 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (absโ€˜๐ด))
22417, 223resqrtcld 15369 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(absโ€˜๐ด)) โˆˆ โ„)
225224recnd 11247 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(absโ€˜๐ด)) โˆˆ โ„‚)
226225mullidd 11237 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ (1 ยท (โˆšโ€˜(absโ€˜๐ด))) = (โˆšโ€˜(absโ€˜๐ด)))
2272263ad2ant1 1132 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (1 ยท (โˆšโ€˜(absโ€˜๐ด))) = (โˆšโ€˜(absโ€˜๐ด)))
228222, 227eqtrd 2771 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))) = (โˆšโ€˜(absโ€˜๐ด)))
229228oveq2d 7428 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) = (i ยท (โˆšโ€˜(absโ€˜๐ด))))
230205, 229oveq12d 7430 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (0 + (i ยท (โˆšโ€˜(absโ€˜๐ด)))))
2314, 225mulcld 11239 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (i ยท (โˆšโ€˜(absโ€˜๐ด))) โˆˆ โ„‚)
2322313ad2ant1 1132 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (i ยท (โˆšโ€˜(absโ€˜๐ด))) โˆˆ โ„‚)
233232addlidd 11420 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (0 + (i ยท (โˆšโ€˜(absโ€˜๐ด)))) = (i ยท (โˆšโ€˜(absโ€˜๐ด))))
234230, 233eqtrd 2771 . . . . . . . . . . 11 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (i ยท (โˆšโ€˜(absโ€˜๐ด))))
235234oveq2d 7428 . . . . . . . . . 10 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) = (i ยท (i ยท (โˆšโ€˜(absโ€˜๐ด)))))
236 ixi 11848 . . . . . . . . . . . . . 14 (i ยท i) = -1
237236a1i 11 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ (i ยท i) = -1)
238237oveq1d 7427 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ ((i ยท i) ยท (โˆšโ€˜(absโ€˜๐ด))) = (-1 ยท (โˆšโ€˜(absโ€˜๐ด))))
2394, 4, 225mulassd 11242 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ ((i ยท i) ยท (โˆšโ€˜(absโ€˜๐ด))) = (i ยท (i ยท (โˆšโ€˜(absโ€˜๐ด)))))
240225mulm1d 11671 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ (-1 ยท (โˆšโ€˜(absโ€˜๐ด))) = -(โˆšโ€˜(absโ€˜๐ด)))
241238, 239, 2403eqtr3d 2779 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ (i ยท (i ยท (โˆšโ€˜(absโ€˜๐ด)))) = -(โˆšโ€˜(absโ€˜๐ด)))
2422413ad2ant1 1132 . . . . . . . . . 10 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (i ยท (i ยท (โˆšโ€˜(absโ€˜๐ด)))) = -(โˆšโ€˜(absโ€˜๐ด)))
243235, 242eqtrd 2771 . . . . . . . . 9 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) = -(โˆšโ€˜(absโ€˜๐ด)))
244243fveq2d 6896 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„œโ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = (โ„œโ€˜-(โˆšโ€˜(absโ€˜๐ด))))
245224renegcld 11646 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ -(โˆšโ€˜(absโ€˜๐ด)) โˆˆ โ„)
246245rered 15176 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (โ„œโ€˜-(โˆšโ€˜(absโ€˜๐ด))) = -(โˆšโ€˜(absโ€˜๐ด)))
2472463ad2ant1 1132 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„œโ€˜-(โˆšโ€˜(absโ€˜๐ด))) = -(โˆšโ€˜(absโ€˜๐ด)))
248244, 247eqtrd 2771 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„œโ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = -(โˆšโ€˜(absโ€˜๐ด)))
24917, 223sqrtge0d 15372 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (โˆšโ€˜(absโ€˜๐ด)))
250224le0neg2d 11791 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (0 โ‰ค (โˆšโ€˜(absโ€˜๐ด)) โ†” -(โˆšโ€˜(absโ€˜๐ด)) โ‰ค 0))
251249, 250mpbid 231 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ -(โˆšโ€˜(absโ€˜๐ด)) โ‰ค 0)
2522513ad2ant1 1132 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ -(โˆšโ€˜(absโ€˜๐ด)) โ‰ค 0)
253248, 252eqbrtrd 5171 . . . . . 6 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„œโ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) โ‰ค 0)
2542533expib 1121 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ (((โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„œโ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) โ‰ค 0))
255193, 254syld 47 . . . 4 (๐ด โˆˆ โ„‚ โ†’ ((โ„‘โ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = 0 โ†’ (โ„œโ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) โ‰ค 0))
2564, 13mulcld 11239 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ (i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) โˆˆ โ„‚)
257256sqrtcvallem1 42685 . . . 4 (๐ด โˆˆ โ„‚ โ†’ (((โ„‘โ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = 0 โ†’ (โ„œโ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) โ‰ค 0) โ†” ยฌ (i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) โˆˆ โ„+))
258255, 257mpbid 231 . . 3 (๐ด โˆˆ โ„‚ โ†’ ยฌ (i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) โˆˆ โ„+)
25913, 14, 161, 164, 258eqsqrtd 15319 . 2 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (โˆšโ€˜๐ด))
260259eqcomd 2737 1 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜๐ด) = ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ wo 844   โˆง w3a 1086   = wceq 1540   โˆˆ wcel 2105   โ‰  wne 2939  ifcif 4529   class class class wbr 5149  โ€˜cfv 6544  (class class class)co 7412  โ„‚cc 11111  โ„cr 11112  0cc0 11113  1c1 11114  ici 11115   + caddc 11116   ยท cmul 11118   < clt 11253   โ‰ค cle 11254   โˆ’ cmin 11449  -cneg 11450   / cdiv 11876  2c2 12272  โ„+crp 12979  โ†‘cexp 14032  โ„œcre 15049  โ„‘cim 15050  โˆšcsqrt 15185  abscabs 15186
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728  ax-cnex 11169  ax-resscn 11170  ax-1cn 11171  ax-icn 11172  ax-addcl 11173  ax-addrcl 11174  ax-mulcl 11175  ax-mulrcl 11176  ax-mulcom 11177  ax-addass 11178  ax-mulass 11179  ax-distr 11180  ax-i2m1 11181  ax-1ne0 11182  ax-1rid 11183  ax-rnegex 11184  ax-rrecex 11185  ax-cnre 11186  ax-pre-lttri 11187  ax-pre-lttrn 11188  ax-pre-ltadd 11189  ax-pre-mulgt0 11190  ax-pre-sup 11191
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7859  df-2nd 7979  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-er 8706  df-en 8943  df-dom 8944  df-sdom 8945  df-sup 9440  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-div 11877  df-nn 12218  df-2 12280  df-3 12281  df-n0 12478  df-z 12564  df-uz 12828  df-rp 12980  df-seq 13972  df-exp 14033  df-cj 15051  df-re 15052  df-im 15053  df-sqrt 15187  df-abs 15188
This theorem is referenced by:  sqrtcval2  42696  resqrtval  42697  imsqrtval  42698
  Copyright terms: Public domain W3C validator