Proof of Theorem sqrtcval
Step | Hyp | Ref
| Expression |
1 | | sqrtcvallem5 41902 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ∈ ℝ) |
2 | 1 | recnd 11183 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ∈ ℂ) |
3 | | ax-icn 11110 |
. . . . . 6
⊢ i ∈
ℂ |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℂ → i ∈
ℂ) |
5 | | neg1rr 12268 |
. . . . . . . . 9
⊢ -1 ∈
ℝ |
6 | | 1re 11155 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
7 | 5, 6 | ifcli 4533 |
. . . . . . . 8
⊢
if((ℑ‘𝐴)
< 0, -1, 1) ∈ ℝ |
8 | 7 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
if((ℑ‘𝐴) <
0, -1, 1) ∈ ℝ) |
9 | | sqrtcvallem3 41900 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) ∈ ℝ) |
10 | 8, 9 | remulcld 11185 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) ∈ ℝ) |
11 | 10 | recnd 11183 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) ∈ ℂ) |
12 | 4, 11 | mulcld 11175 |
. . . 4
⊢ (𝐴 ∈ ℂ → (i
· (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) ∈ ℂ) |
13 | 2, 12 | addcld 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))) |
16 | 2, 12, 15 | syl2anc 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
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) |
19 | 17, 18 | readdcld 11184 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) +
(ℜ‘𝐴)) ∈
ℝ) |
20 | 19 | rehalfcld 12400 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) +
(ℜ‘𝐴)) / 2)
∈ ℝ) |
21 | 20 | recnd 11183 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) +
(ℜ‘𝐴)) / 2)
∈ ℂ) |
22 | 21 | sqsqrtd 15324 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) = (((abs‘𝐴) + (ℜ‘𝐴)) / 2)) |
23 | 4, 11 | sqmuld 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 |
25 | 24 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(i↑2) = -1) |
26 | 8 | recnd 11183 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
if((ℑ‘𝐴) <
0, -1, 1) ∈ ℂ) |
27 | 9 | recnd 11183 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) ∈ ℂ) |
28 | 26, 27 | sqmuld 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)) |
33 | 30, 31, 32 | mp2an 690 |
. . . . . . . . . . . . . 14
⊢
if((ℑ‘𝐴)
< 0, (-1↑2), (1↑2)) = if((ℑ‘𝐴) < 0, 1, 1) |
34 | | ifid 4526 |
. . . . . . . . . . . . . 14
⊢
if((ℑ‘𝐴)
< 0, 1, 1) = 1 |
35 | 29, 33, 34 | 3eqtri 2768 |
. . . . . . . . . . . . 13
⊢
(if((ℑ‘𝐴) < 0, -1, 1)↑2) =
1 |
36 | 35 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(if((ℑ‘𝐴) <
0, -1, 1)↑2) = 1) |
37 | 17, 18 | resubcld 11583 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) −
(ℜ‘𝐴)) ∈
ℝ) |
38 | 37 | rehalfcld 12400 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) −
(ℜ‘𝐴)) / 2)
∈ ℝ) |
39 | 38 | recnd 11183 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) −
(ℜ‘𝐴)) / 2)
∈ ℂ) |
40 | 39 | sqsqrtd 15324 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2) = (((abs‘𝐴) − (ℜ‘𝐴)) / 2)) |
41 | 36, 40 | oveq12d 7375 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
((if((ℑ‘𝐴) <
0, -1, 1)↑2) · ((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2)) = (1 ·
(((abs‘𝐴) −
(ℜ‘𝐴)) /
2))) |
42 | 39 | mulid2d 11173 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (1
· (((abs‘𝐴)
− (ℜ‘𝐴)) /
2)) = (((abs‘𝐴)
− (ℜ‘𝐴)) /
2)) |
43 | 28, 41, 42 | 3eqtrd 2780 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
((if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2) = (((abs‘𝐴) − (ℜ‘𝐴)) / 2)) |
44 | 25, 43 | oveq12d 7375 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
((i↑2) · ((if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2)) = (-1 ·
(((abs‘𝐴) −
(ℜ‘𝐴)) /
2))) |
45 | 39 | mulm1d 11607 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (-1
· (((abs‘𝐴)
− (ℜ‘𝐴)) /
2)) = -(((abs‘𝐴)
− (ℜ‘𝐴)) /
2)) |
46 | 23, 44, 45 | 3eqtrd 2780 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((i
· (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) = -(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) |
47 | 22, 46 | oveq12d 7375 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) + ((i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2)) = ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) + -(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) |
48 | 21, 39 | negsubd 11518 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2) +
-(((abs‘𝐴) −
(ℜ‘𝐴)) / 2)) =
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2)
− (((abs‘𝐴)
− (ℜ‘𝐴)) /
2))) |
49 | 17 | recnd 11183 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℂ) |
50 | 18 | recnd 11183 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℂ) |
51 | 49, 50, 50 | pnncand 11551 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) +
(ℜ‘𝐴)) −
((abs‘𝐴) −
(ℜ‘𝐴))) =
((ℜ‘𝐴) +
(ℜ‘𝐴))) |
52 | 50 | 2timesd 12396 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (2
· (ℜ‘𝐴))
= ((ℜ‘𝐴) +
(ℜ‘𝐴))) |
53 | 51, 52 | eqtr4d 2779 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) +
(ℜ‘𝐴)) −
((abs‘𝐴) −
(ℜ‘𝐴))) = (2
· (ℜ‘𝐴))) |
54 | 53 | oveq1d 7372 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
((((abs‘𝐴) +
(ℜ‘𝐴)) −
((abs‘𝐴) −
(ℜ‘𝐴))) / 2) =
((2 · (ℜ‘𝐴)) / 2)) |
55 | 19 | recnd 11183 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) +
(ℜ‘𝐴)) ∈
ℂ) |
56 | 37 | recnd 11183 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) −
(ℜ‘𝐴)) ∈
ℂ) |
57 | | 2cnd 12231 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → 2 ∈
ℂ) |
58 | | 2ne0 12257 |
. . . . . . . . . 10
⊢ 2 ≠
0 |
59 | 58 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → 2 ≠
0) |
60 | 55, 56, 57, 59 | divsubdird 11970 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
((((abs‘𝐴) +
(ℜ‘𝐴)) −
((abs‘𝐴) −
(ℜ‘𝐴))) / 2) =
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2)
− (((abs‘𝐴)
− (ℜ‘𝐴)) /
2))) |
61 | 50, 57, 59 | divcan3d 11936 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((2
· (ℜ‘𝐴))
/ 2) = (ℜ‘𝐴)) |
62 | 54, 60, 61 | 3eqtr3d 2784 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2)
− (((abs‘𝐴)
− (ℜ‘𝐴)) /
2)) = (ℜ‘𝐴)) |
63 | 47, 48, 62 | 3eqtrd 2780 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) + ((i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2)) = (ℜ‘𝐴)) |
64 | 57, 2 | mulcld 11175 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (2
· (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) ∈ ℂ) |
65 | 64, 4, 11 | mul12d 11364 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ((2
· (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (i · ((2 ·
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) |
66 | 57, 2, 12 | mulassd 11178 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ((2
· (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (2 ·
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) |
67 | 57, 2, 11 | mulassd 11178 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((2
· (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (2 ·
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) |
68 | 2, 26, 27 | mul12d 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))) |
71 | 19, 70 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → (0 ≤
((abs‘𝐴) +
(ℜ‘𝐴)) ↔ 0
≤ (((abs‘𝐴) +
(ℜ‘𝐴)) /
2))) |
72 | 69, 71 | mpbird 256 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → 0 ≤
((abs‘𝐴) +
(ℜ‘𝐴))) |
73 | | 2rp 12920 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ+ |
74 | 73 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → 2 ∈
ℝ+) |
75 | 19, 72, 74 | sqrtdivd 15308 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = ((√‘((abs‘𝐴) + (ℜ‘𝐴))) /
(√‘2))) |
76 | | sqrtcvallem2 41899 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → 0 ≤
(((abs‘𝐴) −
(ℜ‘𝐴)) /
2)) |
77 | | halfnneg2 12384 |
. . . . . . . . . . . . . . . . 17
⊢
(((abs‘𝐴)
− (ℜ‘𝐴))
∈ ℝ → (0 ≤ ((abs‘𝐴) − (ℜ‘𝐴)) ↔ 0 ≤ (((abs‘𝐴) − (ℜ‘𝐴)) / 2))) |
78 | 37, 77 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → (0 ≤
((abs‘𝐴) −
(ℜ‘𝐴)) ↔ 0
≤ (((abs‘𝐴)
− (ℜ‘𝐴)) /
2))) |
79 | 76, 78 | mpbird 256 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → 0 ≤
((abs‘𝐴) −
(ℜ‘𝐴))) |
80 | 37, 79, 74 | sqrtdivd 15308 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = ((√‘((abs‘𝐴) − (ℜ‘𝐴))) /
(√‘2))) |
81 | 75, 80 | oveq12d 7375 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) =
(((√‘((abs‘𝐴) + (ℜ‘𝐴))) / (√‘2)) ·
((√‘((abs‘𝐴) − (ℜ‘𝐴))) / (√‘2)))) |
82 | 19, 72 | resqrtcld 15302 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(√‘((abs‘𝐴) + (ℜ‘𝐴))) ∈ ℝ) |
83 | 82 | recnd 11183 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(√‘((abs‘𝐴) + (ℜ‘𝐴))) ∈ ℂ) |
84 | | 2re 12227 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ |
85 | 84 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → 2 ∈
ℝ) |
86 | | 0le2 12255 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ≤
2 |
87 | 86 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → 0 ≤
2) |
88 | 85, 87 | resqrtcld 15302 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(√‘2) ∈ ℝ) |
89 | 88 | recnd 11183 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(√‘2) ∈ ℂ) |
90 | 37, 79 | resqrtcld 15302 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(√‘((abs‘𝐴) − (ℜ‘𝐴))) ∈ ℝ) |
91 | 90 | recnd 11183 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(√‘((abs‘𝐴) − (ℜ‘𝐴))) ∈ ℂ) |
92 | | sqrt00 15148 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℝ ∧ 0 ≤ 2) → ((√‘2) = 0 ↔ 2 =
0)) |
93 | 84, 86, 92 | mp2an 690 |
. . . . . . . . . . . . . . . . 17
⊢
((√‘2) = 0 ↔ 2 = 0) |
94 | 93 | necon3bii 2996 |
. . . . . . . . . . . . . . . 16
⊢
((√‘2) ≠ 0 ↔ 2 ≠ 0) |
95 | 58, 94 | mpbir 230 |
. . . . . . . . . . . . . . 15
⊢
(√‘2) ≠ 0 |
96 | 95 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(√‘2) ≠ 0) |
97 | 83, 89, 91, 89, 96, 96 | divmuldivd 11972 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
(((√‘((abs‘𝐴) + (ℜ‘𝐴))) / (√‘2)) ·
((√‘((abs‘𝐴) − (ℜ‘𝐴))) / (√‘2))) =
(((√‘((abs‘𝐴) + (ℜ‘𝐴))) ·
(√‘((abs‘𝐴) − (ℜ‘𝐴)))) / ((√‘2) ·
(√‘2)))) |
98 | 18 | resqcld 14030 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ →
((ℜ‘𝐴)↑2)
∈ ℝ) |
99 | 98 | recnd 11183 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
((ℜ‘𝐴)↑2)
∈ ℂ) |
100 | | imcl 14996 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℝ) |
101 | 100 | resqcld 14030 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ →
((ℑ‘𝐴)↑2)
∈ ℝ) |
102 | 101 | recnd 11183 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
((ℑ‘𝐴)↑2)
∈ ℂ) |
103 | | absvalsq2 15166 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴)↑2) =
(((ℜ‘𝐴)↑2)
+ ((ℑ‘𝐴)↑2))) |
104 | 99, 102, 103 | mvrladdd 11568 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴)↑2)
− ((ℜ‘𝐴)↑2)) = ((ℑ‘𝐴)↑2)) |
105 | | subsq 14114 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘𝐴)
∈ ℂ ∧ (ℜ‘𝐴) ∈ ℂ) → (((abs‘𝐴)↑2) −
((ℜ‘𝐴)↑2))
= (((abs‘𝐴) +
(ℜ‘𝐴)) ·
((abs‘𝐴) −
(ℜ‘𝐴)))) |
106 | 49, 50, 105 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴)↑2)
− ((ℜ‘𝐴)↑2)) = (((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴)))) |
107 | 104, 106 | eqtr3d 2778 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ →
((ℑ‘𝐴)↑2)
= (((abs‘𝐴) +
(ℜ‘𝐴)) ·
((abs‘𝐴) −
(ℜ‘𝐴)))) |
108 | 107 | fveq2d 6846 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(√‘((ℑ‘𝐴)↑2)) =
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴))))) |
109 | 100 | absred 15301 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ →
(abs‘(ℑ‘𝐴)) = (√‘((ℑ‘𝐴)↑2))) |
110 | | reabsifneg 41894 |
. . . . . . . . . . . . . . . . 17
⊢
((ℑ‘𝐴)
∈ ℝ → (abs‘(ℑ‘𝐴)) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) |
111 | 100, 110 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ →
(abs‘(ℑ‘𝐴)) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) |
112 | 109, 111 | eqtr3d 2778 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(√‘((ℑ‘𝐴)↑2)) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) |
113 | 19, 72, 37, 79 | sqrtmuld 15309 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴)))) = ((√‘((abs‘𝐴) + (ℜ‘𝐴))) ·
(√‘((abs‘𝐴) − (ℜ‘𝐴))))) |
114 | 108, 112,
113 | 3eqtr3rd 2785 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
((√‘((abs‘𝐴) + (ℜ‘𝐴))) ·
(√‘((abs‘𝐴) − (ℜ‘𝐴)))) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) |
115 | | remsqsqrt 15141 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℝ ∧ 0 ≤ 2) → ((√‘2) ·
(√‘2)) = 2) |
116 | 84, 86, 115 | mp2an 690 |
. . . . . . . . . . . . . . 15
⊢
((√‘2) · (√‘2)) = 2 |
117 | 116 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
((√‘2) · (√‘2)) = 2) |
118 | 114, 117 | oveq12d 7375 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
(((√‘((abs‘𝐴) + (ℜ‘𝐴))) ·
(√‘((abs‘𝐴) − (ℜ‘𝐴)))) / ((√‘2) ·
(√‘2))) = (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)) |
119 | 81, 97, 118 | 3eqtrd 2780 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)) |
120 | 119 | oveq2d 7373 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(if((ℑ‘𝐴) <
0, -1, 1) · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (if((ℑ‘𝐴) < 0, -1, 1) ·
(if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴)) /
2))) |
121 | 68, 120 | eqtrd 2776 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (if((ℑ‘𝐴) < 0, -1, 1) ·
(if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴)) /
2))) |
122 | 121 | oveq2d 7373 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (2
· ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (2 ·
(if((ℑ‘𝐴) <
0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)))) |
123 | 100 | renegcld 11582 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
-(ℑ‘𝐴) ∈
ℝ) |
124 | 123, 100 | ifcld 4532 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴)) ∈
ℝ) |
125 | 124 | recnd 11183 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴)) ∈
ℂ) |
126 | 26, 125, 57, 59 | divassd 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 · (ℑ‘𝐴))) |
128 | 5 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ → -1 ∈
ℝ) |
129 | 128 | recnd 11183 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ → -1 ∈
ℂ) |
130 | 100 | recnd 11183 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℂ) |
131 | 129, 129,
130 | mulassd 11178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ → ((-1
· -1) · (ℑ‘𝐴)) = (-1 · (-1 ·
(ℑ‘𝐴)))) |
132 | | neg1mulneg1e1 12366 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (-1
· -1) = 1 |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ → (-1
· -1) = 1) |
134 | 133 | oveq1d 7372 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ → ((-1
· -1) · (ℑ‘𝐴)) = (1 · (ℑ‘𝐴))) |
135 | 130 | mulid2d 11173 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ → (1
· (ℑ‘𝐴))
= (ℑ‘𝐴)) |
136 | 134, 135 | eqtrd 2776 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ → ((-1
· -1) · (ℑ‘𝐴)) = (ℑ‘𝐴)) |
137 | 130 | mulm1d 11607 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ → (-1
· (ℑ‘𝐴))
= -(ℑ‘𝐴)) |
138 | 137 | oveq2d 7373 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ → (-1
· (-1 · (ℑ‘𝐴))) = (-1 · -(ℑ‘𝐴))) |
139 | 131, 136,
138 | 3eqtr3rd 2785 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → (-1
· -(ℑ‘𝐴)) = (ℑ‘𝐴)) |
140 | 139 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) < 0)
→ (-1 · -(ℑ‘𝐴)) = (ℑ‘𝐴)) |
141 | 135 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ ¬
(ℑ‘𝐴) < 0)
→ (1 · (ℑ‘𝐴)) = (ℑ‘𝐴)) |
142 | 140, 141 | ifeqda 4522 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
if((ℑ‘𝐴) <
0, (-1 · -(ℑ‘𝐴)), (1 · (ℑ‘𝐴))) = (ℑ‘𝐴)) |
143 | 127, 142 | eqtrid 2788 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
(if((ℑ‘𝐴) <
0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) = (ℑ‘𝐴)) |
144 | 143 | oveq1d 7372 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
((if((ℑ‘𝐴) <
0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) / 2) = ((ℑ‘𝐴) / 2)) |
145 | 126, 144 | eqtr3d 2778 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(if((ℑ‘𝐴) <
0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)) = ((ℑ‘𝐴) / 2)) |
146 | 145 | oveq2d 7373 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (2
· (if((ℑ‘𝐴) < 0, -1, 1) ·
(if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴)) / 2))) =
(2 · ((ℑ‘𝐴) / 2))) |
147 | 130, 57, 59 | divcan2d 11933 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (2
· ((ℑ‘𝐴)
/ 2)) = (ℑ‘𝐴)) |
148 | 146, 147 | eqtrd 2776 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (2
· (if((ℑ‘𝐴) < 0, -1, 1) ·
(if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴)) / 2))) =
(ℑ‘𝐴)) |
149 | 67, 122, 148 | 3eqtrd 2780 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((2
· (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (ℑ‘𝐴)) |
150 | 149 | oveq2d 7373 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (i
· ((2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (i ·
(ℑ‘𝐴))) |
151 | 65, 66, 150 | 3eqtr3d 2784 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (2
· ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (i ·
(ℑ‘𝐴))) |
152 | 63, 151 | oveq12d 7375 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
((((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) + ((i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2)) + (2 ·
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = ((ℜ‘𝐴) + (i ·
(ℑ‘𝐴)))) |
153 | 1 | resqcld 14030 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) ∈
ℝ) |
154 | 153 | recnd 11183 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) ∈
ℂ) |
155 | 2, 12 | mulcld 11175 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) ∈ ℂ) |
156 | 57, 155 | mulcld 11175 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (2
· ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈
ℂ) |
157 | 12 | sqcld 14049 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → ((i
· (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) ∈
ℂ) |
158 | 154, 156,
157 | add32d 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 ·
(ℑ‘𝐴)))) |
160 | 152, 158,
159 | 3eqtr4d 2786 |
. . . 4
⊢ (𝐴 ∈ ℂ →
((((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) + (2 ·
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) + ((i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2)) = 𝐴) |
161 | 16, 160 | eqtrd 2776 |
. . 3
⊢ (𝐴 ∈ ℂ →
(((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))↑2) = 𝐴) |
162 | 20, 69 | sqrtge0d 15305 |
. . . 4
⊢ (𝐴 ∈ ℂ → 0 ≤
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) |
163 | 1, 10 | crred 15116 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(ℜ‘((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) =
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) |
164 | 162, 163 | breqtrrd 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)))))))) |
166 | 13, 165 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(ℜ‘((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (ℑ‘(i ·
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))))) |
167 | 166, 163 | eqtr3d 2778 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) =
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) |
168 | 167 | eqeq1d 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)) |
170 | 21, 169 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0 ↔ (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0)) |
171 | | half0 12380 |
. . . . . . . . 9
⊢
(((abs‘𝐴) +
(ℜ‘𝐴)) ∈
ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0 ↔ ((abs‘𝐴) + (ℜ‘𝐴)) = 0)) |
172 | 55, 171 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2) = 0
↔ ((abs‘𝐴) +
(ℜ‘𝐴)) =
0)) |
173 | 49, 50 | addcomd 11357 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) +
(ℜ‘𝐴)) =
((ℜ‘𝐴) +
(abs‘𝐴))) |
174 | 173 | eqeq1d 2738 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) +
(ℜ‘𝐴)) = 0
↔ ((ℜ‘𝐴) +
(abs‘𝐴)) =
0)) |
175 | | addeq0 11578 |
. . . . . . . . 9
⊢
(((ℜ‘𝐴)
∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) →
(((ℜ‘𝐴) +
(abs‘𝐴)) = 0 ↔
(ℜ‘𝐴) =
-(abs‘𝐴))) |
176 | 50, 49, 175 | syl2anc 584 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(((ℜ‘𝐴) +
(abs‘𝐴)) = 0 ↔
(ℜ‘𝐴) =
-(abs‘𝐴))) |
177 | 172, 174,
176 | 3bitrd 304 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2) = 0
↔ (ℜ‘𝐴) =
-(abs‘𝐴))) |
178 | 168, 170,
177 | 3bitrd 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)) |
181 | 180 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(((ℜ‘𝐴)↑2)
= ((abs‘𝐴)↑2)
↔ ((abs‘𝐴)↑2) = ((ℜ‘𝐴)↑2))) |
182 | | sqeqor 14120 |
. . . . . . . . . 10
⊢
(((ℜ‘𝐴)
∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) →
(((ℜ‘𝐴)↑2)
= ((abs‘𝐴)↑2)
↔ ((ℜ‘𝐴) =
(abs‘𝐴) ∨
(ℜ‘𝐴) =
-(abs‘𝐴)))) |
183 | 50, 49, 182 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(((ℜ‘𝐴)↑2)
= ((abs‘𝐴)↑2)
↔ ((ℜ‘𝐴) =
(abs‘𝐴) ∨
(ℜ‘𝐴) =
-(abs‘𝐴)))) |
184 | 103 | eqeq1d 2738 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴)↑2) =
((ℜ‘𝐴)↑2)
↔ (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) =
((ℜ‘𝐴)↑2))) |
185 | | addid0 11574 |
. . . . . . . . . . 11
⊢
((((ℜ‘𝐴)↑2) ∈ ℂ ∧
((ℑ‘𝐴)↑2)
∈ ℂ) → ((((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) =
((ℜ‘𝐴)↑2)
↔ ((ℑ‘𝐴)↑2) = 0)) |
186 | 99, 102, 185 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
((((ℜ‘𝐴)↑2)
+ ((ℑ‘𝐴)↑2)) = ((ℜ‘𝐴)↑2) ↔
((ℑ‘𝐴)↑2)
= 0)) |
187 | | sqeq0 14025 |
. . . . . . . . . . 11
⊢
((ℑ‘𝐴)
∈ ℂ → (((ℑ‘𝐴)↑2) = 0 ↔ (ℑ‘𝐴) = 0)) |
188 | 130, 187 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(((ℑ‘𝐴)↑2)
= 0 ↔ (ℑ‘𝐴) = 0)) |
189 | 184, 186,
188 | 3bitrd 304 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴)↑2) =
((ℜ‘𝐴)↑2)
↔ (ℑ‘𝐴) =
0)) |
190 | 181, 183,
189 | 3bitr3d 308 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(((ℜ‘𝐴) =
(abs‘𝐴) ∨
(ℜ‘𝐴) =
-(abs‘𝐴)) ↔
(ℑ‘𝐴) =
0)) |
191 | 179, 190 | imbitrid 243 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((ℜ‘𝐴) =
-(abs‘𝐴) →
(ℑ‘𝐴) =
0)) |
192 | 191 | ancld 551 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
((ℜ‘𝐴) =
-(abs‘𝐴) →
((ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) =
0))) |
193 | 178, 192 | sylbid 239 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
((ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = 0 →
((ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) =
0))) |
194 | | simp2 1137 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (ℜ‘𝐴) =
-(abs‘𝐴)) |
195 | 194 | oveq2d 7373 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((abs‘𝐴) +
(ℜ‘𝐴)) =
((abs‘𝐴) +
-(abs‘𝐴))) |
196 | 49 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (abs‘𝐴) ∈
ℂ) |
197 | 196 | negidd 11502 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((abs‘𝐴) +
-(abs‘𝐴)) =
0) |
198 | 195, 197 | eqtrd 2776 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((abs‘𝐴) +
(ℜ‘𝐴)) =
0) |
199 | 198 | oveq1d 7372 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (((abs‘𝐴) +
(ℜ‘𝐴)) / 2) = (0
/ 2)) |
200 | | 2cn 12228 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℂ |
201 | 200, 58 | div0i 11889 |
. . . . . . . . . . . . . . . 16
⊢ (0 / 2) =
0 |
202 | 199, 201 | eqtrdi 2792 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (((abs‘𝐴) +
(ℜ‘𝐴)) / 2) =
0) |
203 | 202 | fveq2d 6846 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) =
(√‘0)) |
204 | | sqrt0 15126 |
. . . . . . . . . . . . . 14
⊢
(√‘0) = 0 |
205 | 203, 204 | eqtrdi 2792 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0) |
206 | | simp3 1138 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (ℑ‘𝐴) =
0) |
207 | | 0red 11158 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ 0 ∈ ℝ) |
208 | 207 | ltnrd 11289 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ¬ 0 < 0) |
209 | 206, 208 | eqnbrtrd 5123 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ¬ (ℑ‘𝐴) < 0) |
210 | 209 | iffalsed 4497 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ if((ℑ‘𝐴)
< 0, -1, 1) = 1) |
211 | 194 | oveq2d 7373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((abs‘𝐴)
− (ℜ‘𝐴)) =
((abs‘𝐴) −
-(abs‘𝐴))) |
212 | 49, 49 | subnegd 11519 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) −
-(abs‘𝐴)) =
((abs‘𝐴) +
(abs‘𝐴))) |
213 | 49 | 2timesd 12396 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ ℂ → (2
· (abs‘𝐴)) =
((abs‘𝐴) +
(abs‘𝐴))) |
214 | 212, 213 | eqtr4d 2779 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) −
-(abs‘𝐴)) = (2
· (abs‘𝐴))) |
215 | 214 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((abs‘𝐴)
− -(abs‘𝐴)) =
(2 · (abs‘𝐴))) |
216 | 211, 215 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((abs‘𝐴)
− (ℜ‘𝐴)) =
(2 · (abs‘𝐴))) |
217 | 216 | oveq1d 7372 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (((abs‘𝐴)
− (ℜ‘𝐴)) /
2) = ((2 · (abs‘𝐴)) / 2)) |
218 | 49, 57, 59 | divcan3d 11936 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ → ((2
· (abs‘𝐴)) /
2) = (abs‘𝐴)) |
219 | 218 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((2 · (abs‘𝐴)) / 2) = (abs‘𝐴)) |
220 | 217, 219 | eqtrd 2776 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (((abs‘𝐴)
− (ℜ‘𝐴)) /
2) = (abs‘𝐴)) |
221 | 220 | fveq2d 6846 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = (√‘(abs‘𝐴))) |
222 | 210, 221 | oveq12d 7375 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (1 ·
(√‘(abs‘𝐴)))) |
223 | | absge0 15172 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ → 0 ≤
(abs‘𝐴)) |
224 | 17, 223 | resqrtcld 15302 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
(√‘(abs‘𝐴)) ∈ ℝ) |
225 | 224 | recnd 11183 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ →
(√‘(abs‘𝐴)) ∈ ℂ) |
226 | 225 | mulid2d 11173 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → (1
· (√‘(abs‘𝐴))) = (√‘(abs‘𝐴))) |
227 | 226 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (1 · (√‘(abs‘𝐴))) = (√‘(abs‘𝐴))) |
228 | 222, 227 | eqtrd 2776 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (√‘(abs‘𝐴))) |
229 | 228 | oveq2d 7373 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (i · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (i ·
(√‘(abs‘𝐴)))) |
230 | 205, 229 | oveq12d 7375 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (0 + (i ·
(√‘(abs‘𝐴))))) |
231 | 4, 225 | mulcld 11175 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → (i
· (√‘(abs‘𝐴))) ∈ ℂ) |
232 | 231 | 3ad2ant1 1133 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (i · (√‘(abs‘𝐴))) ∈ ℂ) |
233 | 232 | addid2d 11356 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (0 + (i · (√‘(abs‘𝐴)))) = (i ·
(√‘(abs‘𝐴)))) |
234 | 230, 233 | eqtrd 2776 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (i ·
(√‘(abs‘𝐴)))) |
235 | 234 | oveq2d 7373 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (i · (i ·
(√‘(abs‘𝐴))))) |
236 | | ixi 11784 |
. . . . . . . . . . . . . 14
⊢ (i
· i) = -1 |
237 | 236 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (i
· i) = -1) |
238 | 237 | oveq1d 7372 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → ((i
· i) · (√‘(abs‘𝐴))) = (-1 ·
(√‘(abs‘𝐴)))) |
239 | 4, 4, 225 | mulassd 11178 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → ((i
· i) · (√‘(abs‘𝐴))) = (i · (i ·
(√‘(abs‘𝐴))))) |
240 | 225 | mulm1d 11607 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (-1
· (√‘(abs‘𝐴))) = -(√‘(abs‘𝐴))) |
241 | 238, 239,
240 | 3eqtr3d 2784 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (i
· (i · (√‘(abs‘𝐴)))) = -(√‘(abs‘𝐴))) |
242 | 241 | 3ad2ant1 1133 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (i · (i · (√‘(abs‘𝐴)))) = -(√‘(abs‘𝐴))) |
243 | 235, 242 | eqtrd 2776 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) =
-(√‘(abs‘𝐴))) |
244 | 243 | fveq2d 6846 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) =
(ℜ‘-(√‘(abs‘𝐴)))) |
245 | 224 | renegcld 11582 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
-(√‘(abs‘𝐴)) ∈ ℝ) |
246 | 245 | rered 15109 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(ℜ‘-(√‘(abs‘𝐴))) = -(√‘(abs‘𝐴))) |
247 | 246 | 3ad2ant1 1133 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (ℜ‘-(√‘(abs‘𝐴))) = -(√‘(abs‘𝐴))) |
248 | 244, 247 | eqtrd 2776 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) =
-(√‘(abs‘𝐴))) |
249 | 17, 223 | sqrtge0d 15305 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → 0 ≤
(√‘(abs‘𝐴))) |
250 | 224 | le0neg2d 11727 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (0 ≤
(√‘(abs‘𝐴)) ↔ -(√‘(abs‘𝐴)) ≤ 0)) |
251 | 249, 250 | mpbid 231 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
-(√‘(abs‘𝐴)) ≤ 0) |
252 | 251 | 3ad2ant1 1133 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ -(√‘(abs‘𝐴)) ≤ 0) |
253 | 248, 252 | eqbrtrd 5127 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) ≤ 0) |
254 | 253 | 3expib 1122 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(((ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) ≤ 0)) |
255 | 193, 254 | syld 47 |
. . . 4
⊢ (𝐴 ∈ ℂ →
((ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = 0 → (ℜ‘(i
· ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) ≤ 0)) |
256 | 4, 13 | mulcld 11175 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (i
· ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈
ℂ) |
257 | 256 | sqrtcvallem1 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)))))) ∈
ℝ+)) |
258 | 255, 257 | mpbid 231 |
. . 3
⊢ (𝐴 ∈ ℂ → ¬ (i
· ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈
ℝ+) |
259 | 13, 14, 161, 164, 258 | eqsqrtd 15252 |
. 2
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (√‘𝐴)) |
260 | 259 | eqcomd 2742 |
1
⊢ (𝐴 ∈ ℂ →
(√‘𝐴) =
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) |