| Step | Hyp | Ref
| Expression |
| 1 | | cnre 11258 |
. . 3
⊢ (𝐴 ∈ ℂ →
∃𝑦 ∈ ℝ
∃𝑧 ∈ ℝ
𝐴 = (𝑦 + (i · 𝑧))) |
| 2 | | recn 11245 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
| 3 | | ax-icn 11214 |
. . . . . . . 8
⊢ i ∈
ℂ |
| 4 | | recn 11245 |
. . . . . . . 8
⊢ (𝑧 ∈ ℝ → 𝑧 ∈
ℂ) |
| 5 | | mulcl 11239 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ 𝑧
∈ ℂ) → (i · 𝑧) ∈ ℂ) |
| 6 | 3, 4, 5 | sylancr 587 |
. . . . . . 7
⊢ (𝑧 ∈ ℝ → (i
· 𝑧) ∈
ℂ) |
| 7 | | subcl 11507 |
. . . . . . 7
⊢ ((𝑦 ∈ ℂ ∧ (i
· 𝑧) ∈ ℂ)
→ (𝑦 − (i
· 𝑧)) ∈
ℂ) |
| 8 | 2, 6, 7 | syl2an 596 |
. . . . . 6
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 − (i · 𝑧)) ∈
ℂ) |
| 9 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑦 ∈
ℂ) |
| 10 | 6 | adantl 481 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (i
· 𝑧) ∈
ℂ) |
| 11 | 9, 10, 9 | ppncand 11660 |
. . . . . . 7
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦 + (i · 𝑧)) + (𝑦 − (i · 𝑧))) = (𝑦 + 𝑦)) |
| 12 | | readdcl 11238 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 + 𝑦) ∈ ℝ) |
| 13 | 12 | anidms 566 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ → (𝑦 + 𝑦) ∈ ℝ) |
| 14 | 13 | adantr 480 |
. . . . . . 7
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 + 𝑦) ∈ ℝ) |
| 15 | 11, 14 | eqeltrd 2841 |
. . . . . 6
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦 + (i · 𝑧)) + (𝑦 − (i · 𝑧))) ∈ ℝ) |
| 16 | 9, 10, 10 | pnncand 11659 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦 + (i · 𝑧)) − (𝑦 − (i · 𝑧))) = ((i · 𝑧) + (i · 𝑧))) |
| 17 | 3 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → i ∈
ℂ) |
| 18 | 4 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑧 ∈
ℂ) |
| 19 | 17, 18, 18 | adddid 11285 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (i
· (𝑧 + 𝑧)) = ((i · 𝑧) + (i · 𝑧))) |
| 20 | 16, 19 | eqtr4d 2780 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦 + (i · 𝑧)) − (𝑦 − (i · 𝑧))) = (i · (𝑧 + 𝑧))) |
| 21 | 20 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (i
· ((𝑦 + (i ·
𝑧)) − (𝑦 − (i · 𝑧)))) = (i · (i ·
(𝑧 + 𝑧)))) |
| 22 | 18, 18 | addcld 11280 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 + 𝑧) ∈ ℂ) |
| 23 | | mulass 11243 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ i ∈ ℂ ∧ (𝑧 + 𝑧) ∈ ℂ) → ((i · i)
· (𝑧 + 𝑧)) = (i · (i ·
(𝑧 + 𝑧)))) |
| 24 | 3, 3, 22, 23 | mp3an12i 1467 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((i
· i) · (𝑧 +
𝑧)) = (i · (i
· (𝑧 + 𝑧)))) |
| 25 | 21, 24 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (i
· ((𝑦 + (i ·
𝑧)) − (𝑦 − (i · 𝑧)))) = ((i · i) ·
(𝑧 + 𝑧))) |
| 26 | | ixi 11892 |
. . . . . . . . 9
⊢ (i
· i) = -1 |
| 27 | | 1re 11261 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
| 28 | 27 | renegcli 11570 |
. . . . . . . . 9
⊢ -1 ∈
ℝ |
| 29 | 26, 28 | eqeltri 2837 |
. . . . . . . 8
⊢ (i
· i) ∈ ℝ |
| 30 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑧 ∈
ℝ) |
| 31 | 30, 30 | readdcld 11290 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑧 + 𝑧) ∈ ℝ) |
| 32 | | remulcl 11240 |
. . . . . . . 8
⊢ (((i
· i) ∈ ℝ ∧ (𝑧 + 𝑧) ∈ ℝ) → ((i · i)
· (𝑧 + 𝑧)) ∈
ℝ) |
| 33 | 29, 31, 32 | sylancr 587 |
. . . . . . 7
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((i
· i) · (𝑧 +
𝑧)) ∈
ℝ) |
| 34 | 25, 33 | eqeltrd 2841 |
. . . . . 6
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (i
· ((𝑦 + (i ·
𝑧)) − (𝑦 − (i · 𝑧)))) ∈
ℝ) |
| 35 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 − (i · 𝑧)) → ((𝑦 + (i · 𝑧)) + 𝑥) = ((𝑦 + (i · 𝑧)) + (𝑦 − (i · 𝑧)))) |
| 36 | 35 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 − (i · 𝑧)) → (((𝑦 + (i · 𝑧)) + 𝑥) ∈ ℝ ↔ ((𝑦 + (i · 𝑧)) + (𝑦 − (i · 𝑧))) ∈ ℝ)) |
| 37 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 − (i · 𝑧)) → ((𝑦 + (i · 𝑧)) − 𝑥) = ((𝑦 + (i · 𝑧)) − (𝑦 − (i · 𝑧)))) |
| 38 | 37 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 − (i · 𝑧)) → (i · ((𝑦 + (i · 𝑧)) − 𝑥)) = (i · ((𝑦 + (i · 𝑧)) − (𝑦 − (i · 𝑧))))) |
| 39 | 38 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 − (i · 𝑧)) → ((i · ((𝑦 + (i · 𝑧)) − 𝑥)) ∈ ℝ ↔ (i · ((𝑦 + (i · 𝑧)) − (𝑦 − (i · 𝑧)))) ∈ ℝ)) |
| 40 | 36, 39 | anbi12d 632 |
. . . . . . 7
⊢ (𝑥 = (𝑦 − (i · 𝑧)) → ((((𝑦 + (i · 𝑧)) + 𝑥) ∈ ℝ ∧ (i · ((𝑦 + (i · 𝑧)) − 𝑥)) ∈ ℝ) ↔ (((𝑦 + (i · 𝑧)) + (𝑦 − (i · 𝑧))) ∈ ℝ ∧ (i · ((𝑦 + (i · 𝑧)) − (𝑦 − (i · 𝑧)))) ∈ ℝ))) |
| 41 | 40 | rspcev 3622 |
. . . . . 6
⊢ (((𝑦 − (i · 𝑧)) ∈ ℂ ∧ (((𝑦 + (i · 𝑧)) + (𝑦 − (i · 𝑧))) ∈ ℝ ∧ (i · ((𝑦 + (i · 𝑧)) − (𝑦 − (i · 𝑧)))) ∈ ℝ)) → ∃𝑥 ∈ ℂ (((𝑦 + (i · 𝑧)) + 𝑥) ∈ ℝ ∧ (i · ((𝑦 + (i · 𝑧)) − 𝑥)) ∈ ℝ)) |
| 42 | 8, 15, 34, 41 | syl12anc 837 |
. . . . 5
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
∃𝑥 ∈ ℂ
(((𝑦 + (i · 𝑧)) + 𝑥) ∈ ℝ ∧ (i · ((𝑦 + (i · 𝑧)) − 𝑥)) ∈ ℝ)) |
| 43 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝐴 = (𝑦 + (i · 𝑧)) → (𝐴 + 𝑥) = ((𝑦 + (i · 𝑧)) + 𝑥)) |
| 44 | 43 | eleq1d 2826 |
. . . . . . 7
⊢ (𝐴 = (𝑦 + (i · 𝑧)) → ((𝐴 + 𝑥) ∈ ℝ ↔ ((𝑦 + (i · 𝑧)) + 𝑥) ∈ ℝ)) |
| 45 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝐴 = (𝑦 + (i · 𝑧)) → (𝐴 − 𝑥) = ((𝑦 + (i · 𝑧)) − 𝑥)) |
| 46 | 45 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝐴 = (𝑦 + (i · 𝑧)) → (i · (𝐴 − 𝑥)) = (i · ((𝑦 + (i · 𝑧)) − 𝑥))) |
| 47 | 46 | eleq1d 2826 |
. . . . . . 7
⊢ (𝐴 = (𝑦 + (i · 𝑧)) → ((i · (𝐴 − 𝑥)) ∈ ℝ ↔ (i · ((𝑦 + (i · 𝑧)) − 𝑥)) ∈ ℝ)) |
| 48 | 44, 47 | anbi12d 632 |
. . . . . 6
⊢ (𝐴 = (𝑦 + (i · 𝑧)) → (((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ) ↔ (((𝑦 + (i · 𝑧)) + 𝑥) ∈ ℝ ∧ (i · ((𝑦 + (i · 𝑧)) − 𝑥)) ∈ ℝ))) |
| 49 | 48 | rexbidv 3179 |
. . . . 5
⊢ (𝐴 = (𝑦 + (i · 𝑧)) → (∃𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ) ↔ ∃𝑥 ∈ ℂ (((𝑦 + (i · 𝑧)) + 𝑥) ∈ ℝ ∧ (i · ((𝑦 + (i · 𝑧)) − 𝑥)) ∈ ℝ))) |
| 50 | 42, 49 | syl5ibrcom 247 |
. . . 4
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐴 = (𝑦 + (i · 𝑧)) → ∃𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ))) |
| 51 | 50 | rexlimivv 3201 |
. . 3
⊢
(∃𝑦 ∈
ℝ ∃𝑧 ∈
ℝ 𝐴 = (𝑦 + (i · 𝑧)) → ∃𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ)) |
| 52 | 1, 51 | syl 17 |
. 2
⊢ (𝐴 ∈ ℂ →
∃𝑥 ∈ ℂ
((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ)) |
| 53 | | an4 656 |
. . . 4
⊢ ((((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ) ∧ ((𝐴 + 𝑦) ∈ ℝ ∧ (i · (𝐴 − 𝑦)) ∈ ℝ)) ↔ (((𝐴 + 𝑥) ∈ ℝ ∧ (𝐴 + 𝑦) ∈ ℝ) ∧ ((i · (𝐴 − 𝑥)) ∈ ℝ ∧ (i · (𝐴 − 𝑦)) ∈ ℝ))) |
| 54 | | resubcl 11573 |
. . . . . . 7
⊢ (((𝐴 + 𝑥) ∈ ℝ ∧ (𝐴 + 𝑦) ∈ ℝ) → ((𝐴 + 𝑥) − (𝐴 + 𝑦)) ∈ ℝ) |
| 55 | | pnpcan 11548 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝐴 + 𝑥) − (𝐴 + 𝑦)) = (𝑥 − 𝑦)) |
| 56 | 55 | 3expb 1121 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((𝐴 + 𝑥) − (𝐴 + 𝑦)) = (𝑥 − 𝑦)) |
| 57 | 56 | eleq1d 2826 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) →
(((𝐴 + 𝑥) − (𝐴 + 𝑦)) ∈ ℝ ↔ (𝑥 − 𝑦) ∈ ℝ)) |
| 58 | 54, 57 | imbitrid 244 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) →
(((𝐴 + 𝑥) ∈ ℝ ∧ (𝐴 + 𝑦) ∈ ℝ) → (𝑥 − 𝑦) ∈ ℝ)) |
| 59 | | resubcl 11573 |
. . . . . . . 8
⊢ (((i
· (𝐴 − 𝑦)) ∈ ℝ ∧ (i
· (𝐴 − 𝑥)) ∈ ℝ) → ((i
· (𝐴 − 𝑦)) − (i · (𝐴 − 𝑥))) ∈ ℝ) |
| 60 | 59 | ancoms 458 |
. . . . . . 7
⊢ (((i
· (𝐴 − 𝑥)) ∈ ℝ ∧ (i
· (𝐴 − 𝑦)) ∈ ℝ) → ((i
· (𝐴 − 𝑦)) − (i · (𝐴 − 𝑥))) ∈ ℝ) |
| 61 | 3 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → i
∈ ℂ) |
| 62 | | subcl 11507 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐴 − 𝑦) ∈ ℂ) |
| 63 | 62 | adantrl 716 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝐴 − 𝑦) ∈ ℂ) |
| 64 | | subcl 11507 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴 − 𝑥) ∈ ℂ) |
| 65 | 64 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝐴 − 𝑥) ∈ ℂ) |
| 66 | 61, 63, 65 | subdid 11719 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (i
· ((𝐴 − 𝑦) − (𝐴 − 𝑥))) = ((i · (𝐴 − 𝑦)) − (i · (𝐴 − 𝑥)))) |
| 67 | | nnncan1 11545 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝐴 − 𝑦) − (𝐴 − 𝑥)) = (𝑥 − 𝑦)) |
| 68 | 67 | 3com23 1127 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝐴 − 𝑦) − (𝐴 − 𝑥)) = (𝑥 − 𝑦)) |
| 69 | 68 | 3expb 1121 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((𝐴 − 𝑦) − (𝐴 − 𝑥)) = (𝑥 − 𝑦)) |
| 70 | 69 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (i
· ((𝐴 − 𝑦) − (𝐴 − 𝑥))) = (i · (𝑥 − 𝑦))) |
| 71 | 66, 70 | eqtr3d 2779 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((i
· (𝐴 − 𝑦)) − (i · (𝐴 − 𝑥))) = (i · (𝑥 − 𝑦))) |
| 72 | 71 | eleq1d 2826 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (((i
· (𝐴 − 𝑦)) − (i · (𝐴 − 𝑥))) ∈ ℝ ↔ (i · (𝑥 − 𝑦)) ∈ ℝ)) |
| 73 | 60, 72 | imbitrid 244 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (((i
· (𝐴 − 𝑥)) ∈ ℝ ∧ (i
· (𝐴 − 𝑦)) ∈ ℝ) → (i
· (𝑥 − 𝑦)) ∈
ℝ)) |
| 74 | 58, 73 | anim12d 609 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) →
((((𝐴 + 𝑥) ∈ ℝ ∧ (𝐴 + 𝑦) ∈ ℝ) ∧ ((i · (𝐴 − 𝑥)) ∈ ℝ ∧ (i · (𝐴 − 𝑦)) ∈ ℝ)) → ((𝑥 − 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ))) |
| 75 | | rimul 12257 |
. . . . . 6
⊢ (((𝑥 − 𝑦) ∈ ℝ ∧ (i · (𝑥 − 𝑦)) ∈ ℝ) → (𝑥 − 𝑦) = 0) |
| 76 | 75 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) →
(((𝑥 − 𝑦) ∈ ℝ ∧ (i
· (𝑥 − 𝑦)) ∈ ℝ) → (𝑥 − 𝑦) = 0)) |
| 77 | | subeq0 11535 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑥 − 𝑦) = 0 ↔ 𝑥 = 𝑦)) |
| 78 | 77 | biimpd 229 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑥 − 𝑦) = 0 → 𝑥 = 𝑦)) |
| 79 | 78 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((𝑥 − 𝑦) = 0 → 𝑥 = 𝑦)) |
| 80 | 74, 76, 79 | 3syld 60 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) →
((((𝐴 + 𝑥) ∈ ℝ ∧ (𝐴 + 𝑦) ∈ ℝ) ∧ ((i · (𝐴 − 𝑥)) ∈ ℝ ∧ (i · (𝐴 − 𝑦)) ∈ ℝ)) → 𝑥 = 𝑦)) |
| 81 | 53, 80 | biimtrid 242 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) →
((((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ) ∧ ((𝐴 + 𝑦) ∈ ℝ ∧ (i · (𝐴 − 𝑦)) ∈ ℝ)) → 𝑥 = 𝑦)) |
| 82 | 81 | ralrimivva 3202 |
. 2
⊢ (𝐴 ∈ ℂ →
∀𝑥 ∈ ℂ
∀𝑦 ∈ ℂ
((((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ) ∧ ((𝐴 + 𝑦) ∈ ℝ ∧ (i · (𝐴 − 𝑦)) ∈ ℝ)) → 𝑥 = 𝑦)) |
| 83 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐴 + 𝑥) = (𝐴 + 𝑦)) |
| 84 | 83 | eleq1d 2826 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐴 + 𝑥) ∈ ℝ ↔ (𝐴 + 𝑦) ∈ ℝ)) |
| 85 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴 − 𝑥) = (𝐴 − 𝑦)) |
| 86 | 85 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = 𝑦 → (i · (𝐴 − 𝑥)) = (i · (𝐴 − 𝑦))) |
| 87 | 86 | eleq1d 2826 |
. . . 4
⊢ (𝑥 = 𝑦 → ((i · (𝐴 − 𝑥)) ∈ ℝ ↔ (i · (𝐴 − 𝑦)) ∈ ℝ)) |
| 88 | 84, 87 | anbi12d 632 |
. . 3
⊢ (𝑥 = 𝑦 → (((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ) ↔ ((𝐴 + 𝑦) ∈ ℝ ∧ (i · (𝐴 − 𝑦)) ∈ ℝ))) |
| 89 | 88 | reu4 3737 |
. 2
⊢
(∃!𝑥 ∈
ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i
· (𝐴 − 𝑥)) ∈ ℝ) ↔
(∃𝑥 ∈ ℂ
((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ ((((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ) ∧ ((𝐴 + 𝑦) ∈ ℝ ∧ (i · (𝐴 − 𝑦)) ∈ ℝ)) → 𝑥 = 𝑦))) |
| 90 | 52, 82, 89 | sylanbrc 583 |
1
⊢ (𝐴 ∈ ℂ →
∃!𝑥 ∈ ℂ
((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ)) |