| Step | Hyp | Ref
| Expression |
| 1 | | cnre 11258 |
. 2
⊢ (𝐴 ∈ ℂ →
∃𝑥 ∈ ℝ
∃𝑦 ∈ ℝ
𝐴 = (𝑥 + (i · 𝑦))) |
| 2 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑏 = ((i · (0
−ℝ 𝑦)) + (0 −ℝ 𝑥)) → ((𝑥 + (i · 𝑦)) + 𝑏) = ((𝑥 + (i · 𝑦)) + ((i · (0
−ℝ 𝑦)) + (0 −ℝ 𝑥)))) |
| 3 | 2 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑏 = ((i · (0
−ℝ 𝑦)) + (0 −ℝ 𝑥)) → (((𝑥 + (i · 𝑦)) + 𝑏) = 0 ↔ ((𝑥 + (i · 𝑦)) + ((i · (0
−ℝ 𝑦)) + (0 −ℝ 𝑥))) = 0)) |
| 4 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑏 = ((i · (0
−ℝ 𝑦)) + (0 −ℝ 𝑥)) → (𝑏 + (𝑥 + (i · 𝑦))) = (((i · (0
−ℝ 𝑦)) + (0 −ℝ 𝑥)) + (𝑥 + (i · 𝑦)))) |
| 5 | 4 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑏 = ((i · (0
−ℝ 𝑦)) + (0 −ℝ 𝑥)) → ((𝑏 + (𝑥 + (i · 𝑦))) = 0 ↔ (((i · (0
−ℝ 𝑦)) + (0 −ℝ 𝑥)) + (𝑥 + (i · 𝑦))) = 0)) |
| 6 | 3, 5 | anbi12d 632 |
. . . . . 6
⊢ (𝑏 = ((i · (0
−ℝ 𝑦)) + (0 −ℝ 𝑥)) → ((((𝑥 + (i · 𝑦)) + 𝑏) = 0 ∧ (𝑏 + (𝑥 + (i · 𝑦))) = 0) ↔ (((𝑥 + (i · 𝑦)) + ((i · (0
−ℝ 𝑦)) + (0 −ℝ 𝑥))) = 0 ∧ (((i · (0
−ℝ 𝑦)) + (0 −ℝ 𝑥)) + (𝑥 + (i · 𝑦))) = 0))) |
| 7 | | ax-icn 11214 |
. . . . . . . . . 10
⊢ i ∈
ℂ |
| 8 | 7 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → i ∈
ℂ) |
| 9 | | rernegcl 42401 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → (0
−ℝ 𝑦) ∈ ℝ) |
| 10 | 9 | recnd 11289 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → (0
−ℝ 𝑦) ∈ ℂ) |
| 11 | 8, 10 | mulcld 11281 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ → (i
· (0 −ℝ 𝑦)) ∈ ℂ) |
| 12 | 11 | adantl 481 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (i
· (0 −ℝ 𝑦)) ∈ ℂ) |
| 13 | | rernegcl 42401 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → (0
−ℝ 𝑥) ∈ ℝ) |
| 14 | 13 | recnd 11289 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ → (0
−ℝ 𝑥) ∈ ℂ) |
| 15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (0
−ℝ 𝑥) ∈ ℂ) |
| 16 | 12, 15 | addcld 11280 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((i
· (0 −ℝ 𝑦)) + (0 −ℝ 𝑥)) ∈
ℂ) |
| 17 | | recn 11245 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
| 18 | 17 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈
ℂ) |
| 19 | | recn 11245 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
| 20 | 8, 19 | mulcld 11281 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → (i
· 𝑦) ∈
ℂ) |
| 21 | 20 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (i
· 𝑦) ∈
ℂ) |
| 22 | 18, 21, 12 | addassd 11283 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) + (i · (0
−ℝ 𝑦))) = (𝑥 + ((i · 𝑦) + (i · (0 −ℝ
𝑦))))) |
| 23 | 8, 19, 10 | adddid 11285 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ → (i
· (𝑦 + (0
−ℝ 𝑦))) = ((i · 𝑦) + (i · (0 −ℝ
𝑦)))) |
| 24 | | renegid 42403 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ → (𝑦 + (0 −ℝ
𝑦)) = 0) |
| 25 | 24 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ → (i
· (𝑦 + (0
−ℝ 𝑦))) = (i · 0)) |
| 26 | | sn-it0e0 42445 |
. . . . . . . . . . . . . 14
⊢ (i
· 0) = 0 |
| 27 | 25, 26 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ → (i
· (𝑦 + (0
−ℝ 𝑦))) = 0) |
| 28 | 23, 27 | eqtr3d 2779 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → ((i
· 𝑦) + (i ·
(0 −ℝ 𝑦))) = 0) |
| 29 | 28 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((i
· 𝑦) + (i ·
(0 −ℝ 𝑦))) = 0) |
| 30 | 29 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + ((i · 𝑦) + (i · (0
−ℝ 𝑦)))) = (𝑥 + 0)) |
| 31 | | readdrid 42439 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → (𝑥 + 0) = 𝑥) |
| 32 | 31 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 0) = 𝑥) |
| 33 | 22, 30, 32 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) + (i · (0
−ℝ 𝑦))) = 𝑥) |
| 34 | 33 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((𝑥 + (i · 𝑦)) + (i · (0
−ℝ 𝑦))) + (0 −ℝ 𝑥)) = (𝑥 + (0 −ℝ 𝑥))) |
| 35 | 18, 21 | addcld 11280 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + (i · 𝑦)) ∈
ℂ) |
| 36 | 35, 12, 15 | addassd 11283 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((𝑥 + (i · 𝑦)) + (i · (0
−ℝ 𝑦))) + (0 −ℝ 𝑥)) = ((𝑥 + (i · 𝑦)) + ((i · (0
−ℝ 𝑦)) + (0 −ℝ 𝑥)))) |
| 37 | | renegid 42403 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → (𝑥 + (0 −ℝ
𝑥)) = 0) |
| 38 | 37 | adantr 480 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + (0 −ℝ
𝑥)) = 0) |
| 39 | 34, 36, 38 | 3eqtr3d 2785 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) + ((i · (0
−ℝ 𝑦)) + (0 −ℝ 𝑥))) = 0) |
| 40 | 12, 15, 35 | addassd 11283 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((i
· (0 −ℝ 𝑦)) + (0 −ℝ 𝑥)) + (𝑥 + (i · 𝑦))) = ((i · (0
−ℝ 𝑦)) + ((0 −ℝ 𝑥) + (𝑥 + (i · 𝑦))))) |
| 41 | | renegid2 42443 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → ((0
−ℝ 𝑥) + 𝑥) = 0) |
| 42 | 41 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((0
−ℝ 𝑥) + 𝑥) = 0) |
| 43 | 42 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((0
−ℝ 𝑥) + 𝑥) + (i · 𝑦)) = (0 + (i · 𝑦))) |
| 44 | 15, 18, 21 | addassd 11283 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((0
−ℝ 𝑥) + 𝑥) + (i · 𝑦)) = ((0 −ℝ 𝑥) + (𝑥 + (i · 𝑦)))) |
| 45 | | sn-addlid 42434 |
. . . . . . . . . . 11
⊢ ((i
· 𝑦) ∈ ℂ
→ (0 + (i · 𝑦))
= (i · 𝑦)) |
| 46 | 21, 45 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (0 + (i
· 𝑦)) = (i ·
𝑦)) |
| 47 | 43, 44, 46 | 3eqtr3rd 2786 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (i
· 𝑦) = ((0
−ℝ 𝑥) + (𝑥 + (i · 𝑦)))) |
| 48 | 47 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((i
· (0 −ℝ 𝑦)) + (i · 𝑦)) = ((i · (0
−ℝ 𝑦)) + ((0 −ℝ 𝑥) + (𝑥 + (i · 𝑦))))) |
| 49 | 8, 10, 19 | adddid 11285 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → (i
· ((0 −ℝ 𝑦) + 𝑦)) = ((i · (0
−ℝ 𝑦)) + (i · 𝑦))) |
| 50 | | renegid2 42443 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → ((0
−ℝ 𝑦) + 𝑦) = 0) |
| 51 | 50 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ → (i
· ((0 −ℝ 𝑦) + 𝑦)) = (i · 0)) |
| 52 | 51, 26 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ → (i
· ((0 −ℝ 𝑦) + 𝑦)) = 0) |
| 53 | 49, 52 | eqtr3d 2779 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → ((i
· (0 −ℝ 𝑦)) + (i · 𝑦)) = 0) |
| 54 | 53 | adantl 481 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((i
· (0 −ℝ 𝑦)) + (i · 𝑦)) = 0) |
| 55 | 40, 48, 54 | 3eqtr2d 2783 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((i
· (0 −ℝ 𝑦)) + (0 −ℝ 𝑥)) + (𝑥 + (i · 𝑦))) = 0) |
| 56 | 39, 55 | jca 511 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((𝑥 + (i · 𝑦)) + ((i · (0
−ℝ 𝑦)) + (0 −ℝ 𝑥))) = 0 ∧ (((i · (0
−ℝ 𝑦)) + (0 −ℝ 𝑥)) + (𝑥 + (i · 𝑦))) = 0)) |
| 57 | 6, 16, 56 | rspcedvdw 3625 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
∃𝑏 ∈ ℂ
(((𝑥 + (i · 𝑦)) + 𝑏) = 0 ∧ (𝑏 + (𝑥 + (i · 𝑦))) = 0)) |
| 58 | 57 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) →
∃𝑏 ∈ ℂ
(((𝑥 + (i · 𝑦)) + 𝑏) = 0 ∧ (𝑏 + (𝑥 + (i · 𝑦))) = 0)) |
| 59 | | oveq1 7438 |
. . . . . . 7
⊢ (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 + 𝑏) = ((𝑥 + (i · 𝑦)) + 𝑏)) |
| 60 | 59 | eqeq1d 2739 |
. . . . . 6
⊢ (𝐴 = (𝑥 + (i · 𝑦)) → ((𝐴 + 𝑏) = 0 ↔ ((𝑥 + (i · 𝑦)) + 𝑏) = 0)) |
| 61 | | oveq2 7439 |
. . . . . . 7
⊢ (𝐴 = (𝑥 + (i · 𝑦)) → (𝑏 + 𝐴) = (𝑏 + (𝑥 + (i · 𝑦)))) |
| 62 | 61 | eqeq1d 2739 |
. . . . . 6
⊢ (𝐴 = (𝑥 + (i · 𝑦)) → ((𝑏 + 𝐴) = 0 ↔ (𝑏 + (𝑥 + (i · 𝑦))) = 0)) |
| 63 | 60, 62 | anbi12d 632 |
. . . . 5
⊢ (𝐴 = (𝑥 + (i · 𝑦)) → (((𝐴 + 𝑏) = 0 ∧ (𝑏 + 𝐴) = 0) ↔ (((𝑥 + (i · 𝑦)) + 𝑏) = 0 ∧ (𝑏 + (𝑥 + (i · 𝑦))) = 0))) |
| 64 | 63 | rexbidv 3179 |
. . . 4
⊢ (𝐴 = (𝑥 + (i · 𝑦)) → (∃𝑏 ∈ ℂ ((𝐴 + 𝑏) = 0 ∧ (𝑏 + 𝐴) = 0) ↔ ∃𝑏 ∈ ℂ (((𝑥 + (i · 𝑦)) + 𝑏) = 0 ∧ (𝑏 + (𝑥 + (i · 𝑦))) = 0))) |
| 65 | 58, 64 | syl5ibrcom 247 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝐴 = (𝑥 + (i · 𝑦)) → ∃𝑏 ∈ ℂ ((𝐴 + 𝑏) = 0 ∧ (𝑏 + 𝐴) = 0))) |
| 66 | 65 | rexlimdvva 3213 |
. 2
⊢ (𝐴 ∈ ℂ →
(∃𝑥 ∈ ℝ
∃𝑦 ∈ ℝ
𝐴 = (𝑥 + (i · 𝑦)) → ∃𝑏 ∈ ℂ ((𝐴 + 𝑏) = 0 ∧ (𝑏 + 𝐴) = 0))) |
| 67 | 1, 66 | mpd 15 |
1
⊢ (𝐴 ∈ ℂ →
∃𝑏 ∈ ℂ
((𝐴 + 𝑏) = 0 ∧ (𝑏 + 𝐴) = 0)) |