| Step | Hyp | Ref
| Expression |
| 1 | | cjval 15141 |
. 2
⊢ (𝐴 ∈ ℂ →
(∗‘𝐴) =
(℩𝑥 ∈
ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i
· (𝐴 − 𝑥)) ∈
ℝ))) |
| 2 | | replim 15155 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → 𝐴 = ((ℜ‘𝐴) + (i ·
(ℑ‘𝐴)))) |
| 3 | 2 | oveq1d 7446 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝐴 + ((ℜ‘𝐴) − (i ·
(ℑ‘𝐴)))) =
(((ℜ‘𝐴) + (i
· (ℑ‘𝐴))) + ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))) |
| 4 | | recl 15149 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) |
| 5 | 4 | recnd 11289 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℂ) |
| 6 | | ax-icn 11214 |
. . . . . . 7
⊢ i ∈
ℂ |
| 7 | | imcl 15150 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℝ) |
| 8 | 7 | recnd 11289 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℂ) |
| 9 | | mulcl 11239 |
. . . . . . 7
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → (i ·
(ℑ‘𝐴)) ∈
ℂ) |
| 10 | 6, 8, 9 | sylancr 587 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (i
· (ℑ‘𝐴))
∈ ℂ) |
| 11 | 5, 10, 5 | ppncand 11660 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(((ℜ‘𝐴) + (i
· (ℑ‘𝐴))) + ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))) = ((ℜ‘𝐴) + (ℜ‘𝐴))) |
| 12 | 3, 11 | eqtrd 2777 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝐴 + ((ℜ‘𝐴) − (i ·
(ℑ‘𝐴)))) =
((ℜ‘𝐴) +
(ℜ‘𝐴))) |
| 13 | 4, 4 | readdcld 11290 |
. . . 4
⊢ (𝐴 ∈ ℂ →
((ℜ‘𝐴) +
(ℜ‘𝐴)) ∈
ℝ) |
| 14 | 12, 13 | eqeltrd 2841 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝐴 + ((ℜ‘𝐴) − (i ·
(ℑ‘𝐴)))) ∈
ℝ) |
| 15 | 5, 10, 10 | pnncand 11659 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(((ℜ‘𝐴) + (i
· (ℑ‘𝐴))) − ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))) = ((i ·
(ℑ‘𝐴)) + (i
· (ℑ‘𝐴)))) |
| 16 | 2 | oveq1d 7446 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝐴 − ((ℜ‘𝐴) − (i ·
(ℑ‘𝐴)))) =
(((ℜ‘𝐴) + (i
· (ℑ‘𝐴))) − ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))) |
| 17 | 6 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → i ∈
ℂ) |
| 18 | 17, 8, 8 | adddid 11285 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (i
· ((ℑ‘𝐴)
+ (ℑ‘𝐴))) = ((i
· (ℑ‘𝐴))
+ (i · (ℑ‘𝐴)))) |
| 19 | 15, 16, 18 | 3eqtr4d 2787 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝐴 − ((ℜ‘𝐴) − (i ·
(ℑ‘𝐴)))) = (i
· ((ℑ‘𝐴)
+ (ℑ‘𝐴)))) |
| 20 | 19 | oveq2d 7447 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (i
· (𝐴 −
((ℜ‘𝐴) −
(i · (ℑ‘𝐴))))) = (i · (i ·
((ℑ‘𝐴) +
(ℑ‘𝐴))))) |
| 21 | 7, 7 | readdcld 11290 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((ℑ‘𝐴) +
(ℑ‘𝐴)) ∈
ℝ) |
| 22 | 21 | recnd 11289 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
((ℑ‘𝐴) +
(ℑ‘𝐴)) ∈
ℂ) |
| 23 | | mulass 11243 |
. . . . . 6
⊢ ((i
∈ ℂ ∧ i ∈ ℂ ∧ ((ℑ‘𝐴) + (ℑ‘𝐴)) ∈ ℂ) → ((i · i)
· ((ℑ‘𝐴)
+ (ℑ‘𝐴))) = (i
· (i · ((ℑ‘𝐴) + (ℑ‘𝐴))))) |
| 24 | 6, 6, 22, 23 | mp3an12i 1467 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((i
· i) · ((ℑ‘𝐴) + (ℑ‘𝐴))) = (i · (i ·
((ℑ‘𝐴) +
(ℑ‘𝐴))))) |
| 25 | 20, 24 | eqtr4d 2780 |
. . . 4
⊢ (𝐴 ∈ ℂ → (i
· (𝐴 −
((ℜ‘𝐴) −
(i · (ℑ‘𝐴))))) = ((i · i) ·
((ℑ‘𝐴) +
(ℑ‘𝐴)))) |
| 26 | | ixi 11892 |
. . . . . 6
⊢ (i
· i) = -1 |
| 27 | | neg1rr 12381 |
. . . . . 6
⊢ -1 ∈
ℝ |
| 28 | 26, 27 | eqeltri 2837 |
. . . . 5
⊢ (i
· i) ∈ ℝ |
| 29 | | remulcl 11240 |
. . . . 5
⊢ (((i
· i) ∈ ℝ ∧ ((ℑ‘𝐴) + (ℑ‘𝐴)) ∈ ℝ) → ((i · i)
· ((ℑ‘𝐴)
+ (ℑ‘𝐴)))
∈ ℝ) |
| 30 | 28, 21, 29 | sylancr 587 |
. . . 4
⊢ (𝐴 ∈ ℂ → ((i
· i) · ((ℑ‘𝐴) + (ℑ‘𝐴))) ∈ ℝ) |
| 31 | 25, 30 | eqeltrd 2841 |
. . 3
⊢ (𝐴 ∈ ℂ → (i
· (𝐴 −
((ℜ‘𝐴) −
(i · (ℑ‘𝐴))))) ∈ ℝ) |
| 32 | 5, 10 | subcld 11620 |
. . . 4
⊢ (𝐴 ∈ ℂ →
((ℜ‘𝐴) −
(i · (ℑ‘𝐴))) ∈ ℂ) |
| 33 | | cju 12262 |
. . . 4
⊢ (𝐴 ∈ ℂ →
∃!𝑥 ∈ ℂ
((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ)) |
| 34 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑥 = ((ℜ‘𝐴) − (i ·
(ℑ‘𝐴))) →
(𝐴 + 𝑥) = (𝐴 + ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))) |
| 35 | 34 | eleq1d 2826 |
. . . . . 6
⊢ (𝑥 = ((ℜ‘𝐴) − (i ·
(ℑ‘𝐴))) →
((𝐴 + 𝑥) ∈ ℝ ↔ (𝐴 + ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))) ∈
ℝ)) |
| 36 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = ((ℜ‘𝐴) − (i ·
(ℑ‘𝐴))) →
(𝐴 − 𝑥) = (𝐴 − ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))) |
| 37 | 36 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑥 = ((ℜ‘𝐴) − (i ·
(ℑ‘𝐴))) →
(i · (𝐴 −
𝑥)) = (i · (𝐴 − ((ℜ‘𝐴) − (i ·
(ℑ‘𝐴)))))) |
| 38 | 37 | eleq1d 2826 |
. . . . . 6
⊢ (𝑥 = ((ℜ‘𝐴) − (i ·
(ℑ‘𝐴))) →
((i · (𝐴 −
𝑥)) ∈ ℝ ↔
(i · (𝐴 −
((ℜ‘𝐴) −
(i · (ℑ‘𝐴))))) ∈ ℝ)) |
| 39 | 35, 38 | anbi12d 632 |
. . . . 5
⊢ (𝑥 = ((ℜ‘𝐴) − (i ·
(ℑ‘𝐴))) →
(((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ) ↔ ((𝐴 + ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))) ∈ ℝ ∧ (i
· (𝐴 −
((ℜ‘𝐴) −
(i · (ℑ‘𝐴))))) ∈ ℝ))) |
| 40 | 39 | riota2 7413 |
. . . 4
⊢
((((ℜ‘𝐴)
− (i · (ℑ‘𝐴))) ∈ ℂ ∧ ∃!𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ)) → (((𝐴 + ((ℜ‘𝐴) − (i ·
(ℑ‘𝐴)))) ∈
ℝ ∧ (i · (𝐴 − ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))) ∈ ℝ) ↔
(℩𝑥 ∈
ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i
· (𝐴 − 𝑥)) ∈ ℝ)) =
((ℜ‘𝐴) −
(i · (ℑ‘𝐴))))) |
| 41 | 32, 33, 40 | syl2anc 584 |
. . 3
⊢ (𝐴 ∈ ℂ → (((𝐴 + ((ℜ‘𝐴) − (i ·
(ℑ‘𝐴)))) ∈
ℝ ∧ (i · (𝐴 − ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))) ∈ ℝ) ↔
(℩𝑥 ∈
ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i
· (𝐴 − 𝑥)) ∈ ℝ)) =
((ℜ‘𝐴) −
(i · (ℑ‘𝐴))))) |
| 42 | 14, 31, 41 | mpbi2and 712 |
. 2
⊢ (𝐴 ∈ ℂ →
(℩𝑥 ∈
ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i
· (𝐴 − 𝑥)) ∈ ℝ)) =
((ℜ‘𝐴) −
(i · (ℑ‘𝐴)))) |
| 43 | 1, 42 | eqtrd 2777 |
1
⊢ (𝐴 ∈ ℂ →
(∗‘𝐴) =
((ℜ‘𝐴) −
(i · (ℑ‘𝐴)))) |