Step | Hyp | Ref
| Expression |
1 | | cnre 10983 |
. 2
⊢ (𝐴 ∈ ℂ →
∃𝑥 ∈ ℝ
∃𝑦 ∈ ℝ
𝐴 = (𝑥 + (i · 𝑦))) |
2 | | recn 10972 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
3 | | ax-icn 10941 |
. . . . . . 7
⊢ i ∈
ℂ |
4 | | recn 10972 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
5 | | mulcl 10966 |
. . . . . . 7
⊢ ((i
∈ ℂ ∧ 𝑦
∈ ℂ) → (i · 𝑦) ∈ ℂ) |
6 | 3, 4, 5 | sylancr 587 |
. . . . . 6
⊢ (𝑦 ∈ ℝ → (i
· 𝑦) ∈
ℂ) |
7 | | ax-1cn 10940 |
. . . . . . 7
⊢ 1 ∈
ℂ |
8 | | adddir 10977 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ (i
· 𝑦) ∈ ℂ
∧ 1 ∈ ℂ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1))) |
9 | 7, 8 | mp3an3 1449 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ (i
· 𝑦) ∈ ℂ)
→ ((𝑥 + (i ·
𝑦)) · 1) = ((𝑥 · 1) + ((i ·
𝑦) ·
1))) |
10 | 2, 6, 9 | syl2an 596 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i ·
𝑦) ·
1))) |
11 | | ax-1rid 10952 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → (𝑥 · 1) = 𝑥) |
12 | | mulass 10970 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ 𝑦
∈ ℂ ∧ 1 ∈ ℂ) → ((i · 𝑦) · 1) = (i · (𝑦 · 1))) |
13 | 3, 7, 12 | mp3an13 1451 |
. . . . . . . 8
⊢ (𝑦 ∈ ℂ → ((i
· 𝑦) · 1) =
(i · (𝑦 ·
1))) |
14 | 4, 13 | syl 17 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ → ((i
· 𝑦) · 1) =
(i · (𝑦 ·
1))) |
15 | | ax-1rid 10952 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ → (𝑦 · 1) = 𝑦) |
16 | 15 | oveq2d 7288 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ → (i
· (𝑦 · 1)) =
(i · 𝑦)) |
17 | 14, 16 | eqtrd 2780 |
. . . . . 6
⊢ (𝑦 ∈ ℝ → ((i
· 𝑦) · 1) =
(i · 𝑦)) |
18 | 11, 17 | oveqan12d 7291 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 · 1) + ((i ·
𝑦) · 1)) = (𝑥 + (i · 𝑦))) |
19 | 10, 18 | eqtrd 2780 |
. . . 4
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) · 1) = (𝑥 + (i · 𝑦))) |
20 | | oveq1 7279 |
. . . . 5
⊢ (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = ((𝑥 + (i · 𝑦)) · 1)) |
21 | | id 22 |
. . . . 5
⊢ (𝐴 = (𝑥 + (i · 𝑦)) → 𝐴 = (𝑥 + (i · 𝑦))) |
22 | 20, 21 | eqeq12d 2756 |
. . . 4
⊢ (𝐴 = (𝑥 + (i · 𝑦)) → ((𝐴 · 1) = 𝐴 ↔ ((𝑥 + (i · 𝑦)) · 1) = (𝑥 + (i · 𝑦)))) |
23 | 19, 22 | syl5ibrcom 246 |
. . 3
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = 𝐴)) |
24 | 23 | rexlimivv 3223 |
. 2
⊢
(∃𝑥 ∈
ℝ ∃𝑦 ∈
ℝ 𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = 𝐴) |
25 | 1, 24 | syl 17 |
1
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) |