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 43136
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 15171 and crimi 15172. 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 43135 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) โˆˆ โ„)
21recnd 11272 . . . 4 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) โˆˆ โ„‚)
3 ax-icn 11197 . . . . . 6 i โˆˆ โ„‚
43a1i 11 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ i โˆˆ โ„‚)
5 neg1rr 12357 . . . . . . . . 9 -1 โˆˆ โ„
6 1re 11244 . . . . . . . . 9 1 โˆˆ โ„
75, 6ifcli 4576 . . . . . . . 8 if((โ„‘โ€˜๐ด) < 0, -1, 1) โˆˆ โ„
87a1i 11 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ if((โ„‘โ€˜๐ด) < 0, -1, 1) โˆˆ โ„)
9 sqrtcvallem3 43133 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) โˆˆ โ„)
108, 9remulcld 11274 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))) โˆˆ โ„)
1110recnd 11272 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))) โˆˆ โ„‚)
124, 11mulcld 11264 . . . 4 (๐ด โˆˆ โ„‚ โ†’ (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) โˆˆ โ„‚)
132, 12addcld 11263 . . 3 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) โˆˆ โ„‚)
14 id 22 . . 3 (๐ด โˆˆ โ„‚ โ†’ ๐ด โˆˆ โ„‚)
15 binom2 14212 . . . . 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 582 . . . 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 15257 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ (absโ€˜๐ด) โˆˆ โ„)
18 recl 15089 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ (โ„œโ€˜๐ด) โˆˆ โ„)
1917, 18readdcld 11273 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆˆ โ„)
2019rehalfcld 12489 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) โˆˆ โ„)
2120recnd 11272 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) โˆˆ โ„‚)
2221sqsqrtd 15418 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) = (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))
234, 11sqmuld 14154 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2) = ((iโ†‘2) ยท ((if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))โ†‘2)))
24 i2 14197 . . . . . . . . . . 11 (iโ†‘2) = -1
2524a1i 11 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (iโ†‘2) = -1)
268recnd 11272 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ if((โ„‘โ€˜๐ด) < 0, -1, 1) โˆˆ โ„‚)
279recnd 11272 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) โˆˆ โ„‚)
2826, 27sqmuld 14154 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ ((if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))โ†‘2) = ((if((โ„‘โ€˜๐ด) < 0, -1, 1)โ†‘2) ยท ((โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))โ†‘2)))
29 ovif 7516 . . . . . . . . . . . . . 14 (if((โ„‘โ€˜๐ด) < 0, -1, 1)โ†‘2) = if((โ„‘โ€˜๐ด) < 0, (-1โ†‘2), (1โ†‘2))
30 neg1sqe1 14191 . . . . . . . . . . . . . . 15 (-1โ†‘2) = 1
31 sq1 14190 . . . . . . . . . . . . . . 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 690 . . . . . . . . . . . . . 14 if((โ„‘โ€˜๐ด) < 0, (-1โ†‘2), (1โ†‘2)) = if((โ„‘โ€˜๐ด) < 0, 1, 1)
34 ifid 4569 . . . . . . . . . . . . . 14 if((โ„‘โ€˜๐ด) < 0, 1, 1) = 1
3529, 33, 343eqtri 2757 . . . . . . . . . . . . 13 (if((โ„‘โ€˜๐ด) < 0, -1, 1)โ†‘2) = 1
3635a1i 11 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1)โ†‘2) = 1)
3717, 18resubcld 11672 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) โˆˆ โ„)
3837rehalfcld 12489 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2) โˆˆ โ„)
3938recnd 11272 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2) โˆˆ โ„‚)
4039sqsqrtd 15418 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))โ†‘2) = (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))
4136, 40oveq12d 7435 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ ((if((โ„‘โ€˜๐ด) < 0, -1, 1)โ†‘2) ยท ((โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))โ†‘2)) = (1 ยท (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))
4239mullidd 11262 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ (1 ยท (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) = (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))
4328, 41, 423eqtrd 2769 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ ((if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))โ†‘2) = (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))
4425, 43oveq12d 7435 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ ((iโ†‘2) ยท ((if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))โ†‘2)) = (-1 ยท (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))
4539mulm1d 11696 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (-1 ยท (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) = -(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))
4623, 44, 453eqtrd 2769 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2) = -(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))
4722, 46oveq12d 7435 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ (((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) + ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2)) = ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) + -(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))
4821, 39negsubd 11607 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) + -(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) = ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) โˆ’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))
4917recnd 11272 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ (absโ€˜๐ด) โˆˆ โ„‚)
5018recnd 11272 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ (โ„œโ€˜๐ด) โˆˆ โ„‚)
5149, 50, 50pnncand 11640 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆ’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) = ((โ„œโ€˜๐ด) + (โ„œโ€˜๐ด)))
52502timesd 12485 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (2 ยท (โ„œโ€˜๐ด)) = ((โ„œโ€˜๐ด) + (โ„œโ€˜๐ด)))
5351, 52eqtr4d 2768 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆ’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) = (2 ยท (โ„œโ€˜๐ด)))
5453oveq1d 7432 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆ’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) / 2) = ((2 ยท (โ„œโ€˜๐ด)) / 2))
5519recnd 11272 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆˆ โ„‚)
5637recnd 11272 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) โˆˆ โ„‚)
57 2cnd 12320 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ 2 โˆˆ โ„‚)
58 2ne0 12346 . . . . . . . . . 10 2 โ‰  0
5958a1i 11 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ 2 โ‰  0)
6055, 56, 57, 59divsubdird 12059 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆ’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) / 2) = ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) โˆ’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))
6150, 57, 59divcan3d 12025 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((2 ยท (โ„œโ€˜๐ด)) / 2) = (โ„œโ€˜๐ด))
6254, 60, 613eqtr3d 2773 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) โˆ’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) = (โ„œโ€˜๐ด))
6347, 48, 623eqtrd 2769 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ (((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) + ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2)) = (โ„œโ€˜๐ด))
6457, 2mulcld 11264 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ (2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) โˆˆ โ„‚)
6564, 4, 11mul12d 11453 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (i ยท ((2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))
6657, 2, 12mulassd 11267 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))))
6757, 2, 11mulassd 11267 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ ((2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) = (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))
682, 26, 27mul12d 11453 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) = (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))
69 sqrtcvallem4 43134 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))
70 halfnneg2 12473 . . . . . . . . . . . . . . . . 17 (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆˆ โ„ โ†’ (0 โ‰ค ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โ†” 0 โ‰ค (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)))
7119, 70syl 17 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ (0 โ‰ค ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โ†” 0 โ‰ค (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)))
7269, 71mpbird 256 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค ((absโ€˜๐ด) + (โ„œโ€˜๐ด)))
73 2rp 13011 . . . . . . . . . . . . . . . 16 2 โˆˆ โ„+
7473a1i 11 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ 2 โˆˆ โ„+)
7519, 72, 74sqrtdivd 15402 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) = ((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) / (โˆšโ€˜2)))
76 sqrtcvallem2 43132 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))
77 halfnneg2 12473 . . . . . . . . . . . . . . . . 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 15402 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) = ((โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) / (โˆšโ€˜2)))
8175, 80oveq12d 7435 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))) = (((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) / (โˆšโ€˜2)) ยท ((โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) / (โˆšโ€˜2))))
8219, 72resqrtcld 15396 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) โˆˆ โ„)
8382recnd 11272 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) โˆˆ โ„‚)
84 2re 12316 . . . . . . . . . . . . . . . . 17 2 โˆˆ โ„
8584a1i 11 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ 2 โˆˆ โ„)
86 0le2 12344 . . . . . . . . . . . . . . . . 17 0 โ‰ค 2
8786a1i 11 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค 2)
8885, 87resqrtcld 15396 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜2) โˆˆ โ„)
8988recnd 11272 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜2) โˆˆ โ„‚)
9037, 79resqrtcld 15396 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) โˆˆ โ„)
9190recnd 11272 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) โˆˆ โ„‚)
92 sqrt00 15242 . . . . . . . . . . . . . . . . . 18 ((2 โˆˆ โ„ โˆง 0 โ‰ค 2) โ†’ ((โˆšโ€˜2) = 0 โ†” 2 = 0))
9384, 86, 92mp2an 690 . . . . . . . . . . . . . . . . 17 ((โˆšโ€˜2) = 0 โ†” 2 = 0)
9493necon3bii 2983 . . . . . . . . . . . . . . . 16 ((โˆšโ€˜2) โ‰  0 โ†” 2 โ‰  0)
9558, 94mpbir 230 . . . . . . . . . . . . . . 15 (โˆšโ€˜2) โ‰  0
9695a1i 11 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜2) โ‰  0)
9783, 89, 91, 89, 96, 96divmuldivd 12061 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ (((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) / (โˆšโ€˜2)) ยท ((โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) / (โˆšโ€˜2))) = (((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) ยท (โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))) / ((โˆšโ€˜2) ยท (โˆšโ€˜2))))
9818resqcld 14121 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„‚ โ†’ ((โ„œโ€˜๐ด)โ†‘2) โˆˆ โ„)
9998recnd 11272 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ ((โ„œโ€˜๐ด)โ†‘2) โˆˆ โ„‚)
100 imcl 15090 . . . . . . . . . . . . . . . . . . . 20 (๐ด โˆˆ โ„‚ โ†’ (โ„‘โ€˜๐ด) โˆˆ โ„)
101100resqcld 14121 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„‚ โ†’ ((โ„‘โ€˜๐ด)โ†‘2) โˆˆ โ„)
102101recnd 11272 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ ((โ„‘โ€˜๐ด)โ†‘2) โˆˆ โ„‚)
103 absvalsq2 15260 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด)โ†‘2) = (((โ„œโ€˜๐ด)โ†‘2) + ((โ„‘โ€˜๐ด)โ†‘2)))
10499, 102, 103mvrladdd 11657 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด)โ†‘2) โˆ’ ((โ„œโ€˜๐ด)โ†‘2)) = ((โ„‘โ€˜๐ด)โ†‘2))
105 subsq 14205 . . . . . . . . . . . . . . . . . 18 (((absโ€˜๐ด) โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) โˆˆ โ„‚) โ†’ (((absโ€˜๐ด)โ†‘2) โˆ’ ((โ„œโ€˜๐ด)โ†‘2)) = (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) ยท ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))))
10649, 50, 105syl2anc 582 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด)โ†‘2) โˆ’ ((โ„œโ€˜๐ด)โ†‘2)) = (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) ยท ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))))
107104, 106eqtr3d 2767 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ ((โ„‘โ€˜๐ด)โ†‘2) = (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) ยท ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))))
108107fveq2d 6898 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜((โ„‘โ€˜๐ด)โ†‘2)) = (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) ยท ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))))
109100absred 15395 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ (absโ€˜(โ„‘โ€˜๐ด)) = (โˆšโ€˜((โ„‘โ€˜๐ด)โ†‘2)))
110 reabsifneg 43127 . . . . . . . . . . . . . . . . 17 ((โ„‘โ€˜๐ด) โˆˆ โ„ โ†’ (absโ€˜(โ„‘โ€˜๐ด)) = if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)))
111100, 110syl 17 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ (absโ€˜(โ„‘โ€˜๐ด)) = if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)))
112109, 111eqtr3d 2767 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜((โ„‘โ€˜๐ด)โ†‘2)) = if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)))
11319, 72, 37, 79sqrtmuld 15403 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) ยท ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))) = ((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) ยท (โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))))
114108, 112, 1133eqtr3rd 2774 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) ยท (โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))) = if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)))
115 remsqsqrt 15235 . . . . . . . . . . . . . . . 16 ((2 โˆˆ โ„ โˆง 0 โ‰ค 2) โ†’ ((โˆšโ€˜2) ยท (โˆšโ€˜2)) = 2)
11684, 86, 115mp2an 690 . . . . . . . . . . . . . . 15 ((โˆšโ€˜2) ยท (โˆšโ€˜2)) = 2
117116a1i 11 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜2) ยท (โˆšโ€˜2)) = 2)
118114, 117oveq12d 7435 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ (((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) ยท (โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))) / ((โˆšโ€˜2) ยท (โˆšโ€˜2))) = (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2))
11981, 97, 1183eqtrd 2769 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))) = (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2))
120119oveq2d 7433 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) = (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2)))
12168, 120eqtrd 2765 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) = (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2)))
122121oveq2d 7433 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (2 ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2))))
123100renegcld 11671 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ -(โ„‘โ€˜๐ด) โˆˆ โ„)
124123, 100ifcld 4575 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) โˆˆ โ„)
125124recnd 11272 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) โˆˆ โ„‚)
12626, 125, 57, 59divassd 12055 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ ((if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด))) / 2) = (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2)))
127 ovif12 7518 . . . . . . . . . . . . . 14 (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด))) = if((โ„‘โ€˜๐ด) < 0, (-1 ยท -(โ„‘โ€˜๐ด)), (1 ยท (โ„‘โ€˜๐ด)))
1285a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„‚ โ†’ -1 โˆˆ โ„)
129128recnd 11272 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ -1 โˆˆ โ„‚)
130100recnd 11272 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ (โ„‘โ€˜๐ด) โˆˆ โ„‚)
131129, 129, 130mulassd 11267 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„‚ โ†’ ((-1 ยท -1) ยท (โ„‘โ€˜๐ด)) = (-1 ยท (-1 ยท (โ„‘โ€˜๐ด))))
132 neg1mulneg1e1 12455 . . . . . . . . . . . . . . . . . . . 20 (-1 ยท -1) = 1
133132a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„‚ โ†’ (-1 ยท -1) = 1)
134133oveq1d 7432 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ ((-1 ยท -1) ยท (โ„‘โ€˜๐ด)) = (1 ยท (โ„‘โ€˜๐ด)))
135130mullidd 11262 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ (1 ยท (โ„‘โ€˜๐ด)) = (โ„‘โ€˜๐ด))
136134, 135eqtrd 2765 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„‚ โ†’ ((-1 ยท -1) ยท (โ„‘โ€˜๐ด)) = (โ„‘โ€˜๐ด))
137130mulm1d 11696 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ (-1 ยท (โ„‘โ€˜๐ด)) = -(โ„‘โ€˜๐ด))
138137oveq2d 7433 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„‚ โ†’ (-1 ยท (-1 ยท (โ„‘โ€˜๐ด))) = (-1 ยท -(โ„‘โ€˜๐ด)))
139131, 136, 1383eqtr3rd 2774 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ (-1 ยท -(โ„‘โ€˜๐ด)) = (โ„‘โ€˜๐ด))
140139adantr 479 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‚ โˆง (โ„‘โ€˜๐ด) < 0) โ†’ (-1 ยท -(โ„‘โ€˜๐ด)) = (โ„‘โ€˜๐ด))
141135adantr 479 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‚ โˆง ยฌ (โ„‘โ€˜๐ด) < 0) โ†’ (1 ยท (โ„‘โ€˜๐ด)) = (โ„‘โ€˜๐ด))
142140, 141ifeqda 4565 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ if((โ„‘โ€˜๐ด) < 0, (-1 ยท -(โ„‘โ€˜๐ด)), (1 ยท (โ„‘โ€˜๐ด))) = (โ„‘โ€˜๐ด))
143127, 142eqtrid 2777 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด))) = (โ„‘โ€˜๐ด))
144143oveq1d 7432 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ ((if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด))) / 2) = ((โ„‘โ€˜๐ด) / 2))
145126, 144eqtr3d 2767 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2)) = ((โ„‘โ€˜๐ด) / 2))
146145oveq2d 7433 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (2 ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2))) = (2 ยท ((โ„‘โ€˜๐ด) / 2)))
147130, 57, 59divcan2d 12022 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (2 ยท ((โ„‘โ€˜๐ด) / 2)) = (โ„‘โ€˜๐ด))
148146, 147eqtrd 2765 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (2 ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2))) = (โ„‘โ€˜๐ด))
14967, 122, 1483eqtrd 2769 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) = (โ„‘โ€˜๐ด))
150149oveq2d 7433 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ (i ยท ((2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (i ยท (โ„‘โ€˜๐ด)))
15165, 66, 1503eqtr3d 2773 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) = (i ยท (โ„‘โ€˜๐ด)))
15263, 151oveq12d 7435 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ ((((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) + ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2)) + (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = ((โ„œโ€˜๐ด) + (i ยท (โ„‘โ€˜๐ด))))
1531resqcld 14121 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) โˆˆ โ„)
154153recnd 11272 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) โˆˆ โ„‚)
1552, 12mulcld 11264 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) โˆˆ โ„‚)
15657, 155mulcld 11264 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) โˆˆ โ„‚)
15712sqcld 14140 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2) โˆˆ โ„‚)
158154, 156, 157add32d 11471 . . . . 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 15095 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ ๐ด = ((โ„œโ€˜๐ด) + (i ยท (โ„‘โ€˜๐ด))))
160152, 158, 1593eqtr4d 2775 . . . 4 (๐ด โˆˆ โ„‚ โ†’ ((((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) + (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) + ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2)) = ๐ด)
16116, 160eqtrd 2765 . . 3 (๐ด โˆˆ โ„‚ โ†’ (((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))โ†‘2) = ๐ด)
16220, 69sqrtge0d 15399 . . . 4 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)))
1631, 10crred 15210 . . . 4 (๐ด โˆˆ โ„‚ โ†’ (โ„œโ€˜((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) = (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)))
164162, 163breqtrrd 5176 . . 3 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (โ„œโ€˜((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))))
165 reim 15088 . . . . . . . . . 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 2767 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ (โ„‘โ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)))
168167eqeq1d 2727 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((โ„‘โ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = 0 โ†” (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) = 0))
169 cnsqrt00 15371 . . . . . . . 8 ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) = 0 โ†” (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = 0))
17021, 169syl 17 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) = 0 โ†” (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = 0))
171 half0 12469 . . . . . . . . 9 (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = 0 โ†” ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) = 0))
17255, 171syl 17 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = 0 โ†” ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) = 0))
17349, 50addcomd 11446 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) = ((โ„œโ€˜๐ด) + (absโ€˜๐ด)))
174173eqeq1d 2727 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) = 0 โ†” ((โ„œโ€˜๐ด) + (absโ€˜๐ด)) = 0))
175 addeq0 11667 . . . . . . . . 9 (((โ„œโ€˜๐ด) โˆˆ โ„‚ โˆง (absโ€˜๐ด) โˆˆ โ„‚) โ†’ (((โ„œโ€˜๐ด) + (absโ€˜๐ด)) = 0 โ†” (โ„œโ€˜๐ด) = -(absโ€˜๐ด)))
17650, 49, 175syl2anc 582 . . . . . . . 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 866 . . . . . . . 8 ((โ„œโ€˜๐ด) = -(absโ€˜๐ด) โ†’ ((โ„œโ€˜๐ด) = (absโ€˜๐ด) โˆจ (โ„œโ€˜๐ด) = -(absโ€˜๐ด)))
180 eqcom 2732 . . . . . . . . . 10 (((โ„œโ€˜๐ด)โ†‘2) = ((absโ€˜๐ด)โ†‘2) โ†” ((absโ€˜๐ด)โ†‘2) = ((โ„œโ€˜๐ด)โ†‘2))
181180a1i 11 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (((โ„œโ€˜๐ด)โ†‘2) = ((absโ€˜๐ด)โ†‘2) โ†” ((absโ€˜๐ด)โ†‘2) = ((โ„œโ€˜๐ด)โ†‘2)))
182 sqeqor 14211 . . . . . . . . . 10 (((โ„œโ€˜๐ด) โˆˆ โ„‚ โˆง (absโ€˜๐ด) โˆˆ โ„‚) โ†’ (((โ„œโ€˜๐ด)โ†‘2) = ((absโ€˜๐ด)โ†‘2) โ†” ((โ„œโ€˜๐ด) = (absโ€˜๐ด) โˆจ (โ„œโ€˜๐ด) = -(absโ€˜๐ด))))
18350, 49, 182syl2anc 582 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (((โ„œโ€˜๐ด)โ†‘2) = ((absโ€˜๐ด)โ†‘2) โ†” ((โ„œโ€˜๐ด) = (absโ€˜๐ด) โˆจ (โ„œโ€˜๐ด) = -(absโ€˜๐ด))))
184103eqeq1d 2727 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด)โ†‘2) = ((โ„œโ€˜๐ด)โ†‘2) โ†” (((โ„œโ€˜๐ด)โ†‘2) + ((โ„‘โ€˜๐ด)โ†‘2)) = ((โ„œโ€˜๐ด)โ†‘2)))
185 addid0 11663 . . . . . . . . . . 11 ((((โ„œโ€˜๐ด)โ†‘2) โˆˆ โ„‚ โˆง ((โ„‘โ€˜๐ด)โ†‘2) โˆˆ โ„‚) โ†’ ((((โ„œโ€˜๐ด)โ†‘2) + ((โ„‘โ€˜๐ด)โ†‘2)) = ((โ„œโ€˜๐ด)โ†‘2) โ†” ((โ„‘โ€˜๐ด)โ†‘2) = 0))
18699, 102, 185syl2anc 582 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ ((((โ„œโ€˜๐ด)โ†‘2) + ((โ„‘โ€˜๐ด)โ†‘2)) = ((โ„œโ€˜๐ด)โ†‘2) โ†” ((โ„‘โ€˜๐ด)โ†‘2) = 0))
187 sqeq0 14116 . . . . . . . . . . 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 549 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ ((โ„œโ€˜๐ด) = -(absโ€˜๐ด) โ†’ ((โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0)))
193178, 192sylbid 239 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ ((โ„‘โ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = 0 โ†’ ((โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0)))
194 simp2 1134 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„œโ€˜๐ด) = -(absโ€˜๐ด))
195194oveq2d 7433 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) = ((absโ€˜๐ด) + -(absโ€˜๐ด)))
196493ad2ant1 1130 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (absโ€˜๐ด) โˆˆ โ„‚)
197196negidd 11591 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((absโ€˜๐ด) + -(absโ€˜๐ด)) = 0)
198195, 197eqtrd 2765 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) = 0)
199198oveq1d 7432 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = (0 / 2))
200 2cn 12317 . . . . . . . . . . . . . . . . 17 2 โˆˆ โ„‚
201200, 58div0i 11978 . . . . . . . . . . . . . . . 16 (0 / 2) = 0
202199, 201eqtrdi 2781 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = 0)
203202fveq2d 6898 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) = (โˆšโ€˜0))
204 sqrt0 15220 . . . . . . . . . . . . . 14 (โˆšโ€˜0) = 0
205203, 204eqtrdi 2781 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) = 0)
206 simp3 1135 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„‘โ€˜๐ด) = 0)
207 0red 11247 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ 0 โˆˆ โ„)
208207ltnrd 11378 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ยฌ 0 < 0)
209206, 208eqnbrtrd 5166 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ยฌ (โ„‘โ€˜๐ด) < 0)
210209iffalsed 4540 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ if((โ„‘โ€˜๐ด) < 0, -1, 1) = 1)
211194oveq2d 7433 . . . . . . . . . . . . . . . . . . . 20 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) = ((absโ€˜๐ด) โˆ’ -(absโ€˜๐ด)))
21249, 49subnegd 11608 . . . . . . . . . . . . . . . . . . . . . 22 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) โˆ’ -(absโ€˜๐ด)) = ((absโ€˜๐ด) + (absโ€˜๐ด)))
213492timesd 12485 . . . . . . . . . . . . . . . . . . . . . 22 (๐ด โˆˆ โ„‚ โ†’ (2 ยท (absโ€˜๐ด)) = ((absโ€˜๐ด) + (absโ€˜๐ด)))
214212, 213eqtr4d 2768 . . . . . . . . . . . . . . . . . . . . 21 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) โˆ’ -(absโ€˜๐ด)) = (2 ยท (absโ€˜๐ด)))
2152143ad2ant1 1130 . . . . . . . . . . . . . . . . . . . 20 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((absโ€˜๐ด) โˆ’ -(absโ€˜๐ด)) = (2 ยท (absโ€˜๐ด)))
216211, 215eqtrd 2765 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) = (2 ยท (absโ€˜๐ด)))
217216oveq1d 7432 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2) = ((2 ยท (absโ€˜๐ด)) / 2))
21849, 57, 59divcan3d 12025 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„‚ โ†’ ((2 ยท (absโ€˜๐ด)) / 2) = (absโ€˜๐ด))
2192183ad2ant1 1130 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((2 ยท (absโ€˜๐ด)) / 2) = (absโ€˜๐ด))
220217, 219eqtrd 2765 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2) = (absโ€˜๐ด))
221220fveq2d 6898 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) = (โˆšโ€˜(absโ€˜๐ด)))
222210, 221oveq12d 7435 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))) = (1 ยท (โˆšโ€˜(absโ€˜๐ด))))
223 absge0 15266 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (absโ€˜๐ด))
22417, 223resqrtcld 15396 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(absโ€˜๐ด)) โˆˆ โ„)
225224recnd 11272 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(absโ€˜๐ด)) โˆˆ โ„‚)
226225mullidd 11262 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ (1 ยท (โˆšโ€˜(absโ€˜๐ด))) = (โˆšโ€˜(absโ€˜๐ด)))
2272263ad2ant1 1130 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (1 ยท (โˆšโ€˜(absโ€˜๐ด))) = (โˆšโ€˜(absโ€˜๐ด)))
228222, 227eqtrd 2765 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))) = (โˆšโ€˜(absโ€˜๐ด)))
229228oveq2d 7433 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) = (i ยท (โˆšโ€˜(absโ€˜๐ด))))
230205, 229oveq12d 7435 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (0 + (i ยท (โˆšโ€˜(absโ€˜๐ด)))))
2314, 225mulcld 11264 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (i ยท (โˆšโ€˜(absโ€˜๐ด))) โˆˆ โ„‚)
2322313ad2ant1 1130 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (i ยท (โˆšโ€˜(absโ€˜๐ด))) โˆˆ โ„‚)
233232addlidd 11445 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (0 + (i ยท (โˆšโ€˜(absโ€˜๐ด)))) = (i ยท (โˆšโ€˜(absโ€˜๐ด))))
234230, 233eqtrd 2765 . . . . . . . . . . 11 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (i ยท (โˆšโ€˜(absโ€˜๐ด))))
235234oveq2d 7433 . . . . . . . . . 10 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) = (i ยท (i ยท (โˆšโ€˜(absโ€˜๐ด)))))
236 ixi 11873 . . . . . . . . . . . . . 14 (i ยท i) = -1
237236a1i 11 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ (i ยท i) = -1)
238237oveq1d 7432 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ ((i ยท i) ยท (โˆšโ€˜(absโ€˜๐ด))) = (-1 ยท (โˆšโ€˜(absโ€˜๐ด))))
2394, 4, 225mulassd 11267 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ ((i ยท i) ยท (โˆšโ€˜(absโ€˜๐ด))) = (i ยท (i ยท (โˆšโ€˜(absโ€˜๐ด)))))
240225mulm1d 11696 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ (-1 ยท (โˆšโ€˜(absโ€˜๐ด))) = -(โˆšโ€˜(absโ€˜๐ด)))
241238, 239, 2403eqtr3d 2773 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ (i ยท (i ยท (โˆšโ€˜(absโ€˜๐ด)))) = -(โˆšโ€˜(absโ€˜๐ด)))
2422413ad2ant1 1130 . . . . . . . . . 10 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (i ยท (i ยท (โˆšโ€˜(absโ€˜๐ด)))) = -(โˆšโ€˜(absโ€˜๐ด)))
243235, 242eqtrd 2765 . . . . . . . . 9 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) = -(โˆšโ€˜(absโ€˜๐ด)))
244243fveq2d 6898 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„œโ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = (โ„œโ€˜-(โˆšโ€˜(absโ€˜๐ด))))
245224renegcld 11671 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ -(โˆšโ€˜(absโ€˜๐ด)) โˆˆ โ„)
246245rered 15203 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (โ„œโ€˜-(โˆšโ€˜(absโ€˜๐ด))) = -(โˆšโ€˜(absโ€˜๐ด)))
2472463ad2ant1 1130 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„œโ€˜-(โˆšโ€˜(absโ€˜๐ด))) = -(โˆšโ€˜(absโ€˜๐ด)))
248244, 247eqtrd 2765 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„œโ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = -(โˆšโ€˜(absโ€˜๐ด)))
24917, 223sqrtge0d 15399 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (โˆšโ€˜(absโ€˜๐ด)))
250224le0neg2d 11816 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (0 โ‰ค (โˆšโ€˜(absโ€˜๐ด)) โ†” -(โˆšโ€˜(absโ€˜๐ด)) โ‰ค 0))
251249, 250mpbid 231 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ -(โˆšโ€˜(absโ€˜๐ด)) โ‰ค 0)
2522513ad2ant1 1130 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ -(โˆšโ€˜(absโ€˜๐ด)) โ‰ค 0)
253248, 252eqbrtrd 5170 . . . . . 6 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„œโ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) โ‰ค 0)
2542533expib 1119 . . . . 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 11264 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ (i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) โˆˆ โ„‚)
257256sqrtcvallem1 43126 . . . 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 15346 . 2 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (โˆšโ€˜๐ด))
260259eqcomd 2731 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 394   โˆจ wo 845   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098   โ‰  wne 2930  ifcif 4529   class class class wbr 5148  โ€˜cfv 6547  (class class class)co 7417  โ„‚cc 11136  โ„cr 11137  0cc0 11138  1c1 11139  ici 11140   + caddc 11141   ยท cmul 11143   < clt 11278   โ‰ค cle 11279   โˆ’ cmin 11474  -cneg 11475   / cdiv 11901  2c2 12297  โ„+crp 13006  โ†‘cexp 14058  โ„œcre 15076  โ„‘cim 15077  โˆšcsqrt 15212  abscabs 15213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5299  ax-nul 5306  ax-pow 5364  ax-pr 5428  ax-un 7739  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215  ax-pre-sup 11216
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3965  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  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 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6499  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-riota 7373  df-ov 7420  df-oprab 7421  df-mpo 7422  df-om 7870  df-2nd 7993  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-er 8723  df-en 8963  df-dom 8964  df-sdom 8965  df-sup 9465  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-div 11902  df-nn 12243  df-2 12305  df-3 12306  df-n0 12503  df-z 12589  df-uz 12853  df-rp 13007  df-seq 13999  df-exp 14059  df-cj 15078  df-re 15079  df-im 15080  df-sqrt 15214  df-abs 15215
This theorem is referenced by:  sqrtcval2  43137  resqrtval  43138  imsqrtval  43139
  Copyright terms: Public domain W3C validator