Proof of Theorem sqrtcval
Step | Hyp | Ref
| Expression |
1 | | sqrtcvallem5 40698 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ∈ ℝ) |
2 | 1 | recnd 10692 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ∈ ℂ) |
3 | | ax-icn 10619 |
. . . . . 6
⊢ i ∈
ℂ |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℂ → i ∈
ℂ) |
5 | | neg1rr 11774 |
. . . . . . . . 9
⊢ -1 ∈
ℝ |
6 | | 1re 10664 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
7 | 5, 6 | ifcli 4460 |
. . . . . . . 8
⊢
if((ℑ‘𝐴)
< 0, -1, 1) ∈ ℝ |
8 | 7 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
if((ℑ‘𝐴) <
0, -1, 1) ∈ ℝ) |
9 | | sqrtcvallem3 40696 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) ∈ ℝ) |
10 | 8, 9 | remulcld 10694 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) ∈ ℝ) |
11 | 10 | recnd 10692 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) ∈ ℂ) |
12 | 4, 11 | mulcld 10684 |
. . . 4
⊢ (𝐴 ∈ ℂ → (i
· (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) ∈ ℂ) |
13 | 2, 12 | addcld 10683 |
. . 3
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) ∈ ℂ) |
14 | | id 22 |
. . 3
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) |
15 | | binom2 13614 |
. . . . 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 588 |
. . . 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 14671 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
18 | | recl 14502 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) |
19 | 17, 18 | readdcld 10693 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) +
(ℜ‘𝐴)) ∈
ℝ) |
20 | 19 | rehalfcld 11906 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) +
(ℜ‘𝐴)) / 2)
∈ ℝ) |
21 | 20 | recnd 10692 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) +
(ℜ‘𝐴)) / 2)
∈ ℂ) |
22 | 21 | sqsqrtd 14832 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) = (((abs‘𝐴) + (ℜ‘𝐴)) / 2)) |
23 | 4, 11 | sqmuld 13557 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((i
· (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) = ((i↑2) ·
((if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2))) |
24 | | i2 13600 |
. . . . . . . . . . 11
⊢
(i↑2) = -1 |
25 | 24 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(i↑2) = -1) |
26 | 8 | recnd 10692 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
if((ℑ‘𝐴) <
0, -1, 1) ∈ ℂ) |
27 | 9 | recnd 10692 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) ∈ ℂ) |
28 | 26, 27 | sqmuld 13557 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
((if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2) =
((if((ℑ‘𝐴) <
0, -1, 1)↑2) · ((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2))) |
29 | | ovif 7238 |
. . . . . . . . . . . . . 14
⊢
(if((ℑ‘𝐴) < 0, -1, 1)↑2) =
if((ℑ‘𝐴) <
0, (-1↑2), (1↑2)) |
30 | | neg1sqe1 13594 |
. . . . . . . . . . . . . . 15
⊢
(-1↑2) = 1 |
31 | | sq1 13593 |
. . . . . . . . . . . . . . 15
⊢
(1↑2) = 1 |
32 | | ifeq12 4431 |
. . . . . . . . . . . . . . 15
⊢
(((-1↑2) = 1 ∧ (1↑2) = 1) → if((ℑ‘𝐴) < 0, (-1↑2),
(1↑2)) = if((ℑ‘𝐴) < 0, 1, 1)) |
33 | 30, 31, 32 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢
if((ℑ‘𝐴)
< 0, (-1↑2), (1↑2)) = if((ℑ‘𝐴) < 0, 1, 1) |
34 | | ifid 4453 |
. . . . . . . . . . . . . 14
⊢
if((ℑ‘𝐴)
< 0, 1, 1) = 1 |
35 | 29, 33, 34 | 3eqtri 2786 |
. . . . . . . . . . . . 13
⊢
(if((ℑ‘𝐴) < 0, -1, 1)↑2) =
1 |
36 | 35 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(if((ℑ‘𝐴) <
0, -1, 1)↑2) = 1) |
37 | 17, 18 | resubcld 11091 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) −
(ℜ‘𝐴)) ∈
ℝ) |
38 | 37 | rehalfcld 11906 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) −
(ℜ‘𝐴)) / 2)
∈ ℝ) |
39 | 38 | recnd 10692 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) −
(ℜ‘𝐴)) / 2)
∈ ℂ) |
40 | 39 | sqsqrtd 14832 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2) = (((abs‘𝐴) − (ℜ‘𝐴)) / 2)) |
41 | 36, 40 | oveq12d 7161 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
((if((ℑ‘𝐴) <
0, -1, 1)↑2) · ((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2)) = (1 ·
(((abs‘𝐴) −
(ℜ‘𝐴)) /
2))) |
42 | 39 | mulid2d 10682 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (1
· (((abs‘𝐴)
− (ℜ‘𝐴)) /
2)) = (((abs‘𝐴)
− (ℜ‘𝐴)) /
2)) |
43 | 28, 41, 42 | 3eqtrd 2798 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
((if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2) = (((abs‘𝐴) − (ℜ‘𝐴)) / 2)) |
44 | 25, 43 | oveq12d 7161 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
((i↑2) · ((if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2)) = (-1 ·
(((abs‘𝐴) −
(ℜ‘𝐴)) /
2))) |
45 | 39 | mulm1d 11115 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (-1
· (((abs‘𝐴)
− (ℜ‘𝐴)) /
2)) = -(((abs‘𝐴)
− (ℜ‘𝐴)) /
2)) |
46 | 23, 44, 45 | 3eqtrd 2798 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((i
· (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) = -(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) |
47 | 22, 46 | oveq12d 7161 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) + ((i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2)) = ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) + -(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) |
48 | 21, 39 | negsubd 11026 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2) +
-(((abs‘𝐴) −
(ℜ‘𝐴)) / 2)) =
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2)
− (((abs‘𝐴)
− (ℜ‘𝐴)) /
2))) |
49 | 17 | recnd 10692 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℂ) |
50 | 18 | recnd 10692 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℂ) |
51 | 49, 50, 50 | pnncand 11059 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) +
(ℜ‘𝐴)) −
((abs‘𝐴) −
(ℜ‘𝐴))) =
((ℜ‘𝐴) +
(ℜ‘𝐴))) |
52 | 50 | 2timesd 11902 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (2
· (ℜ‘𝐴))
= ((ℜ‘𝐴) +
(ℜ‘𝐴))) |
53 | 51, 52 | eqtr4d 2797 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) +
(ℜ‘𝐴)) −
((abs‘𝐴) −
(ℜ‘𝐴))) = (2
· (ℜ‘𝐴))) |
54 | 53 | oveq1d 7158 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
((((abs‘𝐴) +
(ℜ‘𝐴)) −
((abs‘𝐴) −
(ℜ‘𝐴))) / 2) =
((2 · (ℜ‘𝐴)) / 2)) |
55 | 19 | recnd 10692 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) +
(ℜ‘𝐴)) ∈
ℂ) |
56 | 37 | recnd 10692 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) −
(ℜ‘𝐴)) ∈
ℂ) |
57 | | 2cnd 11737 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → 2 ∈
ℂ) |
58 | | 2ne0 11763 |
. . . . . . . . . 10
⊢ 2 ≠
0 |
59 | 58 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → 2 ≠
0) |
60 | 55, 56, 57, 59 | divsubdird 11478 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
((((abs‘𝐴) +
(ℜ‘𝐴)) −
((abs‘𝐴) −
(ℜ‘𝐴))) / 2) =
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2)
− (((abs‘𝐴)
− (ℜ‘𝐴)) /
2))) |
61 | 50, 57, 59 | divcan3d 11444 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((2
· (ℜ‘𝐴))
/ 2) = (ℜ‘𝐴)) |
62 | 54, 60, 61 | 3eqtr3d 2802 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2)
− (((abs‘𝐴)
− (ℜ‘𝐴)) /
2)) = (ℜ‘𝐴)) |
63 | 47, 48, 62 | 3eqtrd 2798 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) + ((i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2)) = (ℜ‘𝐴)) |
64 | 57, 2 | mulcld 10684 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (2
· (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) ∈ ℂ) |
65 | 64, 4, 11 | mul12d 10872 |
. . . . . . 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 10687 |
. . . . . . 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 10687 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((2
· (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (2 ·
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) |
68 | 2, 26, 27 | mul12d 10872 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (if((ℑ‘𝐴) < 0, -1, 1) ·
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) |
69 | | sqrtcvallem4 40697 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → 0 ≤
(((abs‘𝐴) +
(ℜ‘𝐴)) /
2)) |
70 | | halfnneg2 11890 |
. . . . . . . . . . . . . . . . 17
⊢
(((abs‘𝐴) +
(ℜ‘𝐴)) ∈
ℝ → (0 ≤ ((abs‘𝐴) + (ℜ‘𝐴)) ↔ 0 ≤ (((abs‘𝐴) + (ℜ‘𝐴)) / 2))) |
71 | 19, 70 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → (0 ≤
((abs‘𝐴) +
(ℜ‘𝐴)) ↔ 0
≤ (((abs‘𝐴) +
(ℜ‘𝐴)) /
2))) |
72 | 69, 71 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → 0 ≤
((abs‘𝐴) +
(ℜ‘𝐴))) |
73 | | 2rp 12420 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ+ |
74 | 73 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → 2 ∈
ℝ+) |
75 | 19, 72, 74 | sqrtdivd 14816 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = ((√‘((abs‘𝐴) + (ℜ‘𝐴))) /
(√‘2))) |
76 | | sqrtcvallem2 40695 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → 0 ≤
(((abs‘𝐴) −
(ℜ‘𝐴)) /
2)) |
77 | | halfnneg2 11890 |
. . . . . . . . . . . . . . . . 17
⊢
(((abs‘𝐴)
− (ℜ‘𝐴))
∈ ℝ → (0 ≤ ((abs‘𝐴) − (ℜ‘𝐴)) ↔ 0 ≤ (((abs‘𝐴) − (ℜ‘𝐴)) / 2))) |
78 | 37, 77 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → (0 ≤
((abs‘𝐴) −
(ℜ‘𝐴)) ↔ 0
≤ (((abs‘𝐴)
− (ℜ‘𝐴)) /
2))) |
79 | 76, 78 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → 0 ≤
((abs‘𝐴) −
(ℜ‘𝐴))) |
80 | 37, 79, 74 | sqrtdivd 14816 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = ((√‘((abs‘𝐴) − (ℜ‘𝐴))) /
(√‘2))) |
81 | 75, 80 | oveq12d 7161 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) =
(((√‘((abs‘𝐴) + (ℜ‘𝐴))) / (√‘2)) ·
((√‘((abs‘𝐴) − (ℜ‘𝐴))) / (√‘2)))) |
82 | 19, 72 | resqrtcld 14810 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(√‘((abs‘𝐴) + (ℜ‘𝐴))) ∈ ℝ) |
83 | 82 | recnd 10692 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(√‘((abs‘𝐴) + (ℜ‘𝐴))) ∈ ℂ) |
84 | | 2re 11733 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ |
85 | 84 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → 2 ∈
ℝ) |
86 | | 0le2 11761 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ≤
2 |
87 | 86 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → 0 ≤
2) |
88 | 85, 87 | resqrtcld 14810 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(√‘2) ∈ ℝ) |
89 | 88 | recnd 10692 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(√‘2) ∈ ℂ) |
90 | 37, 79 | resqrtcld 14810 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(√‘((abs‘𝐴) − (ℜ‘𝐴))) ∈ ℝ) |
91 | 90 | recnd 10692 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(√‘((abs‘𝐴) − (ℜ‘𝐴))) ∈ ℂ) |
92 | | sqrt00 14656 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℝ ∧ 0 ≤ 2) → ((√‘2) = 0 ↔ 2 =
0)) |
93 | 84, 86, 92 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢
((√‘2) = 0 ↔ 2 = 0) |
94 | 93 | necon3bii 3001 |
. . . . . . . . . . . . . . . 16
⊢
((√‘2) ≠ 0 ↔ 2 ≠ 0) |
95 | 58, 94 | mpbir 234 |
. . . . . . . . . . . . . . 15
⊢
(√‘2) ≠ 0 |
96 | 95 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(√‘2) ≠ 0) |
97 | 83, 89, 91, 89, 96, 96 | divmuldivd 11480 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
(((√‘((abs‘𝐴) + (ℜ‘𝐴))) / (√‘2)) ·
((√‘((abs‘𝐴) − (ℜ‘𝐴))) / (√‘2))) =
(((√‘((abs‘𝐴) + (ℜ‘𝐴))) ·
(√‘((abs‘𝐴) − (ℜ‘𝐴)))) / ((√‘2) ·
(√‘2)))) |
98 | 18 | resqcld 13646 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ →
((ℜ‘𝐴)↑2)
∈ ℝ) |
99 | 98 | recnd 10692 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
((ℜ‘𝐴)↑2)
∈ ℂ) |
100 | | imcl 14503 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℝ) |
101 | 100 | resqcld 13646 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ →
((ℑ‘𝐴)↑2)
∈ ℝ) |
102 | 101 | recnd 10692 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
((ℑ‘𝐴)↑2)
∈ ℂ) |
103 | | absvalsq2 14674 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴)↑2) =
(((ℜ‘𝐴)↑2)
+ ((ℑ‘𝐴)↑2))) |
104 | 99, 102, 103 | mvrladdd 11076 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴)↑2)
− ((ℜ‘𝐴)↑2)) = ((ℑ‘𝐴)↑2)) |
105 | | subsq 13607 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘𝐴)
∈ ℂ ∧ (ℜ‘𝐴) ∈ ℂ) → (((abs‘𝐴)↑2) −
((ℜ‘𝐴)↑2))
= (((abs‘𝐴) +
(ℜ‘𝐴)) ·
((abs‘𝐴) −
(ℜ‘𝐴)))) |
106 | 49, 50, 105 | syl2anc 588 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴)↑2)
− ((ℜ‘𝐴)↑2)) = (((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴)))) |
107 | 104, 106 | eqtr3d 2796 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ →
((ℑ‘𝐴)↑2)
= (((abs‘𝐴) +
(ℜ‘𝐴)) ·
((abs‘𝐴) −
(ℜ‘𝐴)))) |
108 | 107 | fveq2d 6655 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(√‘((ℑ‘𝐴)↑2)) =
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴))))) |
109 | 100 | absred 14809 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ →
(abs‘(ℑ‘𝐴)) = (√‘((ℑ‘𝐴)↑2))) |
110 | | reabsifneg 40690 |
. . . . . . . . . . . . . . . . 17
⊢
((ℑ‘𝐴)
∈ ℝ → (abs‘(ℑ‘𝐴)) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) |
111 | 100, 110 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ →
(abs‘(ℑ‘𝐴)) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) |
112 | 109, 111 | eqtr3d 2796 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(√‘((ℑ‘𝐴)↑2)) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) |
113 | 19, 72, 37, 79 | sqrtmuld 14817 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴)))) = ((√‘((abs‘𝐴) + (ℜ‘𝐴))) ·
(√‘((abs‘𝐴) − (ℜ‘𝐴))))) |
114 | 108, 112,
113 | 3eqtr3rd 2803 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
((√‘((abs‘𝐴) + (ℜ‘𝐴))) ·
(√‘((abs‘𝐴) − (ℜ‘𝐴)))) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) |
115 | | remsqsqrt 14649 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℝ ∧ 0 ≤ 2) → ((√‘2) ·
(√‘2)) = 2) |
116 | 84, 86, 115 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢
((√‘2) · (√‘2)) = 2 |
117 | 116 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
((√‘2) · (√‘2)) = 2) |
118 | 114, 117 | oveq12d 7161 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
(((√‘((abs‘𝐴) + (ℜ‘𝐴))) ·
(√‘((abs‘𝐴) − (ℜ‘𝐴)))) / ((√‘2) ·
(√‘2))) = (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)) |
119 | 81, 97, 118 | 3eqtrd 2798 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)) |
120 | 119 | oveq2d 7159 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(if((ℑ‘𝐴) <
0, -1, 1) · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (if((ℑ‘𝐴) < 0, -1, 1) ·
(if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴)) /
2))) |
121 | 68, 120 | eqtrd 2794 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (if((ℑ‘𝐴) < 0, -1, 1) ·
(if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴)) /
2))) |
122 | 121 | oveq2d 7159 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (2
· ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (2 ·
(if((ℑ‘𝐴) <
0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)))) |
123 | 100 | renegcld 11090 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
-(ℑ‘𝐴) ∈
ℝ) |
124 | 123, 100 | ifcld 4459 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴)) ∈
ℝ) |
125 | 124 | recnd 10692 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴)) ∈
ℂ) |
126 | 26, 125, 57, 59 | divassd 11474 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
((if((ℑ‘𝐴) <
0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) / 2) = (if((ℑ‘𝐴) < 0, -1, 1) ·
(if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴)) /
2))) |
127 | | ovif12 7240 |
. . . . . . . . . . . . . 14
⊢
(if((ℑ‘𝐴) < 0, -1, 1) ·
if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴))) =
if((ℑ‘𝐴) <
0, (-1 · -(ℑ‘𝐴)), (1 · (ℑ‘𝐴))) |
128 | 5 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ → -1 ∈
ℝ) |
129 | 128 | recnd 10692 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ → -1 ∈
ℂ) |
130 | 100 | recnd 10692 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℂ) |
131 | 129, 129,
130 | mulassd 10687 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ → ((-1
· -1) · (ℑ‘𝐴)) = (-1 · (-1 ·
(ℑ‘𝐴)))) |
132 | | neg1mulneg1e1 11872 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (-1
· -1) = 1 |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ → (-1
· -1) = 1) |
134 | 133 | oveq1d 7158 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ → ((-1
· -1) · (ℑ‘𝐴)) = (1 · (ℑ‘𝐴))) |
135 | 130 | mulid2d 10682 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ → (1
· (ℑ‘𝐴))
= (ℑ‘𝐴)) |
136 | 134, 135 | eqtrd 2794 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ → ((-1
· -1) · (ℑ‘𝐴)) = (ℑ‘𝐴)) |
137 | 130 | mulm1d 11115 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ → (-1
· (ℑ‘𝐴))
= -(ℑ‘𝐴)) |
138 | 137 | oveq2d 7159 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ → (-1
· (-1 · (ℑ‘𝐴))) = (-1 · -(ℑ‘𝐴))) |
139 | 131, 136,
138 | 3eqtr3rd 2803 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → (-1
· -(ℑ‘𝐴)) = (ℑ‘𝐴)) |
140 | 139 | adantr 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) < 0)
→ (-1 · -(ℑ‘𝐴)) = (ℑ‘𝐴)) |
141 | 135 | adantr 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ ¬
(ℑ‘𝐴) < 0)
→ (1 · (ℑ‘𝐴)) = (ℑ‘𝐴)) |
142 | 140, 141 | ifeqda 4449 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
if((ℑ‘𝐴) <
0, (-1 · -(ℑ‘𝐴)), (1 · (ℑ‘𝐴))) = (ℑ‘𝐴)) |
143 | 127, 142 | syl5eq 2806 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
(if((ℑ‘𝐴) <
0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) = (ℑ‘𝐴)) |
144 | 143 | oveq1d 7158 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
((if((ℑ‘𝐴) <
0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) / 2) = ((ℑ‘𝐴) / 2)) |
145 | 126, 144 | eqtr3d 2796 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(if((ℑ‘𝐴) <
0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)) = ((ℑ‘𝐴) / 2)) |
146 | 145 | oveq2d 7159 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (2
· (if((ℑ‘𝐴) < 0, -1, 1) ·
(if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴)) / 2))) =
(2 · ((ℑ‘𝐴) / 2))) |
147 | 130, 57, 59 | divcan2d 11441 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (2
· ((ℑ‘𝐴)
/ 2)) = (ℑ‘𝐴)) |
148 | 146, 147 | eqtrd 2794 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (2
· (if((ℑ‘𝐴) < 0, -1, 1) ·
(if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴)) / 2))) =
(ℑ‘𝐴)) |
149 | 67, 122, 148 | 3eqtrd 2798 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((2
· (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (ℑ‘𝐴)) |
150 | 149 | oveq2d 7159 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (i
· ((2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (i ·
(ℑ‘𝐴))) |
151 | 65, 66, 150 | 3eqtr3d 2802 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (2
· ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (i ·
(ℑ‘𝐴))) |
152 | 63, 151 | oveq12d 7161 |
. . . . 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 13646 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) ∈
ℝ) |
154 | 153 | recnd 10692 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) ∈
ℂ) |
155 | 2, 12 | mulcld 10684 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) ∈ ℂ) |
156 | 57, 155 | mulcld 10684 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (2
· ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈
ℂ) |
157 | 12 | sqcld 13543 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → ((i
· (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) ∈
ℂ) |
158 | 154, 156,
157 | add32d 10890 |
. . . . 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 14508 |
. . . . 5
⊢ (𝐴 ∈ ℂ → 𝐴 = ((ℜ‘𝐴) + (i ·
(ℑ‘𝐴)))) |
160 | 152, 158,
159 | 3eqtr4d 2804 |
. . . 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 2794 |
. . 3
⊢ (𝐴 ∈ ℂ →
(((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))↑2) = 𝐴) |
162 | 20, 69 | sqrtge0d 14813 |
. . . 4
⊢ (𝐴 ∈ ℂ → 0 ≤
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) |
163 | 1, 10 | crred 14623 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(ℜ‘((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) =
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) |
164 | 162, 163 | breqtrrd 5053 |
. . 3
⊢ (𝐴 ∈ ℂ → 0 ≤
(ℜ‘((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) |
165 | | reim 14501 |
. . . . . . . . . 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 2796 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) =
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) |
168 | 167 | eqeq1d 2761 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = 0 ↔
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0)) |
169 | | cnsqrt00 14785 |
. . . . . . . 8
⊢
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2)
∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0 ↔ (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0)) |
170 | 21, 169 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0 ↔ (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0)) |
171 | | half0 11886 |
. . . . . . . . 9
⊢
(((abs‘𝐴) +
(ℜ‘𝐴)) ∈
ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0 ↔ ((abs‘𝐴) + (ℜ‘𝐴)) = 0)) |
172 | 55, 171 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2) = 0
↔ ((abs‘𝐴) +
(ℜ‘𝐴)) =
0)) |
173 | 49, 50 | addcomd 10865 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) +
(ℜ‘𝐴)) =
((ℜ‘𝐴) +
(abs‘𝐴))) |
174 | 173 | eqeq1d 2761 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) +
(ℜ‘𝐴)) = 0
↔ ((ℜ‘𝐴) +
(abs‘𝐴)) =
0)) |
175 | | addeq0 11086 |
. . . . . . . . 9
⊢
(((ℜ‘𝐴)
∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) →
(((ℜ‘𝐴) +
(abs‘𝐴)) = 0 ↔
(ℜ‘𝐴) =
-(abs‘𝐴))) |
176 | 50, 49, 175 | syl2anc 588 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(((ℜ‘𝐴) +
(abs‘𝐴)) = 0 ↔
(ℜ‘𝐴) =
-(abs‘𝐴))) |
177 | 172, 174,
176 | 3bitrd 309 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2) = 0
↔ (ℜ‘𝐴) =
-(abs‘𝐴))) |
178 | 168, 170,
177 | 3bitrd 309 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
((ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = 0 ↔ (ℜ‘𝐴) = -(abs‘𝐴))) |
179 | | olc 866 |
. . . . . . . 8
⊢
((ℜ‘𝐴) =
-(abs‘𝐴) →
((ℜ‘𝐴) =
(abs‘𝐴) ∨
(ℜ‘𝐴) =
-(abs‘𝐴))) |
180 | | eqcom 2766 |
. . . . . . . . . 10
⊢
(((ℜ‘𝐴)↑2) = ((abs‘𝐴)↑2) ↔ ((abs‘𝐴)↑2) = ((ℜ‘𝐴)↑2)) |
181 | 180 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(((ℜ‘𝐴)↑2)
= ((abs‘𝐴)↑2)
↔ ((abs‘𝐴)↑2) = ((ℜ‘𝐴)↑2))) |
182 | | sqeqor 13613 |
. . . . . . . . . 10
⊢
(((ℜ‘𝐴)
∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) →
(((ℜ‘𝐴)↑2)
= ((abs‘𝐴)↑2)
↔ ((ℜ‘𝐴) =
(abs‘𝐴) ∨
(ℜ‘𝐴) =
-(abs‘𝐴)))) |
183 | 50, 49, 182 | syl2anc 588 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(((ℜ‘𝐴)↑2)
= ((abs‘𝐴)↑2)
↔ ((ℜ‘𝐴) =
(abs‘𝐴) ∨
(ℜ‘𝐴) =
-(abs‘𝐴)))) |
184 | 103 | eqeq1d 2761 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴)↑2) =
((ℜ‘𝐴)↑2)
↔ (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) =
((ℜ‘𝐴)↑2))) |
185 | | addid0 11082 |
. . . . . . . . . . 11
⊢
((((ℜ‘𝐴)↑2) ∈ ℂ ∧
((ℑ‘𝐴)↑2)
∈ ℂ) → ((((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) =
((ℜ‘𝐴)↑2)
↔ ((ℑ‘𝐴)↑2) = 0)) |
186 | 99, 102, 185 | syl2anc 588 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
((((ℜ‘𝐴)↑2)
+ ((ℑ‘𝐴)↑2)) = ((ℜ‘𝐴)↑2) ↔
((ℑ‘𝐴)↑2)
= 0)) |
187 | | sqeq0 13521 |
. . . . . . . . . . 11
⊢
((ℑ‘𝐴)
∈ ℂ → (((ℑ‘𝐴)↑2) = 0 ↔ (ℑ‘𝐴) = 0)) |
188 | 130, 187 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(((ℑ‘𝐴)↑2)
= 0 ↔ (ℑ‘𝐴) = 0)) |
189 | 184, 186,
188 | 3bitrd 309 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴)↑2) =
((ℜ‘𝐴)↑2)
↔ (ℑ‘𝐴) =
0)) |
190 | 181, 183,
189 | 3bitr3d 313 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(((ℜ‘𝐴) =
(abs‘𝐴) ∨
(ℜ‘𝐴) =
-(abs‘𝐴)) ↔
(ℑ‘𝐴) =
0)) |
191 | 179, 190 | syl5ib 247 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((ℜ‘𝐴) =
-(abs‘𝐴) →
(ℑ‘𝐴) =
0)) |
192 | 191 | ancld 555 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
((ℜ‘𝐴) =
-(abs‘𝐴) →
((ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) =
0))) |
193 | 178, 192 | sylbid 243 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
((ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = 0 →
((ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) =
0))) |
194 | | simp2 1135 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (ℜ‘𝐴) =
-(abs‘𝐴)) |
195 | 194 | oveq2d 7159 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((abs‘𝐴) +
(ℜ‘𝐴)) =
((abs‘𝐴) +
-(abs‘𝐴))) |
196 | | simp1 1134 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ 𝐴 ∈
ℂ) |
197 | 196, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (abs‘𝐴) ∈
ℂ) |
198 | 197 | negidd 11010 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((abs‘𝐴) +
-(abs‘𝐴)) =
0) |
199 | 195, 198 | eqtrd 2794 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((abs‘𝐴) +
(ℜ‘𝐴)) =
0) |
200 | 199 | oveq1d 7158 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (((abs‘𝐴) +
(ℜ‘𝐴)) / 2) = (0
/ 2)) |
201 | | 2cn 11734 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℂ |
202 | 201, 58 | div0i 11397 |
. . . . . . . . . . . . . . . 16
⊢ (0 / 2) =
0 |
203 | 200, 202 | eqtrdi 2810 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (((abs‘𝐴) +
(ℜ‘𝐴)) / 2) =
0) |
204 | 203 | fveq2d 6655 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) =
(√‘0)) |
205 | | sqrt0 14634 |
. . . . . . . . . . . . . 14
⊢
(√‘0) = 0 |
206 | 204, 205 | eqtrdi 2810 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0) |
207 | | simp3 1136 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (ℑ‘𝐴) =
0) |
208 | | 0red 10667 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ 0 ∈ ℝ) |
209 | 208 | ltnrd 10797 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ¬ 0 < 0) |
210 | 207, 209 | eqnbrtrd 5043 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ¬ (ℑ‘𝐴) < 0) |
211 | 210 | iffalsed 4424 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ if((ℑ‘𝐴)
< 0, -1, 1) = 1) |
212 | 194 | oveq2d 7159 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((abs‘𝐴)
− (ℜ‘𝐴)) =
((abs‘𝐴) −
-(abs‘𝐴))) |
213 | 49, 49 | subnegd 11027 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) −
-(abs‘𝐴)) =
((abs‘𝐴) +
(abs‘𝐴))) |
214 | 49 | 2timesd 11902 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ ℂ → (2
· (abs‘𝐴)) =
((abs‘𝐴) +
(abs‘𝐴))) |
215 | 213, 214 | eqtr4d 2797 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) −
-(abs‘𝐴)) = (2
· (abs‘𝐴))) |
216 | 196, 215 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((abs‘𝐴)
− -(abs‘𝐴)) =
(2 · (abs‘𝐴))) |
217 | 212, 216 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((abs‘𝐴)
− (ℜ‘𝐴)) =
(2 · (abs‘𝐴))) |
218 | 217 | oveq1d 7158 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (((abs‘𝐴)
− (ℜ‘𝐴)) /
2) = ((2 · (abs‘𝐴)) / 2)) |
219 | 49, 57, 59 | divcan3d 11444 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ → ((2
· (abs‘𝐴)) /
2) = (abs‘𝐴)) |
220 | 196, 219 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((2 · (abs‘𝐴)) / 2) = (abs‘𝐴)) |
221 | 218, 220 | eqtrd 2794 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (((abs‘𝐴)
− (ℜ‘𝐴)) /
2) = (abs‘𝐴)) |
222 | 221 | fveq2d 6655 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = (√‘(abs‘𝐴))) |
223 | 211, 222 | oveq12d 7161 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (1 ·
(√‘(abs‘𝐴)))) |
224 | | absge0 14680 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ → 0 ≤
(abs‘𝐴)) |
225 | 17, 224 | resqrtcld 14810 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
(√‘(abs‘𝐴)) ∈ ℝ) |
226 | 225 | recnd 10692 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ →
(√‘(abs‘𝐴)) ∈ ℂ) |
227 | 226 | mulid2d 10682 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → (1
· (√‘(abs‘𝐴))) = (√‘(abs‘𝐴))) |
228 | 196, 227 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (1 · (√‘(abs‘𝐴))) = (√‘(abs‘𝐴))) |
229 | 223, 228 | eqtrd 2794 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (√‘(abs‘𝐴))) |
230 | 229 | oveq2d 7159 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (i · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (i ·
(√‘(abs‘𝐴)))) |
231 | 206, 230 | oveq12d 7161 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (0 + (i ·
(√‘(abs‘𝐴))))) |
232 | 4, 226 | mulcld 10684 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → (i
· (√‘(abs‘𝐴))) ∈ ℂ) |
233 | 196, 232 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (i · (√‘(abs‘𝐴))) ∈ ℂ) |
234 | 233 | addid2d 10864 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (0 + (i · (√‘(abs‘𝐴)))) = (i ·
(√‘(abs‘𝐴)))) |
235 | 231, 234 | eqtrd 2794 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (i ·
(√‘(abs‘𝐴)))) |
236 | 235 | oveq2d 7159 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (i · (i ·
(√‘(abs‘𝐴))))) |
237 | | ixi 11292 |
. . . . . . . . . . . . . 14
⊢ (i
· i) = -1 |
238 | 237 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (i
· i) = -1) |
239 | 238 | oveq1d 7158 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → ((i
· i) · (√‘(abs‘𝐴))) = (-1 ·
(√‘(abs‘𝐴)))) |
240 | 4, 4, 226 | mulassd 10687 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → ((i
· i) · (√‘(abs‘𝐴))) = (i · (i ·
(√‘(abs‘𝐴))))) |
241 | 226 | mulm1d 11115 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (-1
· (√‘(abs‘𝐴))) = -(√‘(abs‘𝐴))) |
242 | 239, 240,
241 | 3eqtr3d 2802 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (i
· (i · (√‘(abs‘𝐴)))) = -(√‘(abs‘𝐴))) |
243 | 196, 242 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (i · (i · (√‘(abs‘𝐴)))) = -(√‘(abs‘𝐴))) |
244 | 236, 243 | eqtrd 2794 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) =
-(√‘(abs‘𝐴))) |
245 | 244 | fveq2d 6655 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) =
(ℜ‘-(√‘(abs‘𝐴)))) |
246 | 225 | renegcld 11090 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
-(√‘(abs‘𝐴)) ∈ ℝ) |
247 | 246 | rered 14616 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(ℜ‘-(√‘(abs‘𝐴))) = -(√‘(abs‘𝐴))) |
248 | 196, 247 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (ℜ‘-(√‘(abs‘𝐴))) = -(√‘(abs‘𝐴))) |
249 | 245, 248 | eqtrd 2794 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) =
-(√‘(abs‘𝐴))) |
250 | 17, 224 | sqrtge0d 14813 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → 0 ≤
(√‘(abs‘𝐴))) |
251 | 225 | le0neg2d 11235 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (0 ≤
(√‘(abs‘𝐴)) ↔ -(√‘(abs‘𝐴)) ≤ 0)) |
252 | 250, 251 | mpbid 235 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
-(√‘(abs‘𝐴)) ≤ 0) |
253 | 196, 252 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ -(√‘(abs‘𝐴)) ≤ 0) |
254 | 249, 253 | eqbrtrd 5047 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) ≤ 0) |
255 | 254 | 3expib 1120 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(((ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) ≤ 0)) |
256 | 193, 255 | 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)) |
257 | 4, 13 | mulcld 10684 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (i
· ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈
ℂ) |
258 | 257 | sqrtcvallem1 40689 |
. . . 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)))))) ∈
ℝ+)) |
259 | 256, 258 | mpbid 235 |
. . 3
⊢ (𝐴 ∈ ℂ → ¬ (i
· ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈
ℝ+) |
260 | 13, 14, 161, 164, 259 | eqsqrtd 14760 |
. 2
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (√‘𝐴)) |
261 | 260 | eqcomd 2765 |
1
⊢ (𝐴 ∈ ℂ →
(√‘𝐴) =
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) |