Step | Hyp | Ref
| Expression |
1 | | cnre 6821 |
. 2
⊢ (A ∈ ℂ →
∃x ∈ ℝ ∃y ∈ ℝ A =
(x + (i · y))) |
2 | | recn 6812 |
. . . . . 6
⊢ (x ∈ ℝ →
x ∈
ℂ) |
3 | | ax-icn 6778 |
. . . . . . 7
⊢ i ∈ ℂ |
4 | | recn 6812 |
. . . . . . 7
⊢ (y ∈ ℝ →
y ∈
ℂ) |
5 | | mulcl 6806 |
. . . . . . 7
⊢ ((i ∈ ℂ ∧
y ∈
ℂ) → (i · y) ∈ ℂ) |
6 | 3, 4, 5 | sylancr 393 |
. . . . . 6
⊢ (y ∈ ℝ →
(i · y) ∈ ℂ) |
7 | | ax-1cn 6776 |
. . . . . . 7
⊢ 1 ∈ ℂ |
8 | | adddir 6816 |
. . . . . . 7
⊢
((x ∈ ℂ ∧ (i
· y) ∈ ℂ ∧ 1
∈ ℂ) → ((x + (i · y)) · 1) = ((x · 1) + ((i · y) · 1))) |
9 | 7, 8 | mp3an3 1220 |
. . . . . 6
⊢
((x ∈ ℂ ∧ (i
· y) ∈ ℂ) → ((x + (i · y)) · 1) = ((x · 1) + ((i · y) · 1))) |
10 | 2, 6, 9 | syl2an 273 |
. . . . 5
⊢
((x ∈ ℝ ∧
y ∈
ℝ) → ((x + (i · y)) · 1) = ((x · 1) + ((i · y) · 1))) |
11 | | ax-1rid 6790 |
. . . . . 6
⊢ (x ∈ ℝ →
(x · 1) = x) |
12 | | mulass 6810 |
. . . . . . . . 9
⊢ ((i ∈ ℂ ∧
y ∈
ℂ ∧ 1 ∈ ℂ) → ((i · y) · 1) = (i · (y · 1))) |
13 | 3, 7, 12 | mp3an13 1222 |
. . . . . . . 8
⊢ (y ∈ ℂ →
((i · y) · 1) = (i ·
(y · 1))) |
14 | 4, 13 | syl 14 |
. . . . . . 7
⊢ (y ∈ ℝ →
((i · y) · 1) = (i ·
(y · 1))) |
15 | | ax-1rid 6790 |
. . . . . . . 8
⊢ (y ∈ ℝ →
(y · 1) = y) |
16 | 15 | oveq2d 5471 |
. . . . . . 7
⊢ (y ∈ ℝ →
(i · (y · 1)) = (i ·
y)) |
17 | 14, 16 | eqtrd 2069 |
. . . . . 6
⊢ (y ∈ ℝ →
((i · y) · 1) = (i ·
y)) |
18 | 11, 17 | oveqan12d 5474 |
. . . . 5
⊢
((x ∈ ℝ ∧
y ∈
ℝ) → ((x · 1) + ((i
· y) · 1)) = (x + (i · y))) |
19 | 10, 18 | eqtrd 2069 |
. . . 4
⊢
((x ∈ ℝ ∧
y ∈
ℝ) → ((x + (i · y)) · 1) = (x + (i · y))) |
20 | | oveq1 5462 |
. . . . 5
⊢ (A = (x + (i
· y)) → (A · 1) = ((x + (i · y)) · 1)) |
21 | | id 19 |
. . . . 5
⊢ (A = (x + (i
· y)) → A = (x + (i
· y))) |
22 | 20, 21 | eqeq12d 2051 |
. . . 4
⊢ (A = (x + (i
· y)) → ((A · 1) = A ↔ ((x +
(i · y)) · 1) = (x + (i · y)))) |
23 | 19, 22 | syl5ibrcom 146 |
. . 3
⊢
((x ∈ ℝ ∧
y ∈
ℝ) → (A = (x + (i · y)) → (A
· 1) = A)) |
24 | 23 | rexlimivv 2432 |
. 2
⊢ (∃x ∈ ℝ ∃y ∈ ℝ A =
(x + (i · y)) → (A
· 1) = A) |
25 | 1, 24 | syl 14 |
1
⊢ (A ∈ ℂ →
(A · 1) = A) |