Proof of Theorem sqrtcval
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sqrtcvallem5 43658 | . . . . 5
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ∈ ℝ) | 
| 2 | 1 | recnd 11290 | . . . 4
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ∈ ℂ) | 
| 3 |  | ax-icn 11215 | . . . . . 6
⊢ i ∈
ℂ | 
| 4 | 3 | a1i 11 | . . . . 5
⊢ (𝐴 ∈ ℂ → i ∈
ℂ) | 
| 5 |  | neg1rr 12382 | . . . . . . . . 9
⊢ -1 ∈
ℝ | 
| 6 |  | 1re 11262 | . . . . . . . . 9
⊢ 1 ∈
ℝ | 
| 7 | 5, 6 | ifcli 4572 | . . . . . . . 8
⊢
if((ℑ‘𝐴)
< 0, -1, 1) ∈ ℝ | 
| 8 | 7 | a1i 11 | . . . . . . 7
⊢ (𝐴 ∈ ℂ →
if((ℑ‘𝐴) <
0, -1, 1) ∈ ℝ) | 
| 9 |  | sqrtcvallem3 43656 | . . . . . . 7
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) ∈ ℝ) | 
| 10 | 8, 9 | remulcld 11292 | . . . . . 6
⊢ (𝐴 ∈ ℂ →
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) ∈ ℝ) | 
| 11 | 10 | recnd 11290 | . . . . 5
⊢ (𝐴 ∈ ℂ →
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) ∈ ℂ) | 
| 12 | 4, 11 | mulcld 11282 | . . . 4
⊢ (𝐴 ∈ ℂ → (i
· (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) ∈ ℂ) | 
| 13 | 2, 12 | addcld 11281 | . . 3
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) ∈ ℂ) | 
| 14 |  | id 22 | . . 3
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) | 
| 15 |  | binom2 14257 | . . . . 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 15318 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) | 
| 18 |  | recl 15150 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) | 
| 19 | 17, 18 | readdcld 11291 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) +
(ℜ‘𝐴)) ∈
ℝ) | 
| 20 | 19 | rehalfcld 12515 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) +
(ℜ‘𝐴)) / 2)
∈ ℝ) | 
| 21 | 20 | recnd 11290 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) +
(ℜ‘𝐴)) / 2)
∈ ℂ) | 
| 22 | 21 | sqsqrtd 15479 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) = (((abs‘𝐴) + (ℜ‘𝐴)) / 2)) | 
| 23 | 4, 11 | sqmuld 14199 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((i
· (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) = ((i↑2) ·
((if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2))) | 
| 24 |  | i2 14242 | . . . . . . . . . . 11
⊢
(i↑2) = -1 | 
| 25 | 24 | a1i 11 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(i↑2) = -1) | 
| 26 | 8 | recnd 11290 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
if((ℑ‘𝐴) <
0, -1, 1) ∈ ℂ) | 
| 27 | 9 | recnd 11290 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) ∈ ℂ) | 
| 28 | 26, 27 | sqmuld 14199 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
((if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2) =
((if((ℑ‘𝐴) <
0, -1, 1)↑2) · ((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2))) | 
| 29 |  | ovif 7532 | . . . . . . . . . . . . . 14
⊢
(if((ℑ‘𝐴) < 0, -1, 1)↑2) =
if((ℑ‘𝐴) <
0, (-1↑2), (1↑2)) | 
| 30 |  | neg1sqe1 14236 | . . . . . . . . . . . . . . 15
⊢
(-1↑2) = 1 | 
| 31 |  | sq1 14235 | . . . . . . . . . . . . . . 15
⊢
(1↑2) = 1 | 
| 32 |  | ifeq12 4543 | . . . . . . . . . . . . . . 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 4565 | . . . . . . . . . . . . . 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 11692 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) −
(ℜ‘𝐴)) ∈
ℝ) | 
| 38 | 37 | rehalfcld 12515 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) −
(ℜ‘𝐴)) / 2)
∈ ℝ) | 
| 39 | 38 | recnd 11290 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) −
(ℜ‘𝐴)) / 2)
∈ ℂ) | 
| 40 | 39 | sqsqrtd 15479 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2) = (((abs‘𝐴) − (ℜ‘𝐴)) / 2)) | 
| 41 | 36, 40 | oveq12d 7450 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
((if((ℑ‘𝐴) <
0, -1, 1)↑2) · ((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2)) = (1 ·
(((abs‘𝐴) −
(ℜ‘𝐴)) /
2))) | 
| 42 | 39 | mullidd 11280 | . . . . . . . . . . 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 7450 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
((i↑2) · ((if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2)) = (-1 ·
(((abs‘𝐴) −
(ℜ‘𝐴)) /
2))) | 
| 45 | 39 | mulm1d 11716 | . . . . . . . . 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 7450 | . . . . . . 7
⊢ (𝐴 ∈ ℂ →
(((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) + ((i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2)) = ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) + -(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) | 
| 48 | 21, 39 | negsubd 11627 | . . . . . . 7
⊢ (𝐴 ∈ ℂ →
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2) +
-(((abs‘𝐴) −
(ℜ‘𝐴)) / 2)) =
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2)
− (((abs‘𝐴)
− (ℜ‘𝐴)) /
2))) | 
| 49 | 17 | recnd 11290 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℂ) | 
| 50 | 18 | recnd 11290 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℂ) | 
| 51 | 49, 50, 50 | pnncand 11660 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) +
(ℜ‘𝐴)) −
((abs‘𝐴) −
(ℜ‘𝐴))) =
((ℜ‘𝐴) +
(ℜ‘𝐴))) | 
| 52 | 50 | 2timesd 12511 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (2
· (ℜ‘𝐴))
= ((ℜ‘𝐴) +
(ℜ‘𝐴))) | 
| 53 | 51, 52 | eqtr4d 2779 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) +
(ℜ‘𝐴)) −
((abs‘𝐴) −
(ℜ‘𝐴))) = (2
· (ℜ‘𝐴))) | 
| 54 | 53 | oveq1d 7447 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ →
((((abs‘𝐴) +
(ℜ‘𝐴)) −
((abs‘𝐴) −
(ℜ‘𝐴))) / 2) =
((2 · (ℜ‘𝐴)) / 2)) | 
| 55 | 19 | recnd 11290 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) +
(ℜ‘𝐴)) ∈
ℂ) | 
| 56 | 37 | recnd 11290 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) −
(ℜ‘𝐴)) ∈
ℂ) | 
| 57 |  | 2cnd 12345 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ → 2 ∈
ℂ) | 
| 58 |  | 2ne0 12371 | . . . . . . . . . 10
⊢ 2 ≠
0 | 
| 59 | 58 | a1i 11 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ → 2 ≠
0) | 
| 60 | 55, 56, 57, 59 | divsubdird 12083 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ →
((((abs‘𝐴) +
(ℜ‘𝐴)) −
((abs‘𝐴) −
(ℜ‘𝐴))) / 2) =
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2)
− (((abs‘𝐴)
− (ℜ‘𝐴)) /
2))) | 
| 61 | 50, 57, 59 | divcan3d 12049 | . . . . . . . 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 11282 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ → (2
· (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) ∈ ℂ) | 
| 65 | 64, 4, 11 | mul12d 11471 | . . . . . . 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 11285 | . . . . . . 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 11285 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((2
· (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (2 ·
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) | 
| 68 | 2, 26, 27 | mul12d 11471 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (if((ℑ‘𝐴) < 0, -1, 1) ·
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) | 
| 69 |  | sqrtcvallem4 43657 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → 0 ≤
(((abs‘𝐴) +
(ℜ‘𝐴)) /
2)) | 
| 70 |  | halfnneg2 12499 | . . . . . . . . . . . . . . . . 17
⊢
(((abs‘𝐴) +
(ℜ‘𝐴)) ∈
ℝ → (0 ≤ ((abs‘𝐴) + (ℜ‘𝐴)) ↔ 0 ≤ (((abs‘𝐴) + (ℜ‘𝐴)) / 2))) | 
| 71 | 19, 70 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → (0 ≤
((abs‘𝐴) +
(ℜ‘𝐴)) ↔ 0
≤ (((abs‘𝐴) +
(ℜ‘𝐴)) /
2))) | 
| 72 | 69, 71 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → 0 ≤
((abs‘𝐴) +
(ℜ‘𝐴))) | 
| 73 |  | 2rp 13040 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ+ | 
| 74 | 73 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → 2 ∈
ℝ+) | 
| 75 | 19, 72, 74 | sqrtdivd 15463 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = ((√‘((abs‘𝐴) + (ℜ‘𝐴))) /
(√‘2))) | 
| 76 |  | sqrtcvallem2 43655 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → 0 ≤
(((abs‘𝐴) −
(ℜ‘𝐴)) /
2)) | 
| 77 |  | halfnneg2 12499 | . . . . . . . . . . . . . . . . 17
⊢
(((abs‘𝐴)
− (ℜ‘𝐴))
∈ ℝ → (0 ≤ ((abs‘𝐴) − (ℜ‘𝐴)) ↔ 0 ≤ (((abs‘𝐴) − (ℜ‘𝐴)) / 2))) | 
| 78 | 37, 77 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → (0 ≤
((abs‘𝐴) −
(ℜ‘𝐴)) ↔ 0
≤ (((abs‘𝐴)
− (ℜ‘𝐴)) /
2))) | 
| 79 | 76, 78 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → 0 ≤
((abs‘𝐴) −
(ℜ‘𝐴))) | 
| 80 | 37, 79, 74 | sqrtdivd 15463 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = ((√‘((abs‘𝐴) − (ℜ‘𝐴))) /
(√‘2))) | 
| 81 | 75, 80 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) =
(((√‘((abs‘𝐴) + (ℜ‘𝐴))) / (√‘2)) ·
((√‘((abs‘𝐴) − (ℜ‘𝐴))) / (√‘2)))) | 
| 82 | 19, 72 | resqrtcld 15457 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(√‘((abs‘𝐴) + (ℜ‘𝐴))) ∈ ℝ) | 
| 83 | 82 | recnd 11290 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(√‘((abs‘𝐴) + (ℜ‘𝐴))) ∈ ℂ) | 
| 84 |  | 2re 12341 | . . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ | 
| 85 | 84 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → 2 ∈
ℝ) | 
| 86 |  | 0le2 12369 | . . . . . . . . . . . . . . . . 17
⊢ 0 ≤
2 | 
| 87 | 86 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → 0 ≤
2) | 
| 88 | 85, 87 | resqrtcld 15457 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(√‘2) ∈ ℝ) | 
| 89 | 88 | recnd 11290 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(√‘2) ∈ ℂ) | 
| 90 | 37, 79 | resqrtcld 15457 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(√‘((abs‘𝐴) − (ℜ‘𝐴))) ∈ ℝ) | 
| 91 | 90 | recnd 11290 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(√‘((abs‘𝐴) − (ℜ‘𝐴))) ∈ ℂ) | 
| 92 |  | sqrt00 15303 | . . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℝ ∧ 0 ≤ 2) → ((√‘2) = 0 ↔ 2 =
0)) | 
| 93 | 84, 86, 92 | mp2an 692 | . . . . . . . . . . . . . . . . 17
⊢
((√‘2) = 0 ↔ 2 = 0) | 
| 94 | 93 | necon3bii 2992 | . . . . . . . . . . . . . . . 16
⊢
((√‘2) ≠ 0 ↔ 2 ≠ 0) | 
| 95 | 58, 94 | mpbir 231 | . . . . . . . . . . . . . . 15
⊢
(√‘2) ≠ 0 | 
| 96 | 95 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
(√‘2) ≠ 0) | 
| 97 | 83, 89, 91, 89, 96, 96 | divmuldivd 12085 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
(((√‘((abs‘𝐴) + (ℜ‘𝐴))) / (√‘2)) ·
((√‘((abs‘𝐴) − (ℜ‘𝐴))) / (√‘2))) =
(((√‘((abs‘𝐴) + (ℜ‘𝐴))) ·
(√‘((abs‘𝐴) − (ℜ‘𝐴)))) / ((√‘2) ·
(√‘2)))) | 
| 98 | 18 | resqcld 14166 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ →
((ℜ‘𝐴)↑2)
∈ ℝ) | 
| 99 | 98 | recnd 11290 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
((ℜ‘𝐴)↑2)
∈ ℂ) | 
| 100 |  | imcl 15151 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℝ) | 
| 101 | 100 | resqcld 14166 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ →
((ℑ‘𝐴)↑2)
∈ ℝ) | 
| 102 | 101 | recnd 11290 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
((ℑ‘𝐴)↑2)
∈ ℂ) | 
| 103 |  | absvalsq2 15321 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴)↑2) =
(((ℜ‘𝐴)↑2)
+ ((ℑ‘𝐴)↑2))) | 
| 104 | 99, 102, 103 | mvrladdd 11677 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴)↑2)
− ((ℜ‘𝐴)↑2)) = ((ℑ‘𝐴)↑2)) | 
| 105 |  | subsq 14250 | . . . . . . . . . . . . . . . . . 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 6909 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(√‘((ℑ‘𝐴)↑2)) =
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴))))) | 
| 109 | 100 | absred 15456 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ →
(abs‘(ℑ‘𝐴)) = (√‘((ℑ‘𝐴)↑2))) | 
| 110 |  | reabsifneg 43650 | . . . . . . . . . . . . . . . . 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 15464 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴)))) = ((√‘((abs‘𝐴) + (ℜ‘𝐴))) ·
(√‘((abs‘𝐴) − (ℜ‘𝐴))))) | 
| 114 | 108, 112,
113 | 3eqtr3rd 2785 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
((√‘((abs‘𝐴) + (ℜ‘𝐴))) ·
(√‘((abs‘𝐴) − (ℜ‘𝐴)))) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) | 
| 115 |  | remsqsqrt 15296 | . . . . . . . . . . . . . . . 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 7450 | . . . . . . . . . . . . 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 7448 | . . . . . . . . . . 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 7448 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (2
· ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (2 ·
(if((ℑ‘𝐴) <
0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)))) | 
| 123 | 100 | renegcld 11691 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ →
-(ℑ‘𝐴) ∈
ℝ) | 
| 124 | 123, 100 | ifcld 4571 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴)) ∈
ℝ) | 
| 125 | 124 | recnd 11290 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴)) ∈
ℂ) | 
| 126 | 26, 125, 57, 59 | divassd 12079 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
((if((ℑ‘𝐴) <
0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) / 2) = (if((ℑ‘𝐴) < 0, -1, 1) ·
(if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴)) /
2))) | 
| 127 |  | ovif12 7534 | . . . . . . . . . . . . . 14
⊢
(if((ℑ‘𝐴) < 0, -1, 1) ·
if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴))) =
if((ℑ‘𝐴) <
0, (-1 · -(ℑ‘𝐴)), (1 · (ℑ‘𝐴))) | 
| 128 | 5 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ → -1 ∈
ℝ) | 
| 129 | 128 | recnd 11290 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ → -1 ∈
ℂ) | 
| 130 | 100 | recnd 11290 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℂ) | 
| 131 | 129, 129,
130 | mulassd 11285 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ → ((-1
· -1) · (ℑ‘𝐴)) = (-1 · (-1 ·
(ℑ‘𝐴)))) | 
| 132 |  | neg1mulneg1e1 12480 | . . . . . . . . . . . . . . . . . . . 20
⊢ (-1
· -1) = 1 | 
| 133 | 132 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ → (-1
· -1) = 1) | 
| 134 | 133 | oveq1d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ → ((-1
· -1) · (ℑ‘𝐴)) = (1 · (ℑ‘𝐴))) | 
| 135 | 130 | mullidd 11280 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ → (1
· (ℑ‘𝐴))
= (ℑ‘𝐴)) | 
| 136 | 134, 135 | eqtrd 2776 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ → ((-1
· -1) · (ℑ‘𝐴)) = (ℑ‘𝐴)) | 
| 137 | 130 | mulm1d 11716 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ → (-1
· (ℑ‘𝐴))
= -(ℑ‘𝐴)) | 
| 138 | 137 | oveq2d 7448 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ → (-1
· (-1 · (ℑ‘𝐴))) = (-1 · -(ℑ‘𝐴))) | 
| 139 | 131, 136,
138 | 3eqtr3rd 2785 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → (-1
· -(ℑ‘𝐴)) = (ℑ‘𝐴)) | 
| 140 | 139 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℑ‘𝐴) < 0)
→ (-1 · -(ℑ‘𝐴)) = (ℑ‘𝐴)) | 
| 141 | 135 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧ ¬
(ℑ‘𝐴) < 0)
→ (1 · (ℑ‘𝐴)) = (ℑ‘𝐴)) | 
| 142 | 140, 141 | ifeqda 4561 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ →
if((ℑ‘𝐴) <
0, (-1 · -(ℑ‘𝐴)), (1 · (ℑ‘𝐴))) = (ℑ‘𝐴)) | 
| 143 | 127, 142 | eqtrid 2788 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ →
(if((ℑ‘𝐴) <
0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) = (ℑ‘𝐴)) | 
| 144 | 143 | oveq1d 7447 | . . . . . . . . . . . 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 7448 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (2
· (if((ℑ‘𝐴) < 0, -1, 1) ·
(if((ℑ‘𝐴) <
0, -(ℑ‘𝐴),
(ℑ‘𝐴)) / 2))) =
(2 · ((ℑ‘𝐴) / 2))) | 
| 147 | 130, 57, 59 | divcan2d 12046 | . . . . . . . . . 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 7448 | . . . . . . 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 7450 | . . . . 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 14166 | . . . . . . 7
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) ∈
ℝ) | 
| 154 | 153 | recnd 11290 | . . . . . 6
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) ∈
ℂ) | 
| 155 | 2, 12 | mulcld 11282 | . . . . . . 7
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) ∈ ℂ) | 
| 156 | 57, 155 | mulcld 11282 | . . . . . 6
⊢ (𝐴 ∈ ℂ → (2
· ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈
ℂ) | 
| 157 | 12 | sqcld 14185 | . . . . . 6
⊢ (𝐴 ∈ ℂ → ((i
· (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) ∈
ℂ) | 
| 158 | 154, 156,
157 | add32d 11490 | . . . . 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 15156 | . . . . 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 15460 | . . . 4
⊢ (𝐴 ∈ ℂ → 0 ≤
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) | 
| 163 | 1, 10 | crred 15271 | . . . 4
⊢ (𝐴 ∈ ℂ →
(ℜ‘((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) =
(√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) | 
| 164 | 162, 163 | breqtrrd 5170 | . . 3
⊢ (𝐴 ∈ ℂ → 0 ≤
(ℜ‘((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) | 
| 165 |  | reim 15149 | . . . . . . . . . 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 15432 | . . . . . . . 8
⊢
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2)
∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0 ↔ (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0)) | 
| 170 | 21, 169 | syl 17 | . . . . . . 7
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0 ↔ (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0)) | 
| 171 |  | half0 12496 | . . . . . . . . 9
⊢
(((abs‘𝐴) +
(ℜ‘𝐴)) ∈
ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0 ↔ ((abs‘𝐴) + (ℜ‘𝐴)) = 0)) | 
| 172 | 55, 171 | syl 17 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ →
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2) = 0
↔ ((abs‘𝐴) +
(ℜ‘𝐴)) =
0)) | 
| 173 | 49, 50 | addcomd 11464 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) +
(ℜ‘𝐴)) =
((ℜ‘𝐴) +
(abs‘𝐴))) | 
| 174 | 173 | eqeq1d 2738 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴) +
(ℜ‘𝐴)) = 0
↔ ((ℜ‘𝐴) +
(abs‘𝐴)) =
0)) | 
| 175 |  | addeq0 11687 | . . . . . . . . 9
⊢
(((ℜ‘𝐴)
∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) →
(((ℜ‘𝐴) +
(abs‘𝐴)) = 0 ↔
(ℜ‘𝐴) =
-(abs‘𝐴))) | 
| 176 | 50, 49, 175 | syl2anc 584 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(((ℜ‘𝐴) +
(abs‘𝐴)) = 0 ↔
(ℜ‘𝐴) =
-(abs‘𝐴))) | 
| 177 | 172, 174,
176 | 3bitrd 305 | . . . . . . 7
⊢ (𝐴 ∈ ℂ →
((((abs‘𝐴) +
(ℜ‘𝐴)) / 2) = 0
↔ (ℜ‘𝐴) =
-(abs‘𝐴))) | 
| 178 | 168, 170,
177 | 3bitrd 305 | . . . . . 6
⊢ (𝐴 ∈ ℂ →
((ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = 0 ↔ (ℜ‘𝐴) = -(abs‘𝐴))) | 
| 179 |  | olc 868 | . . . . . . . 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 14256 | . . . . . . . . . 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 11683 | . . . . . . . . . . 11
⊢
((((ℜ‘𝐴)↑2) ∈ ℂ ∧
((ℑ‘𝐴)↑2)
∈ ℂ) → ((((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) =
((ℜ‘𝐴)↑2)
↔ ((ℑ‘𝐴)↑2) = 0)) | 
| 186 | 99, 102, 185 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
((((ℜ‘𝐴)↑2)
+ ((ℑ‘𝐴)↑2)) = ((ℜ‘𝐴)↑2) ↔
((ℑ‘𝐴)↑2)
= 0)) | 
| 187 |  | sqeq0 14161 | . . . . . . . . . . 11
⊢
((ℑ‘𝐴)
∈ ℂ → (((ℑ‘𝐴)↑2) = 0 ↔ (ℑ‘𝐴) = 0)) | 
| 188 | 130, 187 | syl 17 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
(((ℑ‘𝐴)↑2)
= 0 ↔ (ℑ‘𝐴) = 0)) | 
| 189 | 184, 186,
188 | 3bitrd 305 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(((abs‘𝐴)↑2) =
((ℜ‘𝐴)↑2)
↔ (ℑ‘𝐴) =
0)) | 
| 190 | 181, 183,
189 | 3bitr3d 309 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(((ℜ‘𝐴) =
(abs‘𝐴) ∨
(ℜ‘𝐴) =
-(abs‘𝐴)) ↔
(ℑ‘𝐴) =
0)) | 
| 191 | 179, 190 | imbitrid 244 | . . . . . . 7
⊢ (𝐴 ∈ ℂ →
((ℜ‘𝐴) =
-(abs‘𝐴) →
(ℑ‘𝐴) =
0)) | 
| 192 | 191 | ancld 550 | . . . . . 6
⊢ (𝐴 ∈ ℂ →
((ℜ‘𝐴) =
-(abs‘𝐴) →
((ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) =
0))) | 
| 193 | 178, 192 | sylbid 240 | . . . . 5
⊢ (𝐴 ∈ ℂ →
((ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = 0 →
((ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) =
0))) | 
| 194 |  | simp2 1137 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (ℜ‘𝐴) =
-(abs‘𝐴)) | 
| 195 | 194 | oveq2d 7448 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((abs‘𝐴) +
(ℜ‘𝐴)) =
((abs‘𝐴) +
-(abs‘𝐴))) | 
| 196 | 49 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (abs‘𝐴) ∈
ℂ) | 
| 197 | 196 | negidd 11611 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((abs‘𝐴) +
-(abs‘𝐴)) =
0) | 
| 198 | 195, 197 | eqtrd 2776 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((abs‘𝐴) +
(ℜ‘𝐴)) =
0) | 
| 199 | 198 | oveq1d 7447 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (((abs‘𝐴) +
(ℜ‘𝐴)) / 2) = (0
/ 2)) | 
| 200 |  | 2cn 12342 | . . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℂ | 
| 201 | 200, 58 | div0i 12002 | . . . . . . . . . . . . . . . 16
⊢ (0 / 2) =
0 | 
| 202 | 199, 201 | eqtrdi 2792 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (((abs‘𝐴) +
(ℜ‘𝐴)) / 2) =
0) | 
| 203 | 202 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) =
(√‘0)) | 
| 204 |  | sqrt0 15281 | . . . . . . . . . . . . . 14
⊢
(√‘0) = 0 | 
| 205 | 203, 204 | eqtrdi 2792 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0) | 
| 206 |  | simp3 1138 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (ℑ‘𝐴) =
0) | 
| 207 |  | 0red 11265 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ 0 ∈ ℝ) | 
| 208 | 207 | ltnrd 11396 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ¬ 0 < 0) | 
| 209 | 206, 208 | eqnbrtrd 5160 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ¬ (ℑ‘𝐴) < 0) | 
| 210 | 209 | iffalsed 4535 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ if((ℑ‘𝐴)
< 0, -1, 1) = 1) | 
| 211 | 194 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((abs‘𝐴)
− (ℜ‘𝐴)) =
((abs‘𝐴) −
-(abs‘𝐴))) | 
| 212 | 49, 49 | subnegd 11628 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) −
-(abs‘𝐴)) =
((abs‘𝐴) +
(abs‘𝐴))) | 
| 213 | 49 | 2timesd 12511 | . . . . . . . . . . . . . . . . . . . . . 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 7447 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (((abs‘𝐴)
− (ℜ‘𝐴)) /
2) = ((2 · (abs‘𝐴)) / 2)) | 
| 218 | 49, 57, 59 | divcan3d 12049 | . . . . . . . . . . . . . . . . . . 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 6909 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = (√‘(abs‘𝐴))) | 
| 222 | 210, 221 | oveq12d 7450 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (1 ·
(√‘(abs‘𝐴)))) | 
| 223 |  | absge0 15327 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ ℂ → 0 ≤
(abs‘𝐴)) | 
| 224 | 17, 223 | resqrtcld 15457 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℂ →
(√‘(abs‘𝐴)) ∈ ℝ) | 
| 225 | 224 | recnd 11290 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℂ →
(√‘(abs‘𝐴)) ∈ ℂ) | 
| 226 | 225 | mullidd 11280 | . . . . . . . . . . . . . . . 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 7448 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (i · (if((ℑ‘𝐴) < 0, -1, 1) ·
(√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (i ·
(√‘(abs‘𝐴)))) | 
| 230 | 205, 229 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (0 + (i ·
(√‘(abs‘𝐴))))) | 
| 231 | 4, 225 | mulcld 11282 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℂ → (i
· (√‘(abs‘𝐴))) ∈ ℂ) | 
| 232 | 231 | 3ad2ant1 1133 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (i · (√‘(abs‘𝐴))) ∈ ℂ) | 
| 233 | 232 | addlidd 11463 | . . . . . . . . . . . 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 7448 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (i · (i ·
(√‘(abs‘𝐴))))) | 
| 236 |  | ixi 11893 | . . . . . . . . . . . . . 14
⊢ (i
· i) = -1 | 
| 237 | 236 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (i
· i) = -1) | 
| 238 | 237 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → ((i
· i) · (√‘(abs‘𝐴))) = (-1 ·
(√‘(abs‘𝐴)))) | 
| 239 | 4, 4, 225 | mulassd 11285 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → ((i
· i) · (√‘(abs‘𝐴))) = (i · (i ·
(√‘(abs‘𝐴))))) | 
| 240 | 225 | mulm1d 11716 | . . . . . . . . . . . 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 6909 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) =
(ℜ‘-(√‘(abs‘𝐴)))) | 
| 245 | 224 | renegcld 11691 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
-(√‘(abs‘𝐴)) ∈ ℝ) | 
| 246 | 245 | rered 15264 | . . . . . . . . 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 15460 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ → 0 ≤
(√‘(abs‘𝐴))) | 
| 250 | 224 | le0neg2d 11836 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (0 ≤
(√‘(abs‘𝐴)) ↔ -(√‘(abs‘𝐴)) ≤ 0)) | 
| 251 | 249, 250 | mpbid 232 | . . . . . . . 8
⊢ (𝐴 ∈ ℂ →
-(√‘(abs‘𝐴)) ≤ 0) | 
| 252 | 251 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(ℜ‘𝐴) =
-(abs‘𝐴) ∧
(ℑ‘𝐴) = 0)
→ -(√‘(abs‘𝐴)) ≤ 0) | 
| 253 | 248, 252 | eqbrtrd 5164 | . . . . . 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 11282 | . . . . 5
⊢ (𝐴 ∈ ℂ → (i
· ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈
ℂ) | 
| 257 | 256 | sqrtcvallem1 43649 | . . . 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 232 | . . 3
⊢ (𝐴 ∈ ℂ → ¬ (i
· ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈
ℝ+) | 
| 259 | 13, 14, 161, 164, 258 | eqsqrtd 15407 | . 2
⊢ (𝐴 ∈ ℂ →
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (√‘𝐴)) | 
| 260 | 259 | eqcomd 2742 | 1
⊢ (𝐴 ∈ ℂ →
(√‘𝐴) =
((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i ·
(if((ℑ‘𝐴) <
0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) |