| Step | Hyp | Ref
| Expression |
| 1 | | cnre 11258 |
. 2
⊢ (𝐴 ∈ ℂ →
∃𝑥 ∈ ℝ
∃𝑦 ∈ ℝ
𝐴 = (𝑥 + (i · 𝑦))) |
| 2 | | recn 11245 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
| 3 | | ax-icn 11214 |
. . . . . . 7
⊢ i ∈
ℂ |
| 4 | | recn 11245 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
| 5 | | mulcl 11239 |
. . . . . . 7
⊢ ((i
∈ ℂ ∧ 𝑦
∈ ℂ) → (i · 𝑦) ∈ ℂ) |
| 6 | 3, 4, 5 | sylancr 587 |
. . . . . 6
⊢ (𝑦 ∈ ℝ → (i
· 𝑦) ∈
ℂ) |
| 7 | | ax-1cn 11213 |
. . . . . . 7
⊢ 1 ∈
ℂ |
| 8 | | adddir 11252 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ (i
· 𝑦) ∈ ℂ
∧ 1 ∈ ℂ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1))) |
| 9 | 7, 8 | mp3an3 1452 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ (i
· 𝑦) ∈ ℂ)
→ ((𝑥 + (i ·
𝑦)) · 1) = ((𝑥 · 1) + ((i ·
𝑦) ·
1))) |
| 10 | 2, 6, 9 | syl2an 596 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i ·
𝑦) ·
1))) |
| 11 | | ax-1rid 11225 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → (𝑥 · 1) = 𝑥) |
| 12 | | mulass 11243 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝑦
∈ ℂ ∧ 1 ∈ ℂ) → ((i · 𝑦) · 1) = (i · (𝑦 · 1))) |
| 13 | 3, 7, 12 | mp3an13 1454 |
. . . . . . . 8
⊢ (𝑦 ∈ ℂ → ((i
· 𝑦) · 1) =
(i · (𝑦 ·
1))) |
| 14 | 4, 13 | syl 17 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ → ((i
· 𝑦) · 1) =
(i · (𝑦 ·
1))) |
| 15 | | ax-1rid 11225 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ → (𝑦 · 1) = 𝑦) |
| 16 | 15 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ → (i
· (𝑦 · 1)) =
(i · 𝑦)) |
| 17 | 14, 16 | eqtrd 2777 |
. . . . . 6
⊢ (𝑦 ∈ ℝ → ((i
· 𝑦) · 1) =
(i · 𝑦)) |
| 18 | 11, 17 | oveqan12d 7450 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 · 1) + ((i ·
𝑦) · 1)) = (𝑥 + (i · 𝑦))) |
| 19 | 10, 18 | eqtrd 2777 |
. . . 4
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) · 1) = (𝑥 + (i · 𝑦))) |
| 20 | | oveq1 7438 |
. . . . 5
⊢ (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = ((𝑥 + (i · 𝑦)) · 1)) |
| 21 | | id 22 |
. . . . 5
⊢ (𝐴 = (𝑥 + (i · 𝑦)) → 𝐴 = (𝑥 + (i · 𝑦))) |
| 22 | 20, 21 | eqeq12d 2753 |
. . . 4
⊢ (𝐴 = (𝑥 + (i · 𝑦)) → ((𝐴 · 1) = 𝐴 ↔ ((𝑥 + (i · 𝑦)) · 1) = (𝑥 + (i · 𝑦)))) |
| 23 | 19, 22 | syl5ibrcom 247 |
. . 3
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = 𝐴)) |
| 24 | 23 | rexlimivv 3201 |
. 2
⊢
(∃𝑥 ∈
ℝ ∃𝑦 ∈
ℝ 𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = 𝐴) |
| 25 | 1, 24 | syl 17 |
1
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) |