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 42694
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 15143 and crimi 15144. 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 42693 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) โˆˆ โ„)
21recnd 11246 . . . 4 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) โˆˆ โ„‚)
3 ax-icn 11171 . . . . . 6 i โˆˆ โ„‚
43a1i 11 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ i โˆˆ โ„‚)
5 neg1rr 12331 . . . . . . . . 9 -1 โˆˆ โ„
6 1re 11218 . . . . . . . . 9 1 โˆˆ โ„
75, 6ifcli 4574 . . . . . . . 8 if((โ„‘โ€˜๐ด) < 0, -1, 1) โˆˆ โ„
87a1i 11 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ if((โ„‘โ€˜๐ด) < 0, -1, 1) โˆˆ โ„)
9 sqrtcvallem3 42691 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) โˆˆ โ„)
108, 9remulcld 11248 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))) โˆˆ โ„)
1110recnd 11246 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))) โˆˆ โ„‚)
124, 11mulcld 11238 . . . 4 (๐ด โˆˆ โ„‚ โ†’ (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) โˆˆ โ„‚)
132, 12addcld 11237 . . 3 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) โˆˆ โ„‚)
14 id 22 . . 3 (๐ด โˆˆ โ„‚ โ†’ ๐ด โˆˆ โ„‚)
15 binom2 14185 . . . . 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 15229 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ (absโ€˜๐ด) โˆˆ โ„)
18 recl 15061 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ (โ„œโ€˜๐ด) โˆˆ โ„)
1917, 18readdcld 11247 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆˆ โ„)
2019rehalfcld 12463 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) โˆˆ โ„)
2120recnd 11246 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) โˆˆ โ„‚)
2221sqsqrtd 15390 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) = (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))
234, 11sqmuld 14127 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2) = ((iโ†‘2) ยท ((if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))โ†‘2)))
24 i2 14170 . . . . . . . . . . 11 (iโ†‘2) = -1
2524a1i 11 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (iโ†‘2) = -1)
268recnd 11246 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ if((โ„‘โ€˜๐ด) < 0, -1, 1) โˆˆ โ„‚)
279recnd 11246 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) โˆˆ โ„‚)
2826, 27sqmuld 14127 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ ((if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))โ†‘2) = ((if((โ„‘โ€˜๐ด) < 0, -1, 1)โ†‘2) ยท ((โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))โ†‘2)))
29 ovif 7508 . . . . . . . . . . . . . 14 (if((โ„‘โ€˜๐ด) < 0, -1, 1)โ†‘2) = if((โ„‘โ€˜๐ด) < 0, (-1โ†‘2), (1โ†‘2))
30 neg1sqe1 14164 . . . . . . . . . . . . . . 15 (-1โ†‘2) = 1
31 sq1 14163 . . . . . . . . . . . . . . 15 (1โ†‘2) = 1
32 ifeq12 4545 . . . . . . . . . . . . . . 15 (((-1โ†‘2) = 1 โˆง (1โ†‘2) = 1) โ†’ if((โ„‘โ€˜๐ด) < 0, (-1โ†‘2), (1โ†‘2)) = if((โ„‘โ€˜๐ด) < 0, 1, 1))
3330, 31, 32mp2an 688 . . . . . . . . . . . . . 14 if((โ„‘โ€˜๐ด) < 0, (-1โ†‘2), (1โ†‘2)) = if((โ„‘โ€˜๐ด) < 0, 1, 1)
34 ifid 4567 . . . . . . . . . . . . . 14 if((โ„‘โ€˜๐ด) < 0, 1, 1) = 1
3529, 33, 343eqtri 2762 . . . . . . . . . . . . 13 (if((โ„‘โ€˜๐ด) < 0, -1, 1)โ†‘2) = 1
3635a1i 11 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1)โ†‘2) = 1)
3717, 18resubcld 11646 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) โˆˆ โ„)
3837rehalfcld 12463 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2) โˆˆ โ„)
3938recnd 11246 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2) โˆˆ โ„‚)
4039sqsqrtd 15390 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))โ†‘2) = (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))
4136, 40oveq12d 7429 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ ((if((โ„‘โ€˜๐ด) < 0, -1, 1)โ†‘2) ยท ((โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))โ†‘2)) = (1 ยท (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))
4239mullidd 11236 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ (1 ยท (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) = (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))
4328, 41, 423eqtrd 2774 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ ((if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))โ†‘2) = (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))
4425, 43oveq12d 7429 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ ((iโ†‘2) ยท ((if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))โ†‘2)) = (-1 ยท (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))
4539mulm1d 11670 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (-1 ยท (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) = -(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))
4623, 44, 453eqtrd 2774 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2) = -(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))
4722, 46oveq12d 7429 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ (((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) + ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2)) = ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) + -(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))
4821, 39negsubd 11581 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) + -(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) = ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) โˆ’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))
4917recnd 11246 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ (absโ€˜๐ด) โˆˆ โ„‚)
5018recnd 11246 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ (โ„œโ€˜๐ด) โˆˆ โ„‚)
5149, 50, 50pnncand 11614 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆ’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) = ((โ„œโ€˜๐ด) + (โ„œโ€˜๐ด)))
52502timesd 12459 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (2 ยท (โ„œโ€˜๐ด)) = ((โ„œโ€˜๐ด) + (โ„œโ€˜๐ด)))
5351, 52eqtr4d 2773 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆ’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) = (2 ยท (โ„œโ€˜๐ด)))
5453oveq1d 7426 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆ’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) / 2) = ((2 ยท (โ„œโ€˜๐ด)) / 2))
5519recnd 11246 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆˆ โ„‚)
5637recnd 11246 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) โˆˆ โ„‚)
57 2cnd 12294 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ 2 โˆˆ โ„‚)
58 2ne0 12320 . . . . . . . . . 10 2 โ‰  0
5958a1i 11 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ 2 โ‰  0)
6055, 56, 57, 59divsubdird 12033 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆ’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) / 2) = ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) โˆ’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))
6150, 57, 59divcan3d 11999 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((2 ยท (โ„œโ€˜๐ด)) / 2) = (โ„œโ€˜๐ด))
6254, 60, 613eqtr3d 2778 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) โˆ’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) = (โ„œโ€˜๐ด))
6347, 48, 623eqtrd 2774 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ (((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) + ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2)) = (โ„œโ€˜๐ด))
6457, 2mulcld 11238 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ (2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) โˆˆ โ„‚)
6564, 4, 11mul12d 11427 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (i ยท ((2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))
6657, 2, 12mulassd 11241 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))))
6757, 2, 11mulassd 11241 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ ((2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) = (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))
682, 26, 27mul12d 11427 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) = (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))
69 sqrtcvallem4 42692 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))
70 halfnneg2 12447 . . . . . . . . . . . . . . . . 17 (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆˆ โ„ โ†’ (0 โ‰ค ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โ†” 0 โ‰ค (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)))
7119, 70syl 17 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ (0 โ‰ค ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โ†” 0 โ‰ค (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)))
7269, 71mpbird 256 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค ((absโ€˜๐ด) + (โ„œโ€˜๐ด)))
73 2rp 12983 . . . . . . . . . . . . . . . 16 2 โˆˆ โ„+
7473a1i 11 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ 2 โˆˆ โ„+)
7519, 72, 74sqrtdivd 15374 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) = ((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) / (โˆšโ€˜2)))
76 sqrtcvallem2 42690 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))
77 halfnneg2 12447 . . . . . . . . . . . . . . . . 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 15374 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) = ((โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) / (โˆšโ€˜2)))
8175, 80oveq12d 7429 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))) = (((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) / (โˆšโ€˜2)) ยท ((โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) / (โˆšโ€˜2))))
8219, 72resqrtcld 15368 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) โˆˆ โ„)
8382recnd 11246 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) โˆˆ โ„‚)
84 2re 12290 . . . . . . . . . . . . . . . . 17 2 โˆˆ โ„
8584a1i 11 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ 2 โˆˆ โ„)
86 0le2 12318 . . . . . . . . . . . . . . . . 17 0 โ‰ค 2
8786a1i 11 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค 2)
8885, 87resqrtcld 15368 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜2) โˆˆ โ„)
8988recnd 11246 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜2) โˆˆ โ„‚)
9037, 79resqrtcld 15368 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) โˆˆ โ„)
9190recnd 11246 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) โˆˆ โ„‚)
92 sqrt00 15214 . . . . . . . . . . . . . . . . . 18 ((2 โˆˆ โ„ โˆง 0 โ‰ค 2) โ†’ ((โˆšโ€˜2) = 0 โ†” 2 = 0))
9384, 86, 92mp2an 688 . . . . . . . . . . . . . . . . 17 ((โˆšโ€˜2) = 0 โ†” 2 = 0)
9493necon3bii 2991 . . . . . . . . . . . . . . . 16 ((โˆšโ€˜2) โ‰  0 โ†” 2 โ‰  0)
9558, 94mpbir 230 . . . . . . . . . . . . . . 15 (โˆšโ€˜2) โ‰  0
9695a1i 11 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜2) โ‰  0)
9783, 89, 91, 89, 96, 96divmuldivd 12035 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ (((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) / (โˆšโ€˜2)) ยท ((โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))) / (โˆšโ€˜2))) = (((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) ยท (โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))) / ((โˆšโ€˜2) ยท (โˆšโ€˜2))))
9818resqcld 14094 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„‚ โ†’ ((โ„œโ€˜๐ด)โ†‘2) โˆˆ โ„)
9998recnd 11246 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ ((โ„œโ€˜๐ด)โ†‘2) โˆˆ โ„‚)
100 imcl 15062 . . . . . . . . . . . . . . . . . . . 20 (๐ด โˆˆ โ„‚ โ†’ (โ„‘โ€˜๐ด) โˆˆ โ„)
101100resqcld 14094 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„‚ โ†’ ((โ„‘โ€˜๐ด)โ†‘2) โˆˆ โ„)
102101recnd 11246 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ ((โ„‘โ€˜๐ด)โ†‘2) โˆˆ โ„‚)
103 absvalsq2 15232 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด)โ†‘2) = (((โ„œโ€˜๐ด)โ†‘2) + ((โ„‘โ€˜๐ด)โ†‘2)))
10499, 102, 103mvrladdd 11631 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด)โ†‘2) โˆ’ ((โ„œโ€˜๐ด)โ†‘2)) = ((โ„‘โ€˜๐ด)โ†‘2))
105 subsq 14178 . . . . . . . . . . . . . . . . . 18 (((absโ€˜๐ด) โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) โˆˆ โ„‚) โ†’ (((absโ€˜๐ด)โ†‘2) โˆ’ ((โ„œโ€˜๐ด)โ†‘2)) = (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) ยท ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))))
10649, 50, 105syl2anc 582 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด)โ†‘2) โˆ’ ((โ„œโ€˜๐ด)โ†‘2)) = (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) ยท ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))))
107104, 106eqtr3d 2772 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ ((โ„‘โ€˜๐ด)โ†‘2) = (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) ยท ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด))))
108107fveq2d 6894 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜((โ„‘โ€˜๐ด)โ†‘2)) = (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) ยท ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))))
109100absred 15367 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ (absโ€˜(โ„‘โ€˜๐ด)) = (โˆšโ€˜((โ„‘โ€˜๐ด)โ†‘2)))
110 reabsifneg 42685 . . . . . . . . . . . . . . . . 17 ((โ„‘โ€˜๐ด) โˆˆ โ„ โ†’ (absโ€˜(โ„‘โ€˜๐ด)) = if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)))
111100, 110syl 17 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ (absโ€˜(โ„‘โ€˜๐ด)) = if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)))
112109, 111eqtr3d 2772 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜((โ„‘โ€˜๐ด)โ†‘2)) = if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)))
11319, 72, 37, 79sqrtmuld 15375 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) ยท ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))) = ((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) ยท (โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))))
114108, 112, 1133eqtr3rd 2779 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) ยท (โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))) = if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)))
115 remsqsqrt 15207 . . . . . . . . . . . . . . . 16 ((2 โˆˆ โ„ โˆง 0 โ‰ค 2) โ†’ ((โˆšโ€˜2) ยท (โˆšโ€˜2)) = 2)
11684, 86, 115mp2an 688 . . . . . . . . . . . . . . 15 ((โˆšโ€˜2) ยท (โˆšโ€˜2)) = 2
117116a1i 11 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜2) ยท (โˆšโ€˜2)) = 2)
118114, 117oveq12d 7429 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ (((โˆšโ€˜((absโ€˜๐ด) + (โ„œโ€˜๐ด))) ยท (โˆšโ€˜((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)))) / ((โˆšโ€˜2) ยท (โˆšโ€˜2))) = (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2))
11981, 97, 1183eqtrd 2774 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))) = (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2))
120119oveq2d 7427 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) = (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2)))
12168, 120eqtrd 2770 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) = (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2)))
122121oveq2d 7427 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (2 ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2))))
123100renegcld 11645 . . . . . . . . . . . . . . 15 (๐ด โˆˆ โ„‚ โ†’ -(โ„‘โ€˜๐ด) โˆˆ โ„)
124123, 100ifcld 4573 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) โˆˆ โ„)
125124recnd 11246 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) โˆˆ โ„‚)
12626, 125, 57, 59divassd 12029 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ ((if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด))) / 2) = (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2)))
127 ovif12 7510 . . . . . . . . . . . . . 14 (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด))) = if((โ„‘โ€˜๐ด) < 0, (-1 ยท -(โ„‘โ€˜๐ด)), (1 ยท (โ„‘โ€˜๐ด)))
1285a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„‚ โ†’ -1 โˆˆ โ„)
129128recnd 11246 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ -1 โˆˆ โ„‚)
130100recnd 11246 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ (โ„‘โ€˜๐ด) โˆˆ โ„‚)
131129, 129, 130mulassd 11241 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„‚ โ†’ ((-1 ยท -1) ยท (โ„‘โ€˜๐ด)) = (-1 ยท (-1 ยท (โ„‘โ€˜๐ด))))
132 neg1mulneg1e1 12429 . . . . . . . . . . . . . . . . . . . 20 (-1 ยท -1) = 1
133132a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„‚ โ†’ (-1 ยท -1) = 1)
134133oveq1d 7426 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ ((-1 ยท -1) ยท (โ„‘โ€˜๐ด)) = (1 ยท (โ„‘โ€˜๐ด)))
135130mullidd 11236 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ (1 ยท (โ„‘โ€˜๐ด)) = (โ„‘โ€˜๐ด))
136134, 135eqtrd 2770 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„‚ โ†’ ((-1 ยท -1) ยท (โ„‘โ€˜๐ด)) = (โ„‘โ€˜๐ด))
137130mulm1d 11670 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ (-1 ยท (โ„‘โ€˜๐ด)) = -(โ„‘โ€˜๐ด))
138137oveq2d 7427 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„‚ โ†’ (-1 ยท (-1 ยท (โ„‘โ€˜๐ด))) = (-1 ยท -(โ„‘โ€˜๐ด)))
139131, 136, 1383eqtr3rd 2779 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ (-1 ยท -(โ„‘โ€˜๐ด)) = (โ„‘โ€˜๐ด))
140139adantr 479 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‚ โˆง (โ„‘โ€˜๐ด) < 0) โ†’ (-1 ยท -(โ„‘โ€˜๐ด)) = (โ„‘โ€˜๐ด))
141135adantr 479 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‚ โˆง ยฌ (โ„‘โ€˜๐ด) < 0) โ†’ (1 ยท (โ„‘โ€˜๐ด)) = (โ„‘โ€˜๐ด))
142140, 141ifeqda 4563 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ if((โ„‘โ€˜๐ด) < 0, (-1 ยท -(โ„‘โ€˜๐ด)), (1 ยท (โ„‘โ€˜๐ด))) = (โ„‘โ€˜๐ด))
143127, 142eqtrid 2782 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด))) = (โ„‘โ€˜๐ด))
144143oveq1d 7426 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ ((if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด))) / 2) = ((โ„‘โ€˜๐ด) / 2))
145126, 144eqtr3d 2772 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2)) = ((โ„‘โ€˜๐ด) / 2))
146145oveq2d 7427 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (2 ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2))) = (2 ยท ((โ„‘โ€˜๐ด) / 2)))
147130, 57, 59divcan2d 11996 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (2 ยท ((โ„‘โ€˜๐ด) / 2)) = (โ„‘โ€˜๐ด))
148146, 147eqtrd 2770 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (2 ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (if((โ„‘โ€˜๐ด) < 0, -(โ„‘โ€˜๐ด), (โ„‘โ€˜๐ด)) / 2))) = (โ„‘โ€˜๐ด))
14967, 122, 1483eqtrd 2774 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) = (โ„‘โ€˜๐ด))
150149oveq2d 7427 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ (i ยท ((2 ยท (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))) ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (i ยท (โ„‘โ€˜๐ด)))
15165, 66, 1503eqtr3d 2778 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) = (i ยท (โ„‘โ€˜๐ด)))
15263, 151oveq12d 7429 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ ((((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) + ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2)) + (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = ((โ„œโ€˜๐ด) + (i ยท (โ„‘โ€˜๐ด))))
1531resqcld 14094 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) โˆˆ โ„)
154153recnd 11246 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) โˆˆ โ„‚)
1552, 12mulcld 11238 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) โˆˆ โ„‚)
15657, 155mulcld 11238 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) โˆˆ โ„‚)
15712sqcld 14113 . . . . . 6 (๐ด โˆˆ โ„‚ โ†’ ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2) โˆˆ โ„‚)
158154, 156, 157add32d 11445 . . . . 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 15067 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ ๐ด = ((โ„œโ€˜๐ด) + (i ยท (โ„‘โ€˜๐ด))))
160152, 158, 1593eqtr4d 2780 . . . 4 (๐ด โˆˆ โ„‚ โ†’ ((((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2))โ†‘2) + (2 ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) ยท (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) + ((i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))โ†‘2)) = ๐ด)
16116, 160eqtrd 2770 . . 3 (๐ด โˆˆ โ„‚ โ†’ (((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))โ†‘2) = ๐ด)
16220, 69sqrtge0d 15371 . . . 4 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)))
1631, 10crred 15182 . . . 4 (๐ด โˆˆ โ„‚ โ†’ (โ„œโ€˜((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) = (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)))
164162, 163breqtrrd 5175 . . 3 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (โ„œโ€˜((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))))
165 reim 15060 . . . . . . . . . 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 2772 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ (โ„‘โ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)))
168167eqeq1d 2732 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((โ„‘โ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = 0 โ†” (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) = 0))
169 cnsqrt00 15343 . . . . . . . 8 ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) = 0 โ†” (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = 0))
17021, 169syl 17 . . . . . . 7 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) = 0 โ†” (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = 0))
171 half0 12443 . . . . . . . . 9 (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = 0 โ†” ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) = 0))
17255, 171syl 17 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ ((((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = 0 โ†” ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) = 0))
17349, 50addcomd 11420 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) = ((โ„œโ€˜๐ด) + (absโ€˜๐ด)))
174173eqeq1d 2732 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) = 0 โ†” ((โ„œโ€˜๐ด) + (absโ€˜๐ด)) = 0))
175 addeq0 11641 . . . . . . . . 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 864 . . . . . . . 8 ((โ„œโ€˜๐ด) = -(absโ€˜๐ด) โ†’ ((โ„œโ€˜๐ด) = (absโ€˜๐ด) โˆจ (โ„œโ€˜๐ด) = -(absโ€˜๐ด)))
180 eqcom 2737 . . . . . . . . . 10 (((โ„œโ€˜๐ด)โ†‘2) = ((absโ€˜๐ด)โ†‘2) โ†” ((absโ€˜๐ด)โ†‘2) = ((โ„œโ€˜๐ด)โ†‘2))
181180a1i 11 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (((โ„œโ€˜๐ด)โ†‘2) = ((absโ€˜๐ด)โ†‘2) โ†” ((absโ€˜๐ด)โ†‘2) = ((โ„œโ€˜๐ด)โ†‘2)))
182 sqeqor 14184 . . . . . . . . . 10 (((โ„œโ€˜๐ด) โˆˆ โ„‚ โˆง (absโ€˜๐ด) โˆˆ โ„‚) โ†’ (((โ„œโ€˜๐ด)โ†‘2) = ((absโ€˜๐ด)โ†‘2) โ†” ((โ„œโ€˜๐ด) = (absโ€˜๐ด) โˆจ (โ„œโ€˜๐ด) = -(absโ€˜๐ด))))
18350, 49, 182syl2anc 582 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (((โ„œโ€˜๐ด)โ†‘2) = ((absโ€˜๐ด)โ†‘2) โ†” ((โ„œโ€˜๐ด) = (absโ€˜๐ด) โˆจ (โ„œโ€˜๐ด) = -(absโ€˜๐ด))))
184103eqeq1d 2732 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ (((absโ€˜๐ด)โ†‘2) = ((โ„œโ€˜๐ด)โ†‘2) โ†” (((โ„œโ€˜๐ด)โ†‘2) + ((โ„‘โ€˜๐ด)โ†‘2)) = ((โ„œโ€˜๐ด)โ†‘2)))
185 addid0 11637 . . . . . . . . . . 11 ((((โ„œโ€˜๐ด)โ†‘2) โˆˆ โ„‚ โˆง ((โ„‘โ€˜๐ด)โ†‘2) โˆˆ โ„‚) โ†’ ((((โ„œโ€˜๐ด)โ†‘2) + ((โ„‘โ€˜๐ด)โ†‘2)) = ((โ„œโ€˜๐ด)โ†‘2) โ†” ((โ„‘โ€˜๐ด)โ†‘2) = 0))
18699, 102, 185syl2anc 582 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ ((((โ„œโ€˜๐ด)โ†‘2) + ((โ„‘โ€˜๐ด)โ†‘2)) = ((โ„œโ€˜๐ด)โ†‘2) โ†” ((โ„‘โ€˜๐ด)โ†‘2) = 0))
187 sqeq0 14089 . . . . . . . . . . 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 1135 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„œโ€˜๐ด) = -(absโ€˜๐ด))
195194oveq2d 7427 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) = ((absโ€˜๐ด) + -(absโ€˜๐ด)))
196493ad2ant1 1131 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (absโ€˜๐ด) โˆˆ โ„‚)
197196negidd 11565 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((absโ€˜๐ด) + -(absโ€˜๐ด)) = 0)
198195, 197eqtrd 2770 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((absโ€˜๐ด) + (โ„œโ€˜๐ด)) = 0)
199198oveq1d 7426 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = (0 / 2))
200 2cn 12291 . . . . . . . . . . . . . . . . 17 2 โˆˆ โ„‚
201200, 58div0i 11952 . . . . . . . . . . . . . . . 16 (0 / 2) = 0
202199, 201eqtrdi 2786 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2) = 0)
203202fveq2d 6894 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) = (โˆšโ€˜0))
204 sqrt0 15192 . . . . . . . . . . . . . 14 (โˆšโ€˜0) = 0
205203, 204eqtrdi 2786 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) = 0)
206 simp3 1136 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„‘โ€˜๐ด) = 0)
207 0red 11221 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ 0 โˆˆ โ„)
208207ltnrd 11352 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ยฌ 0 < 0)
209206, 208eqnbrtrd 5165 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ยฌ (โ„‘โ€˜๐ด) < 0)
210209iffalsed 4538 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ if((โ„‘โ€˜๐ด) < 0, -1, 1) = 1)
211194oveq2d 7427 . . . . . . . . . . . . . . . . . . . 20 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) = ((absโ€˜๐ด) โˆ’ -(absโ€˜๐ด)))
21249, 49subnegd 11582 . . . . . . . . . . . . . . . . . . . . . 22 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) โˆ’ -(absโ€˜๐ด)) = ((absโ€˜๐ด) + (absโ€˜๐ด)))
213492timesd 12459 . . . . . . . . . . . . . . . . . . . . . 22 (๐ด โˆˆ โ„‚ โ†’ (2 ยท (absโ€˜๐ด)) = ((absโ€˜๐ด) + (absโ€˜๐ด)))
214212, 213eqtr4d 2773 . . . . . . . . . . . . . . . . . . . . 21 (๐ด โˆˆ โ„‚ โ†’ ((absโ€˜๐ด) โˆ’ -(absโ€˜๐ด)) = (2 ยท (absโ€˜๐ด)))
2152143ad2ant1 1131 . . . . . . . . . . . . . . . . . . . 20 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((absโ€˜๐ด) โˆ’ -(absโ€˜๐ด)) = (2 ยท (absโ€˜๐ด)))
216211, 215eqtrd 2770 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) = (2 ยท (absโ€˜๐ด)))
217216oveq1d 7426 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2) = ((2 ยท (absโ€˜๐ด)) / 2))
21849, 57, 59divcan3d 11999 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„‚ โ†’ ((2 ยท (absโ€˜๐ด)) / 2) = (absโ€˜๐ด))
2192183ad2ant1 1131 . . . . . . . . . . . . . . . . . 18 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((2 ยท (absโ€˜๐ด)) / 2) = (absโ€˜๐ด))
220217, 219eqtrd 2770 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2) = (absโ€˜๐ด))
221220fveq2d 6894 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)) = (โˆšโ€˜(absโ€˜๐ด)))
222210, 221oveq12d 7429 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))) = (1 ยท (โˆšโ€˜(absโ€˜๐ด))))
223 absge0 15238 . . . . . . . . . . . . . . . . . . 19 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (absโ€˜๐ด))
22417, 223resqrtcld 15368 . . . . . . . . . . . . . . . . . 18 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(absโ€˜๐ด)) โˆˆ โ„)
225224recnd 11246 . . . . . . . . . . . . . . . . 17 (๐ด โˆˆ โ„‚ โ†’ (โˆšโ€˜(absโ€˜๐ด)) โˆˆ โ„‚)
226225mullidd 11236 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„‚ โ†’ (1 ยท (โˆšโ€˜(absโ€˜๐ด))) = (โˆšโ€˜(absโ€˜๐ด)))
2272263ad2ant1 1131 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (1 ยท (โˆšโ€˜(absโ€˜๐ด))) = (โˆšโ€˜(absโ€˜๐ด)))
228222, 227eqtrd 2770 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))) = (โˆšโ€˜(absโ€˜๐ด)))
229228oveq2d 7427 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))) = (i ยท (โˆšโ€˜(absโ€˜๐ด))))
230205, 229oveq12d 7429 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (0 + (i ยท (โˆšโ€˜(absโ€˜๐ด)))))
2314, 225mulcld 11238 . . . . . . . . . . . . . 14 (๐ด โˆˆ โ„‚ โ†’ (i ยท (โˆšโ€˜(absโ€˜๐ด))) โˆˆ โ„‚)
2322313ad2ant1 1131 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (i ยท (โˆšโ€˜(absโ€˜๐ด))) โˆˆ โ„‚)
233232addlidd 11419 . . . . . . . . . . . 12 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (0 + (i ยท (โˆšโ€˜(absโ€˜๐ด)))) = (i ยท (โˆšโ€˜(absโ€˜๐ด))))
234230, 233eqtrd 2770 . . . . . . . . . . 11 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (i ยท (โˆšโ€˜(absโ€˜๐ด))))
235234oveq2d 7427 . . . . . . . . . 10 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) = (i ยท (i ยท (โˆšโ€˜(absโ€˜๐ด)))))
236 ixi 11847 . . . . . . . . . . . . . 14 (i ยท i) = -1
237236a1i 11 . . . . . . . . . . . . 13 (๐ด โˆˆ โ„‚ โ†’ (i ยท i) = -1)
238237oveq1d 7426 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ ((i ยท i) ยท (โˆšโ€˜(absโ€˜๐ด))) = (-1 ยท (โˆšโ€˜(absโ€˜๐ด))))
2394, 4, 225mulassd 11241 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ ((i ยท i) ยท (โˆšโ€˜(absโ€˜๐ด))) = (i ยท (i ยท (โˆšโ€˜(absโ€˜๐ด)))))
240225mulm1d 11670 . . . . . . . . . . . 12 (๐ด โˆˆ โ„‚ โ†’ (-1 ยท (โˆšโ€˜(absโ€˜๐ด))) = -(โˆšโ€˜(absโ€˜๐ด)))
241238, 239, 2403eqtr3d 2778 . . . . . . . . . . 11 (๐ด โˆˆ โ„‚ โ†’ (i ยท (i ยท (โˆšโ€˜(absโ€˜๐ด)))) = -(โˆšโ€˜(absโ€˜๐ด)))
2422413ad2ant1 1131 . . . . . . . . . 10 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (i ยท (i ยท (โˆšโ€˜(absโ€˜๐ด)))) = -(โˆšโ€˜(absโ€˜๐ด)))
243235, 242eqtrd 2770 . . . . . . . . 9 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) = -(โˆšโ€˜(absโ€˜๐ด)))
244243fveq2d 6894 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„œโ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = (โ„œโ€˜-(โˆšโ€˜(absโ€˜๐ด))))
245224renegcld 11645 . . . . . . . . . 10 (๐ด โˆˆ โ„‚ โ†’ -(โˆšโ€˜(absโ€˜๐ด)) โˆˆ โ„)
246245rered 15175 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (โ„œโ€˜-(โˆšโ€˜(absโ€˜๐ด))) = -(โˆšโ€˜(absโ€˜๐ด)))
2472463ad2ant1 1131 . . . . . . . 8 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„œโ€˜-(โˆšโ€˜(absโ€˜๐ด))) = -(โˆšโ€˜(absโ€˜๐ด)))
248244, 247eqtrd 2770 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„œโ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) = -(โˆšโ€˜(absโ€˜๐ด)))
24917, 223sqrtge0d 15371 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ 0 โ‰ค (โˆšโ€˜(absโ€˜๐ด)))
250224le0neg2d 11790 . . . . . . . . 9 (๐ด โˆˆ โ„‚ โ†’ (0 โ‰ค (โˆšโ€˜(absโ€˜๐ด)) โ†” -(โˆšโ€˜(absโ€˜๐ด)) โ‰ค 0))
251249, 250mpbid 231 . . . . . . . 8 (๐ด โˆˆ โ„‚ โ†’ -(โˆšโ€˜(absโ€˜๐ด)) โ‰ค 0)
2522513ad2ant1 1131 . . . . . . 7 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ -(โˆšโ€˜(absโ€˜๐ด)) โ‰ค 0)
253248, 252eqbrtrd 5169 . . . . . 6 ((๐ด โˆˆ โ„‚ โˆง (โ„œโ€˜๐ด) = -(absโ€˜๐ด) โˆง (โ„‘โ€˜๐ด) = 0) โ†’ (โ„œโ€˜(i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))))) โ‰ค 0)
2542533expib 1120 . . . . 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 11238 . . . . 5 (๐ด โˆˆ โ„‚ โ†’ (i ยท ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2)))))) โˆˆ โ„‚)
257256sqrtcvallem1 42684 . . . 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 15318 . 2 (๐ด โˆˆ โ„‚ โ†’ ((โˆšโ€˜(((absโ€˜๐ด) + (โ„œโ€˜๐ด)) / 2)) + (i ยท (if((โ„‘โ€˜๐ด) < 0, -1, 1) ยท (โˆšโ€˜(((absโ€˜๐ด) โˆ’ (โ„œโ€˜๐ด)) / 2))))) = (โˆšโ€˜๐ด))
260259eqcomd 2736 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 843   โˆง w3a 1085   = wceq 1539   โˆˆ wcel 2104   โ‰  wne 2938  ifcif 4527   class class class wbr 5147  โ€˜cfv 6542  (class class class)co 7411  โ„‚cc 11110  โ„cr 11111  0cc0 11112  1c1 11113  ici 11114   + caddc 11115   ยท cmul 11117   < clt 11252   โ‰ค cle 11253   โˆ’ cmin 11448  -cneg 11449   / cdiv 11875  2c2 12271  โ„+crp 12978  โ†‘cexp 14031  โ„œcre 15048  โ„‘cim 15049  โˆšcsqrt 15184  abscabs 15185
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-sup 9439  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-z 12563  df-uz 12827  df-rp 12979  df-seq 13971  df-exp 14032  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187
This theorem is referenced by:  sqrtcval2  42695  resqrtval  42696  imsqrtval  42697
  Copyright terms: Public domain W3C validator