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 41903
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 15077 and crimi 15078. 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 41902 . . . . 5 (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ∈ ℝ)
21recnd 11183 . . . 4 (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ∈ ℂ)
3 ax-icn 11110 . . . . . 6 i ∈ ℂ
43a1i 11 . . . . 5 (𝐴 ∈ ℂ → i ∈ ℂ)
5 neg1rr 12268 . . . . . . . . 9 -1 ∈ ℝ
6 1re 11155 . . . . . . . . 9 1 ∈ ℝ
75, 6ifcli 4533 . . . . . . . 8 if((ℑ‘𝐴) < 0, -1, 1) ∈ ℝ
87a1i 11 . . . . . . 7 (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, -1, 1) ∈ ℝ)
9 sqrtcvallem3 41900 . . . . . . 7 (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) ∈ ℝ)
108, 9remulcld 11185 . . . . . 6 (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) ∈ ℝ)
1110recnd 11183 . . . . 5 (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) ∈ ℂ)
124, 11mulcld 11175 . . . 4 (𝐴 ∈ ℂ → (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) ∈ ℂ)
132, 12addcld 11174 . . 3 (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) ∈ ℂ)
14 id 22 . . 3 (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
15 binom2 14121 . . . . 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 584 . . . 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 15163 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
18 recl 14995 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ)
1917, 18readdcld 11184 . . . . . . . . . . 11 (𝐴 ∈ ℂ → ((abs‘𝐴) + (ℜ‘𝐴)) ∈ ℝ)
2019rehalfcld 12400 . . . . . . . . . 10 (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) / 2) ∈ ℝ)
2120recnd 11183 . . . . . . . . 9 (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) / 2) ∈ ℂ)
2221sqsqrtd 15324 . . . . . . . 8 (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) = (((abs‘𝐴) + (ℜ‘𝐴)) / 2))
234, 11sqmuld 14063 . . . . . . . . 9 (𝐴 ∈ ℂ → ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) = ((i↑2) · ((if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2)))
24 i2 14106 . . . . . . . . . . 11 (i↑2) = -1
2524a1i 11 . . . . . . . . . 10 (𝐴 ∈ ℂ → (i↑2) = -1)
268recnd 11183 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, -1, 1) ∈ ℂ)
279recnd 11183 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) ∈ ℂ)
2826, 27sqmuld 14063 . . . . . . . . . . 11 (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2) = ((if((ℑ‘𝐴) < 0, -1, 1)↑2) · ((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2)))
29 ovif 7454 . . . . . . . . . . . . . 14 (if((ℑ‘𝐴) < 0, -1, 1)↑2) = if((ℑ‘𝐴) < 0, (-1↑2), (1↑2))
30 neg1sqe1 14100 . . . . . . . . . . . . . . 15 (-1↑2) = 1
31 sq1 14099 . . . . . . . . . . . . . . 15 (1↑2) = 1
32 ifeq12 4504 . . . . . . . . . . . . . . 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 4526 . . . . . . . . . . . . . 14 if((ℑ‘𝐴) < 0, 1, 1) = 1
3529, 33, 343eqtri 2768 . . . . . . . . . . . . 13 (if((ℑ‘𝐴) < 0, -1, 1)↑2) = 1
3635a1i 11 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1)↑2) = 1)
3717, 18resubcld 11583 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℂ → ((abs‘𝐴) − (ℜ‘𝐴)) ∈ ℝ)
3837rehalfcld 12400 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → (((abs‘𝐴) − (ℜ‘𝐴)) / 2) ∈ ℝ)
3938recnd 11183 . . . . . . . . . . . . 13 (𝐴 ∈ ℂ → (((abs‘𝐴) − (ℜ‘𝐴)) / 2) ∈ ℂ)
4039sqsqrtd 15324 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2) = (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
4136, 40oveq12d 7375 . . . . . . . . . . 11 (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1)↑2) · ((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2)) = (1 · (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
4239mulid2d 11173 . . . . . . . . . . 11 (𝐴 ∈ ℂ → (1 · (((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
4328, 41, 423eqtrd 2780 . . . . . . . . . 10 (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2) = (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
4425, 43oveq12d 7375 . . . . . . . . 9 (𝐴 ∈ ℂ → ((i↑2) · ((if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2)) = (-1 · (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
4539mulm1d 11607 . . . . . . . . 9 (𝐴 ∈ ℂ → (-1 · (((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = -(((abs‘𝐴) − (ℜ‘𝐴)) / 2))
4623, 44, 453eqtrd 2780 . . . . . . . 8 (𝐴 ∈ ℂ → ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) = -(((abs‘𝐴) − (ℜ‘𝐴)) / 2))
4722, 46oveq12d 7375 . . . . . . 7 (𝐴 ∈ ℂ → (((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) + ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2)) = ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) + -(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
4821, 39negsubd 11518 . . . . . . 7 (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) + -(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) − (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
4917recnd 11183 . . . . . . . . . . 11 (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℂ)
5018recnd 11183 . . . . . . . . . . 11 (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℂ)
5149, 50, 50pnncand 11551 . . . . . . . . . 10 (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) − ((abs‘𝐴) − (ℜ‘𝐴))) = ((ℜ‘𝐴) + (ℜ‘𝐴)))
52502timesd 12396 . . . . . . . . . 10 (𝐴 ∈ ℂ → (2 · (ℜ‘𝐴)) = ((ℜ‘𝐴) + (ℜ‘𝐴)))
5351, 52eqtr4d 2779 . . . . . . . . 9 (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) − ((abs‘𝐴) − (ℜ‘𝐴))) = (2 · (ℜ‘𝐴)))
5453oveq1d 7372 . . . . . . . 8 (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) − ((abs‘𝐴) − (ℜ‘𝐴))) / 2) = ((2 · (ℜ‘𝐴)) / 2))
5519recnd 11183 . . . . . . . . 9 (𝐴 ∈ ℂ → ((abs‘𝐴) + (ℜ‘𝐴)) ∈ ℂ)
5637recnd 11183 . . . . . . . . 9 (𝐴 ∈ ℂ → ((abs‘𝐴) − (ℜ‘𝐴)) ∈ ℂ)
57 2cnd 12231 . . . . . . . . 9 (𝐴 ∈ ℂ → 2 ∈ ℂ)
58 2ne0 12257 . . . . . . . . . 10 2 ≠ 0
5958a1i 11 . . . . . . . . 9 (𝐴 ∈ ℂ → 2 ≠ 0)
6055, 56, 57, 59divsubdird 11970 . . . . . . . 8 (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) − ((abs‘𝐴) − (ℜ‘𝐴))) / 2) = ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) − (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
6150, 57, 59divcan3d 11936 . . . . . . . 8 (𝐴 ∈ ℂ → ((2 · (ℜ‘𝐴)) / 2) = (ℜ‘𝐴))
6254, 60, 613eqtr3d 2784 . . . . . . 7 (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) − (((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = (ℜ‘𝐴))
6347, 48, 623eqtrd 2780 . . . . . 6 (𝐴 ∈ ℂ → (((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) + ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2)) = (ℜ‘𝐴))
6457, 2mulcld 11175 . . . . . . . 8 (𝐴 ∈ ℂ → (2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) ∈ ℂ)
6564, 4, 11mul12d 11364 . . . . . . 7 (𝐴 ∈ ℂ → ((2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (i · ((2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))
6657, 2, 12mulassd 11178 . . . . . . 7 (𝐴 ∈ ℂ → ((2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))))
6757, 2, 11mulassd 11178 . . . . . . . . 9 (𝐴 ∈ ℂ → ((2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))
682, 26, 27mul12d 11364 . . . . . . . . . . 11 (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (if((ℑ‘𝐴) < 0, -1, 1) · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))
69 sqrtcvallem4 41901 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) + (ℜ‘𝐴)) / 2))
70 halfnneg2 12384 . . . . . . . . . . . . . . . . 17 (((abs‘𝐴) + (ℜ‘𝐴)) ∈ ℝ → (0 ≤ ((abs‘𝐴) + (ℜ‘𝐴)) ↔ 0 ≤ (((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
7119, 70syl 17 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℂ → (0 ≤ ((abs‘𝐴) + (ℜ‘𝐴)) ↔ 0 ≤ (((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
7269, 71mpbird 256 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℂ → 0 ≤ ((abs‘𝐴) + (ℜ‘𝐴)))
73 2rp 12920 . . . . . . . . . . . . . . . 16 2 ∈ ℝ+
7473a1i 11 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℂ → 2 ∈ ℝ+)
7519, 72, 74sqrtdivd 15308 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = ((√‘((abs‘𝐴) + (ℜ‘𝐴))) / (√‘2)))
76 sqrtcvallem2 41899 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
77 halfnneg2 12384 . . . . . . . . . . . . . . . . 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 15308 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = ((√‘((abs‘𝐴) − (ℜ‘𝐴))) / (√‘2)))
8175, 80oveq12d 7375 . . . . . . . . . . . . 13 (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (((√‘((abs‘𝐴) + (ℜ‘𝐴))) / (√‘2)) · ((√‘((abs‘𝐴) − (ℜ‘𝐴))) / (√‘2))))
8219, 72resqrtcld 15302 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℂ → (√‘((abs‘𝐴) + (ℜ‘𝐴))) ∈ ℝ)
8382recnd 11183 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → (√‘((abs‘𝐴) + (ℜ‘𝐴))) ∈ ℂ)
84 2re 12227 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ
8584a1i 11 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℂ → 2 ∈ ℝ)
86 0le2 12255 . . . . . . . . . . . . . . . . 17 0 ≤ 2
8786a1i 11 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℂ → 0 ≤ 2)
8885, 87resqrtcld 15302 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℂ → (√‘2) ∈ ℝ)
8988recnd 11183 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → (√‘2) ∈ ℂ)
9037, 79resqrtcld 15302 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℂ → (√‘((abs‘𝐴) − (ℜ‘𝐴))) ∈ ℝ)
9190recnd 11183 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → (√‘((abs‘𝐴) − (ℜ‘𝐴))) ∈ ℂ)
92 sqrt00 15148 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) = 0 ↔ 2 = 0))
9384, 86, 92mp2an 690 . . . . . . . . . . . . . . . . 17 ((√‘2) = 0 ↔ 2 = 0)
9493necon3bii 2996 . . . . . . . . . . . . . . . 16 ((√‘2) ≠ 0 ↔ 2 ≠ 0)
9558, 94mpbir 230 . . . . . . . . . . . . . . 15 (√‘2) ≠ 0
9695a1i 11 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → (√‘2) ≠ 0)
9783, 89, 91, 89, 96, 96divmuldivd 11972 . . . . . . . . . . . . 13 (𝐴 ∈ ℂ → (((√‘((abs‘𝐴) + (ℜ‘𝐴))) / (√‘2)) · ((√‘((abs‘𝐴) − (ℜ‘𝐴))) / (√‘2))) = (((√‘((abs‘𝐴) + (ℜ‘𝐴))) · (√‘((abs‘𝐴) − (ℜ‘𝐴)))) / ((√‘2) · (√‘2))))
9818resqcld 14030 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℂ → ((ℜ‘𝐴)↑2) ∈ ℝ)
9998recnd 11183 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ ℂ → ((ℜ‘𝐴)↑2) ∈ ℂ)
100 imcl 14996 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ)
101100resqcld 14030 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℂ → ((ℑ‘𝐴)↑2) ∈ ℝ)
102101recnd 11183 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ ℂ → ((ℑ‘𝐴)↑2) ∈ ℂ)
103 absvalsq2 15166 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
10499, 102, 103mvrladdd 11568 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) − ((ℜ‘𝐴)↑2)) = ((ℑ‘𝐴)↑2))
105 subsq 14114 . . . . . . . . . . . . . . . . . 18 (((abs‘𝐴) ∈ ℂ ∧ (ℜ‘𝐴) ∈ ℂ) → (((abs‘𝐴)↑2) − ((ℜ‘𝐴)↑2)) = (((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴))))
10649, 50, 105syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) − ((ℜ‘𝐴)↑2)) = (((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴))))
107104, 106eqtr3d 2778 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℂ → ((ℑ‘𝐴)↑2) = (((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴))))
108107fveq2d 6846 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℂ → (√‘((ℑ‘𝐴)↑2)) = (√‘(((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴)))))
109100absred 15301 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℂ → (abs‘(ℑ‘𝐴)) = (√‘((ℑ‘𝐴)↑2)))
110 reabsifneg 41894 . . . . . . . . . . . . . . . . 17 ((ℑ‘𝐴) ∈ ℝ → (abs‘(ℑ‘𝐴)) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)))
111100, 110syl 17 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℂ → (abs‘(ℑ‘𝐴)) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)))
112109, 111eqtr3d 2778 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℂ → (√‘((ℑ‘𝐴)↑2)) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)))
11319, 72, 37, 79sqrtmuld 15309 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴)))) = ((√‘((abs‘𝐴) + (ℜ‘𝐴))) · (√‘((abs‘𝐴) − (ℜ‘𝐴)))))
114108, 112, 1133eqtr3rd 2785 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → ((√‘((abs‘𝐴) + (ℜ‘𝐴))) · (√‘((abs‘𝐴) − (ℜ‘𝐴)))) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)))
115 remsqsqrt 15141 . . . . . . . . . . . . . . . 16 ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
11684, 86, 115mp2an 690 . . . . . . . . . . . . . . 15 ((√‘2) · (√‘2)) = 2
117116a1i 11 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → ((√‘2) · (√‘2)) = 2)
118114, 117oveq12d 7375 . . . . . . . . . . . . 13 (𝐴 ∈ ℂ → (((√‘((abs‘𝐴) + (ℜ‘𝐴))) · (√‘((abs‘𝐴) − (ℜ‘𝐴)))) / ((√‘2) · (√‘2))) = (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))
11981, 97, 1183eqtrd 2780 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))
120119oveq2d 7373 . . . . . . . . . . 11 (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)))
12168, 120eqtrd 2776 . . . . . . . . . 10 (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)))
122121oveq2d 7373 . . . . . . . . 9 (𝐴 ∈ ℂ → (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (2 · (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))))
123100renegcld 11582 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℂ → -(ℑ‘𝐴) ∈ ℝ)
124123, 100ifcld 4532 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) ∈ ℝ)
125124recnd 11183 . . . . . . . . . . . . 13 (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) ∈ ℂ)
12626, 125, 57, 59divassd 11966 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) / 2) = (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)))
127 ovif12 7456 . . . . . . . . . . . . . 14 (if((ℑ‘𝐴) < 0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) = if((ℑ‘𝐴) < 0, (-1 · -(ℑ‘𝐴)), (1 · (ℑ‘𝐴)))
1285a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℂ → -1 ∈ ℝ)
129128recnd 11183 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ ℂ → -1 ∈ ℂ)
130100recnd 11183 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℂ)
131129, 129, 130mulassd 11178 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ ℂ → ((-1 · -1) · (ℑ‘𝐴)) = (-1 · (-1 · (ℑ‘𝐴))))
132 neg1mulneg1e1 12366 . . . . . . . . . . . . . . . . . . . 20 (-1 · -1) = 1
133132a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℂ → (-1 · -1) = 1)
134133oveq1d 7372 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ ℂ → ((-1 · -1) · (ℑ‘𝐴)) = (1 · (ℑ‘𝐴)))
135130mulid2d 11173 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ ℂ → (1 · (ℑ‘𝐴)) = (ℑ‘𝐴))
136134, 135eqtrd 2776 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ ℂ → ((-1 · -1) · (ℑ‘𝐴)) = (ℑ‘𝐴))
137130mulm1d 11607 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ ℂ → (-1 · (ℑ‘𝐴)) = -(ℑ‘𝐴))
138137oveq2d 7373 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ ℂ → (-1 · (-1 · (ℑ‘𝐴))) = (-1 · -(ℑ‘𝐴)))
139131, 136, 1383eqtr3rd 2785 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℂ → (-1 · -(ℑ‘𝐴)) = (ℑ‘𝐴))
140139adantr 481 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) < 0) → (-1 · -(ℑ‘𝐴)) = (ℑ‘𝐴))
141135adantr 481 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ ¬ (ℑ‘𝐴) < 0) → (1 · (ℑ‘𝐴)) = (ℑ‘𝐴))
142140, 141ifeqda 4522 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, (-1 · -(ℑ‘𝐴)), (1 · (ℑ‘𝐴))) = (ℑ‘𝐴))
143127, 142eqtrid 2788 . . . . . . . . . . . . 13 (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) = (ℑ‘𝐴))
144143oveq1d 7372 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) / 2) = ((ℑ‘𝐴) / 2))
145126, 144eqtr3d 2778 . . . . . . . . . . 11 (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)) = ((ℑ‘𝐴) / 2))
146145oveq2d 7373 . . . . . . . . . 10 (𝐴 ∈ ℂ → (2 · (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))) = (2 · ((ℑ‘𝐴) / 2)))
147130, 57, 59divcan2d 11933 . . . . . . . . . 10 (𝐴 ∈ ℂ → (2 · ((ℑ‘𝐴) / 2)) = (ℑ‘𝐴))
148146, 147eqtrd 2776 . . . . . . . . 9 (𝐴 ∈ ℂ → (2 · (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))) = (ℑ‘𝐴))
14967, 122, 1483eqtrd 2780 . . . . . . . 8 (𝐴 ∈ ℂ → ((2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (ℑ‘𝐴))
150149oveq2d 7373 . . . . . . 7 (𝐴 ∈ ℂ → (i · ((2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (i · (ℑ‘𝐴)))
15165, 66, 1503eqtr3d 2784 . . . . . 6 (𝐴 ∈ ℂ → (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (i · (ℑ‘𝐴)))
15263, 151oveq12d 7375 . . . . 5 (𝐴 ∈ ℂ → ((((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) + ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2)) + (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = ((ℜ‘𝐴) + (i · (ℑ‘𝐴))))
1531resqcld 14030 . . . . . . 7 (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) ∈ ℝ)
154153recnd 11183 . . . . . 6 (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) ∈ ℂ)
1552, 12mulcld 11175 . . . . . . 7 (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) ∈ ℂ)
15657, 155mulcld 11175 . . . . . 6 (𝐴 ∈ ℂ → (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈ ℂ)
15712sqcld 14049 . . . . . 6 (𝐴 ∈ ℂ → ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) ∈ ℂ)
158154, 156, 157add32d 11382 . . . . 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 15001 . . . . 5 (𝐴 ∈ ℂ → 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴))))
160152, 158, 1593eqtr4d 2786 . . . 4 (𝐴 ∈ ℂ → ((((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) + (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) + ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2)) = 𝐴)
16116, 160eqtrd 2776 . . 3 (𝐴 ∈ ℂ → (((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))↑2) = 𝐴)
16220, 69sqrtge0d 15305 . . . 4 (𝐴 ∈ ℂ → 0 ≤ (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
1631, 10crred 15116 . . . 4 (𝐴 ∈ ℂ → (ℜ‘((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
164162, 163breqtrrd 5133 . . 3 (𝐴 ∈ ℂ → 0 ≤ (ℜ‘((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))))
165 reim 14994 . . . . . . . . . 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 2778 . . . . . . . 8 (𝐴 ∈ ℂ → (ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
168167eqeq1d 2738 . . . . . . 7 (𝐴 ∈ ℂ → ((ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = 0 ↔ (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0))
169 cnsqrt00 15277 . . . . . . . 8 ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0 ↔ (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0))
17021, 169syl 17 . . . . . . 7 (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0 ↔ (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0))
171 half0 12380 . . . . . . . . 9 (((abs‘𝐴) + (ℜ‘𝐴)) ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0 ↔ ((abs‘𝐴) + (ℜ‘𝐴)) = 0))
17255, 171syl 17 . . . . . . . 8 (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0 ↔ ((abs‘𝐴) + (ℜ‘𝐴)) = 0))
17349, 50addcomd 11357 . . . . . . . . 9 (𝐴 ∈ ℂ → ((abs‘𝐴) + (ℜ‘𝐴)) = ((ℜ‘𝐴) + (abs‘𝐴)))
174173eqeq1d 2738 . . . . . . . 8 (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) = 0 ↔ ((ℜ‘𝐴) + (abs‘𝐴)) = 0))
175 addeq0 11578 . . . . . . . . 9 (((ℜ‘𝐴) ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) → (((ℜ‘𝐴) + (abs‘𝐴)) = 0 ↔ (ℜ‘𝐴) = -(abs‘𝐴)))
17650, 49, 175syl2anc 584 . . . . . . . 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 2743 . . . . . . . . . 10 (((ℜ‘𝐴)↑2) = ((abs‘𝐴)↑2) ↔ ((abs‘𝐴)↑2) = ((ℜ‘𝐴)↑2))
181180a1i 11 . . . . . . . . 9 (𝐴 ∈ ℂ → (((ℜ‘𝐴)↑2) = ((abs‘𝐴)↑2) ↔ ((abs‘𝐴)↑2) = ((ℜ‘𝐴)↑2)))
182 sqeqor 14120 . . . . . . . . . 10 (((ℜ‘𝐴) ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) → (((ℜ‘𝐴)↑2) = ((abs‘𝐴)↑2) ↔ ((ℜ‘𝐴) = (abs‘𝐴) ∨ (ℜ‘𝐴) = -(abs‘𝐴))))
18350, 49, 182syl2anc 584 . . . . . . . . 9 (𝐴 ∈ ℂ → (((ℜ‘𝐴)↑2) = ((abs‘𝐴)↑2) ↔ ((ℜ‘𝐴) = (abs‘𝐴) ∨ (ℜ‘𝐴) = -(abs‘𝐴))))
184103eqeq1d 2738 . . . . . . . . . 10 (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) = ((ℜ‘𝐴)↑2) ↔ (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) = ((ℜ‘𝐴)↑2)))
185 addid0 11574 . . . . . . . . . . 11 ((((ℜ‘𝐴)↑2) ∈ ℂ ∧ ((ℑ‘𝐴)↑2) ∈ ℂ) → ((((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) = ((ℜ‘𝐴)↑2) ↔ ((ℑ‘𝐴)↑2) = 0))
18699, 102, 185syl2anc 584 . . . . . . . . . 10 (𝐴 ∈ ℂ → ((((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) = ((ℜ‘𝐴)↑2) ↔ ((ℑ‘𝐴)↑2) = 0))
187 sqeq0 14025 . . . . . . . . . . 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 551 . . . . . 6 (𝐴 ∈ ℂ → ((ℜ‘𝐴) = -(abs‘𝐴) → ((ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0)))
193178, 192sylbid 239 . . . . 5 (𝐴 ∈ ℂ → ((ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = 0 → ((ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0)))
194 simp2 1137 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘𝐴) = -(abs‘𝐴))
195194oveq2d 7373 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) + (ℜ‘𝐴)) = ((abs‘𝐴) + -(abs‘𝐴)))
196493ad2ant1 1133 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (abs‘𝐴) ∈ ℂ)
197196negidd 11502 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) + -(abs‘𝐴)) = 0)
198195, 197eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) + (ℜ‘𝐴)) = 0)
199198oveq1d 7372 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = (0 / 2))
200 2cn 12228 . . . . . . . . . . . . . . . . 17 2 ∈ ℂ
201200, 58div0i 11889 . . . . . . . . . . . . . . . 16 (0 / 2) = 0
202199, 201eqtrdi 2792 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0)
203202fveq2d 6846 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = (√‘0))
204 sqrt0 15126 . . . . . . . . . . . . . 14 (√‘0) = 0
205203, 204eqtrdi 2792 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0)
206 simp3 1138 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℑ‘𝐴) = 0)
207 0red 11158 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → 0 ∈ ℝ)
208207ltnrd 11289 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ¬ 0 < 0)
209206, 208eqnbrtrd 5123 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ¬ (ℑ‘𝐴) < 0)
210209iffalsed 4497 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → if((ℑ‘𝐴) < 0, -1, 1) = 1)
211194oveq2d 7373 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) − (ℜ‘𝐴)) = ((abs‘𝐴) − -(abs‘𝐴)))
21249, 49subnegd 11519 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∈ ℂ → ((abs‘𝐴) − -(abs‘𝐴)) = ((abs‘𝐴) + (abs‘𝐴)))
213492timesd 12396 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∈ ℂ → (2 · (abs‘𝐴)) = ((abs‘𝐴) + (abs‘𝐴)))
214212, 213eqtr4d 2779 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ∈ ℂ → ((abs‘𝐴) − -(abs‘𝐴)) = (2 · (abs‘𝐴)))
2152143ad2ant1 1133 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) − -(abs‘𝐴)) = (2 · (abs‘𝐴)))
216211, 215eqtrd 2776 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) − (ℜ‘𝐴)) = (2 · (abs‘𝐴)))
217216oveq1d 7372 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (((abs‘𝐴) − (ℜ‘𝐴)) / 2) = ((2 · (abs‘𝐴)) / 2))
21849, 57, 59divcan3d 11936 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℂ → ((2 · (abs‘𝐴)) / 2) = (abs‘𝐴))
2192183ad2ant1 1133 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((2 · (abs‘𝐴)) / 2) = (abs‘𝐴))
220217, 219eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (((abs‘𝐴) − (ℜ‘𝐴)) / 2) = (abs‘𝐴))
221220fveq2d 6846 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = (√‘(abs‘𝐴)))
222210, 221oveq12d 7375 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (1 · (√‘(abs‘𝐴))))
223 absge0 15172 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))
22417, 223resqrtcld 15302 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ ℂ → (√‘(abs‘𝐴)) ∈ ℝ)
225224recnd 11183 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ ℂ → (√‘(abs‘𝐴)) ∈ ℂ)
226225mulid2d 11173 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℂ → (1 · (√‘(abs‘𝐴))) = (√‘(abs‘𝐴)))
2272263ad2ant1 1133 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (1 · (√‘(abs‘𝐴))) = (√‘(abs‘𝐴)))
228222, 227eqtrd 2776 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (√‘(abs‘𝐴)))
229228oveq2d 7373 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (i · (√‘(abs‘𝐴))))
230205, 229oveq12d 7375 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (0 + (i · (√‘(abs‘𝐴)))))
2314, 225mulcld 11175 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → (i · (√‘(abs‘𝐴))) ∈ ℂ)
2322313ad2ant1 1133 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · (√‘(abs‘𝐴))) ∈ ℂ)
233232addid2d 11356 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (0 + (i · (√‘(abs‘𝐴)))) = (i · (√‘(abs‘𝐴))))
234230, 233eqtrd 2776 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (i · (√‘(abs‘𝐴))))
235234oveq2d 7373 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (i · (i · (√‘(abs‘𝐴)))))
236 ixi 11784 . . . . . . . . . . . . . 14 (i · i) = -1
237236a1i 11 . . . . . . . . . . . . 13 (𝐴 ∈ ℂ → (i · i) = -1)
238237oveq1d 7372 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → ((i · i) · (√‘(abs‘𝐴))) = (-1 · (√‘(abs‘𝐴))))
2394, 4, 225mulassd 11178 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → ((i · i) · (√‘(abs‘𝐴))) = (i · (i · (√‘(abs‘𝐴)))))
240225mulm1d 11607 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → (-1 · (√‘(abs‘𝐴))) = -(√‘(abs‘𝐴)))
241238, 239, 2403eqtr3d 2784 . . . . . . . . . . 11 (𝐴 ∈ ℂ → (i · (i · (√‘(abs‘𝐴)))) = -(√‘(abs‘𝐴)))
2422413ad2ant1 1133 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · (i · (√‘(abs‘𝐴)))) = -(√‘(abs‘𝐴)))
243235, 242eqtrd 2776 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = -(√‘(abs‘𝐴)))
244243fveq2d 6846 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = (ℜ‘-(√‘(abs‘𝐴))))
245224renegcld 11582 . . . . . . . . . 10 (𝐴 ∈ ℂ → -(√‘(abs‘𝐴)) ∈ ℝ)
246245rered 15109 . . . . . . . . 9 (𝐴 ∈ ℂ → (ℜ‘-(√‘(abs‘𝐴))) = -(√‘(abs‘𝐴)))
2472463ad2ant1 1133 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘-(√‘(abs‘𝐴))) = -(√‘(abs‘𝐴)))
248244, 247eqtrd 2776 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = -(√‘(abs‘𝐴)))
24917, 223sqrtge0d 15305 . . . . . . . . 9 (𝐴 ∈ ℂ → 0 ≤ (√‘(abs‘𝐴)))
250224le0neg2d 11727 . . . . . . . . 9 (𝐴 ∈ ℂ → (0 ≤ (√‘(abs‘𝐴)) ↔ -(√‘(abs‘𝐴)) ≤ 0))
251249, 250mpbid 231 . . . . . . . 8 (𝐴 ∈ ℂ → -(√‘(abs‘𝐴)) ≤ 0)
2522513ad2ant1 1133 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → -(√‘(abs‘𝐴)) ≤ 0)
253248, 252eqbrtrd 5127 . . . . . 6 ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) ≤ 0)
2542533expib 1122 . . . . 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 11175 . . . . 5 (𝐴 ∈ ℂ → (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈ ℂ)
257256sqrtcvallem1 41893 . . . 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 15252 . 2 (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (√‘𝐴))
260259eqcomd 2742 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 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wne 2943  ifcif 4486   class class class wbr 5105  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052  ici 11053   + caddc 11054   · cmul 11056   < clt 11189  cle 11190  cmin 11385  -cneg 11386   / cdiv 11812  2c2 12208  +crp 12915  cexp 13967  cre 14982  cim 14983  csqrt 15118  abscabs 15119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-sup 9378  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-z 12500  df-uz 12764  df-rp 12916  df-seq 13907  df-exp 13968  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121
This theorem is referenced by:  sqrtcval2  41904  resqrtval  41905  imsqrtval  41906
  Copyright terms: Public domain W3C validator