Step | Hyp | Ref
| Expression |
1 | | df-c 7780 |
. 2
⊢ ℂ =
(R × R) |
2 | | eqeq1 2177 |
. . 3
⊢
(〈𝑧, 𝑤〉 = 𝐴 → (〈𝑧, 𝑤〉 = (𝑥 + (i · 𝑦)) ↔ 𝐴 = (𝑥 + (i · 𝑦)))) |
3 | 2 | 2rexbidv 2495 |
. 2
⊢
(〈𝑧, 𝑤〉 = 𝐴 → (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 〈𝑧, 𝑤〉 = (𝑥 + (i · 𝑦)) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))) |
4 | | opelreal 7789 |
. . . . . 6
⊢
(〈𝑧,
0R〉 ∈ ℝ ↔ 𝑧 ∈ R) |
5 | | opelreal 7789 |
. . . . . 6
⊢
(〈𝑤,
0R〉 ∈ ℝ ↔ 𝑤 ∈ R) |
6 | 4, 5 | anbi12i 457 |
. . . . 5
⊢
((〈𝑧,
0R〉 ∈ ℝ ∧ 〈𝑤, 0R〉 ∈
ℝ) ↔ (𝑧 ∈
R ∧ 𝑤
∈ R)) |
7 | 6 | biimpri 132 |
. . . 4
⊢ ((𝑧 ∈ R ∧
𝑤 ∈ R)
→ (〈𝑧,
0R〉 ∈ ℝ ∧ 〈𝑤, 0R〉 ∈
ℝ)) |
8 | | df-i 7783 |
. . . . . . . . 9
⊢ i =
〈0R,
1R〉 |
9 | 8 | oveq1i 5863 |
. . . . . . . 8
⊢ (i
· 〈𝑤,
0R〉) = (〈0R,
1R〉 · 〈𝑤,
0R〉) |
10 | | 0r 7712 |
. . . . . . . . . 10
⊢
0R ∈ R |
11 | | 1sr 7713 |
. . . . . . . . . . 11
⊢
1R ∈ R |
12 | | mulcnsr 7797 |
. . . . . . . . . . 11
⊢
(((0R ∈ R ∧
1R ∈ R) ∧ (𝑤 ∈ R ∧
0R ∈ R)) →
(〈0R, 1R〉 ·
〈𝑤,
0R〉) = 〈((0R
·R 𝑤) +R
(-1R ·R
(1R ·R
0R))), ((1R
·R 𝑤) +R
(0R ·R
0R))〉) |
13 | 10, 11, 12 | mpanl12 434 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ R ∧
0R ∈ R) →
(〈0R, 1R〉 ·
〈𝑤,
0R〉) = 〈((0R
·R 𝑤) +R
(-1R ·R
(1R ·R
0R))), ((1R
·R 𝑤) +R
(0R ·R
0R))〉) |
14 | 10, 13 | mpan2 423 |
. . . . . . . . 9
⊢ (𝑤 ∈ R →
(〈0R, 1R〉 ·
〈𝑤,
0R〉) = 〈((0R
·R 𝑤) +R
(-1R ·R
(1R ·R
0R))), ((1R
·R 𝑤) +R
(0R ·R
0R))〉) |
15 | | mulcomsrg 7719 |
. . . . . . . . . . . . . 14
⊢
((0R ∈ R ∧ 𝑤 ∈ R) →
(0R ·R 𝑤) = (𝑤 ·R
0R)) |
16 | 10, 15 | mpan 422 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ R →
(0R ·R 𝑤) = (𝑤 ·R
0R)) |
17 | | 00sr 7731 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ R →
(𝑤
·R 0R) =
0R) |
18 | 16, 17 | eqtrd 2203 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ R →
(0R ·R 𝑤) =
0R) |
19 | 18 | oveq1d 5868 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ R →
((0R ·R 𝑤) +R
(-1R ·R
(1R ·R
0R))) = (0R
+R (-1R
·R (1R
·R
0R)))) |
20 | | 00sr 7731 |
. . . . . . . . . . . . . . . 16
⊢
(1R ∈ R →
(1R ·R
0R) = 0R) |
21 | 11, 20 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(1R ·R
0R) = 0R |
22 | 21 | oveq2i 5864 |
. . . . . . . . . . . . . 14
⊢
(-1R ·R
(1R ·R
0R)) = (-1R
·R
0R) |
23 | | m1r 7714 |
. . . . . . . . . . . . . . 15
⊢
-1R ∈ R |
24 | | 00sr 7731 |
. . . . . . . . . . . . . . 15
⊢
(-1R ∈ R →
(-1R ·R
0R) = 0R) |
25 | 23, 24 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(-1R ·R
0R) = 0R |
26 | 22, 25 | eqtri 2191 |
. . . . . . . . . . . . 13
⊢
(-1R ·R
(1R ·R
0R)) = 0R |
27 | 26 | oveq2i 5864 |
. . . . . . . . . . . 12
⊢
(0R +R
(-1R ·R
(1R ·R
0R))) = (0R
+R 0R) |
28 | | 0idsr 7729 |
. . . . . . . . . . . . 13
⊢
(0R ∈ R →
(0R +R
0R) = 0R) |
29 | 10, 28 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(0R +R
0R) = 0R |
30 | 27, 29 | eqtri 2191 |
. . . . . . . . . . 11
⊢
(0R +R
(-1R ·R
(1R ·R
0R))) = 0R |
31 | 19, 30 | eqtrdi 2219 |
. . . . . . . . . 10
⊢ (𝑤 ∈ R →
((0R ·R 𝑤) +R
(-1R ·R
(1R ·R
0R))) = 0R) |
32 | | mulcomsrg 7719 |
. . . . . . . . . . . . . 14
⊢
((1R ∈ R ∧ 𝑤 ∈ R) →
(1R ·R 𝑤) = (𝑤 ·R
1R)) |
33 | 11, 32 | mpan 422 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ R →
(1R ·R 𝑤) = (𝑤 ·R
1R)) |
34 | | 1idsr 7730 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ R →
(𝑤
·R 1R) = 𝑤) |
35 | 33, 34 | eqtrd 2203 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ R →
(1R ·R 𝑤) = 𝑤) |
36 | 35 | oveq1d 5868 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ R →
((1R ·R 𝑤) +R
(0R ·R
0R)) = (𝑤 +R
(0R ·R
0R))) |
37 | | 00sr 7731 |
. . . . . . . . . . . . . 14
⊢
(0R ∈ R →
(0R ·R
0R) = 0R) |
38 | 10, 37 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(0R ·R
0R) = 0R |
39 | 38 | oveq2i 5864 |
. . . . . . . . . . . 12
⊢ (𝑤 +R
(0R ·R
0R)) = (𝑤 +R
0R) |
40 | | 0idsr 7729 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ R →
(𝑤
+R 0R) = 𝑤) |
41 | 39, 40 | eqtrid 2215 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ R →
(𝑤
+R (0R
·R 0R)) = 𝑤) |
42 | 36, 41 | eqtrd 2203 |
. . . . . . . . . 10
⊢ (𝑤 ∈ R →
((1R ·R 𝑤) +R
(0R ·R
0R)) = 𝑤) |
43 | 31, 42 | opeq12d 3773 |
. . . . . . . . 9
⊢ (𝑤 ∈ R →
〈((0R ·R 𝑤) +R
(-1R ·R
(1R ·R
0R))), ((1R
·R 𝑤) +R
(0R ·R
0R))〉 = 〈0R, 𝑤〉) |
44 | 14, 43 | eqtrd 2203 |
. . . . . . . 8
⊢ (𝑤 ∈ R →
(〈0R, 1R〉 ·
〈𝑤,
0R〉) = 〈0R, 𝑤〉) |
45 | 9, 44 | eqtrid 2215 |
. . . . . . 7
⊢ (𝑤 ∈ R →
(i · 〈𝑤,
0R〉) = 〈0R, 𝑤〉) |
46 | 45 | oveq2d 5869 |
. . . . . 6
⊢ (𝑤 ∈ R →
(〈𝑧,
0R〉 + (i · 〈𝑤, 0R〉)) =
(〈𝑧,
0R〉 + 〈0R, 𝑤〉)) |
47 | 46 | adantl 275 |
. . . . 5
⊢ ((𝑧 ∈ R ∧
𝑤 ∈ R)
→ (〈𝑧,
0R〉 + (i · 〈𝑤, 0R〉)) =
(〈𝑧,
0R〉 + 〈0R, 𝑤〉)) |
48 | | addcnsr 7796 |
. . . . . . 7
⊢ (((𝑧 ∈ R ∧
0R ∈ R) ∧
(0R ∈ R ∧ 𝑤 ∈ R)) → (〈𝑧,
0R〉 + 〈0R, 𝑤〉) = 〈(𝑧 +R
0R), (0R
+R 𝑤)〉) |
49 | 10, 48 | mpanl2 433 |
. . . . . 6
⊢ ((𝑧 ∈ R ∧
(0R ∈ R ∧ 𝑤 ∈ R)) → (〈𝑧,
0R〉 + 〈0R, 𝑤〉) = 〈(𝑧 +R
0R), (0R
+R 𝑤)〉) |
50 | 10, 49 | mpanr1 435 |
. . . . 5
⊢ ((𝑧 ∈ R ∧
𝑤 ∈ R)
→ (〈𝑧,
0R〉 + 〈0R, 𝑤〉) = 〈(𝑧 +R
0R), (0R
+R 𝑤)〉) |
51 | | 0idsr 7729 |
. . . . . 6
⊢ (𝑧 ∈ R →
(𝑧
+R 0R) = 𝑧) |
52 | | addcomsrg 7717 |
. . . . . . . 8
⊢
((0R ∈ R ∧ 𝑤 ∈ R) →
(0R +R 𝑤) = (𝑤 +R
0R)) |
53 | 10, 52 | mpan 422 |
. . . . . . 7
⊢ (𝑤 ∈ R →
(0R +R 𝑤) = (𝑤 +R
0R)) |
54 | 53, 40 | eqtrd 2203 |
. . . . . 6
⊢ (𝑤 ∈ R →
(0R +R 𝑤) = 𝑤) |
55 | | opeq12 3767 |
. . . . . 6
⊢ (((𝑧 +R
0R) = 𝑧 ∧ (0R
+R 𝑤) = 𝑤) → 〈(𝑧 +R
0R), (0R
+R 𝑤)〉 = 〈𝑧, 𝑤〉) |
56 | 51, 54, 55 | syl2an 287 |
. . . . 5
⊢ ((𝑧 ∈ R ∧
𝑤 ∈ R)
→ 〈(𝑧
+R 0R),
(0R +R 𝑤)〉 = 〈𝑧, 𝑤〉) |
57 | 47, 50, 56 | 3eqtrrd 2208 |
. . . 4
⊢ ((𝑧 ∈ R ∧
𝑤 ∈ R)
→ 〈𝑧, 𝑤〉 = (〈𝑧,
0R〉 + (i · 〈𝑤,
0R〉))) |
58 | | vex 2733 |
. . . . . 6
⊢ 𝑧 ∈ V |
59 | | opexg 4213 |
. . . . . 6
⊢ ((𝑧 ∈ V ∧
0R ∈ R) → 〈𝑧,
0R〉 ∈ V) |
60 | 58, 10, 59 | mp2an 424 |
. . . . 5
⊢
〈𝑧,
0R〉 ∈ V |
61 | | vex 2733 |
. . . . . 6
⊢ 𝑤 ∈ V |
62 | | opexg 4213 |
. . . . . 6
⊢ ((𝑤 ∈ V ∧
0R ∈ R) → 〈𝑤,
0R〉 ∈ V) |
63 | 61, 10, 62 | mp2an 424 |
. . . . 5
⊢
〈𝑤,
0R〉 ∈ V |
64 | | eleq1 2233 |
. . . . . . 7
⊢ (𝑥 = 〈𝑧, 0R〉 →
(𝑥 ∈ ℝ ↔
〈𝑧,
0R〉 ∈ ℝ)) |
65 | | eleq1 2233 |
. . . . . . 7
⊢ (𝑦 = 〈𝑤, 0R〉 →
(𝑦 ∈ ℝ ↔
〈𝑤,
0R〉 ∈ ℝ)) |
66 | 64, 65 | bi2anan9 601 |
. . . . . 6
⊢ ((𝑥 = 〈𝑧, 0R〉 ∧
𝑦 = 〈𝑤,
0R〉) → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ↔ (〈𝑧,
0R〉 ∈ ℝ ∧ 〈𝑤, 0R〉 ∈
ℝ))) |
67 | | oveq1 5860 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑧, 0R〉 →
(𝑥 + (i · 𝑦)) = (〈𝑧, 0R〉 + (i
· 𝑦))) |
68 | | oveq2 5861 |
. . . . . . . . 9
⊢ (𝑦 = 〈𝑤, 0R〉 → (i
· 𝑦) = (i ·
〈𝑤,
0R〉)) |
69 | 68 | oveq2d 5869 |
. . . . . . . 8
⊢ (𝑦 = 〈𝑤, 0R〉 →
(〈𝑧,
0R〉 + (i · 𝑦)) = (〈𝑧, 0R〉 + (i
· 〈𝑤,
0R〉))) |
70 | 67, 69 | sylan9eq 2223 |
. . . . . . 7
⊢ ((𝑥 = 〈𝑧, 0R〉 ∧
𝑦 = 〈𝑤,
0R〉) → (𝑥 + (i · 𝑦)) = (〈𝑧, 0R〉 + (i
· 〈𝑤,
0R〉))) |
71 | 70 | eqeq2d 2182 |
. . . . . 6
⊢ ((𝑥 = 〈𝑧, 0R〉 ∧
𝑦 = 〈𝑤,
0R〉) → (〈𝑧, 𝑤〉 = (𝑥 + (i · 𝑦)) ↔ 〈𝑧, 𝑤〉 = (〈𝑧, 0R〉 + (i
· 〈𝑤,
0R〉)))) |
72 | 66, 71 | anbi12d 470 |
. . . . 5
⊢ ((𝑥 = 〈𝑧, 0R〉 ∧
𝑦 = 〈𝑤,
0R〉) → (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 〈𝑧, 𝑤〉 = (𝑥 + (i · 𝑦))) ↔ ((〈𝑧, 0R〉 ∈
ℝ ∧ 〈𝑤,
0R〉 ∈ ℝ) ∧ 〈𝑧, 𝑤〉 = (〈𝑧, 0R〉 + (i
· 〈𝑤,
0R〉))))) |
73 | 60, 63, 72 | spc2ev 2826 |
. . . 4
⊢
(((〈𝑧,
0R〉 ∈ ℝ ∧ 〈𝑤, 0R〉 ∈
ℝ) ∧ 〈𝑧,
𝑤〉 = (〈𝑧,
0R〉 + (i · 〈𝑤, 0R〉))) →
∃𝑥∃𝑦((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 〈𝑧, 𝑤〉 = (𝑥 + (i · 𝑦)))) |
74 | 7, 57, 73 | syl2anc 409 |
. . 3
⊢ ((𝑧 ∈ R ∧
𝑤 ∈ R)
→ ∃𝑥∃𝑦((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 〈𝑧, 𝑤〉 = (𝑥 + (i · 𝑦)))) |
75 | | r2ex 2490 |
. . 3
⊢
(∃𝑥 ∈
ℝ ∃𝑦 ∈
ℝ 〈𝑧, 𝑤〉 = (𝑥 + (i · 𝑦)) ↔ ∃𝑥∃𝑦((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 〈𝑧, 𝑤〉 = (𝑥 + (i · 𝑦)))) |
76 | 74, 75 | sylibr 133 |
. 2
⊢ ((𝑧 ∈ R ∧
𝑤 ∈ R)
→ ∃𝑥 ∈
ℝ ∃𝑦 ∈
ℝ 〈𝑧, 𝑤〉 = (𝑥 + (i · 𝑦))) |
77 | 1, 3, 76 | optocl 4687 |
1
⊢ (𝐴 ∈ ℂ →
∃𝑥 ∈ ℝ
∃𝑦 ∈ ℝ
𝐴 = (𝑥 + (i · 𝑦))) |