Step | Hyp | Ref
| Expression |
1 | | df-c 10861 |
. 2
⊢ ℂ =
(R × R) |
2 | | eqeq1 2743 |
. . 3
⊢
(〈𝑧, 𝑤〉 = 𝐴 → (〈𝑧, 𝑤〉 = (𝑥 + (i · 𝑦)) ↔ 𝐴 = (𝑥 + (i · 𝑦)))) |
3 | 2 | 2rexbidv 3230 |
. 2
⊢
(〈𝑧, 𝑤〉 = 𝐴 → (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 〈𝑧, 𝑤〉 = (𝑥 + (i · 𝑦)) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))) |
4 | | opelreal 10870 |
. . . . . 6
⊢
(〈𝑧,
0R〉 ∈ ℝ ↔ 𝑧 ∈ R) |
5 | | opelreal 10870 |
. . . . . 6
⊢
(〈𝑤,
0R〉 ∈ ℝ ↔ 𝑤 ∈ R) |
6 | 4, 5 | anbi12i 626 |
. . . . 5
⊢
((〈𝑧,
0R〉 ∈ ℝ ∧ 〈𝑤, 0R〉 ∈
ℝ) ↔ (𝑧 ∈
R ∧ 𝑤
∈ R)) |
7 | 6 | biimpri 227 |
. . . 4
⊢ ((𝑧 ∈ R ∧
𝑤 ∈ R)
→ (〈𝑧,
0R〉 ∈ ℝ ∧ 〈𝑤, 0R〉 ∈
ℝ)) |
8 | | df-i 10864 |
. . . . . . . . 9
⊢ i =
〈0R,
1R〉 |
9 | 8 | oveq1i 7278 |
. . . . . . . 8
⊢ (i
· 〈𝑤,
0R〉) = (〈0R,
1R〉 · 〈𝑤,
0R〉) |
10 | | 0r 10820 |
. . . . . . . . . 10
⊢
0R ∈ R |
11 | | 1sr 10821 |
. . . . . . . . . . 11
⊢
1R ∈ R |
12 | | mulcnsr 10876 |
. . . . . . . . . . 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 698 |
. . . . . . . . . 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 687 |
. . . . . . . . 9
⊢ (𝑤 ∈ R →
(〈0R, 1R〉 ·
〈𝑤,
0R〉) = 〈((0R
·R 𝑤) +R
(-1R ·R
(1R ·R
0R))), ((1R
·R 𝑤) +R
(0R ·R
0R))〉) |
15 | | mulcomsr 10829 |
. . . . . . . . . . . . 13
⊢
(0R ·R 𝑤) = (𝑤 ·R
0R) |
16 | | 00sr 10839 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ R →
(𝑤
·R 0R) =
0R) |
17 | 15, 16 | eqtrid 2791 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ R →
(0R ·R 𝑤) =
0R) |
18 | 17 | oveq1d 7283 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ R →
((0R ·R 𝑤) +R
(-1R ·R
(1R ·R
0R))) = (0R
+R (-1R
·R (1R
·R
0R)))) |
19 | | 00sr 10839 |
. . . . . . . . . . . . . . . 16
⊢
(1R ∈ R →
(1R ·R
0R) = 0R) |
20 | 11, 19 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(1R ·R
0R) = 0R |
21 | 20 | oveq2i 7279 |
. . . . . . . . . . . . . 14
⊢
(-1R ·R
(1R ·R
0R)) = (-1R
·R
0R) |
22 | | m1r 10822 |
. . . . . . . . . . . . . . 15
⊢
-1R ∈ R |
23 | | 00sr 10839 |
. . . . . . . . . . . . . . 15
⊢
(-1R ∈ R →
(-1R ·R
0R) = 0R) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(-1R ·R
0R) = 0R |
25 | 21, 24 | eqtri 2767 |
. . . . . . . . . . . . 13
⊢
(-1R ·R
(1R ·R
0R)) = 0R |
26 | 25 | oveq2i 7279 |
. . . . . . . . . . . 12
⊢
(0R +R
(-1R ·R
(1R ·R
0R))) = (0R
+R 0R) |
27 | | 0idsr 10837 |
. . . . . . . . . . . . 13
⊢
(0R ∈ R →
(0R +R
0R) = 0R) |
28 | 10, 27 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(0R +R
0R) = 0R |
29 | 26, 28 | eqtri 2767 |
. . . . . . . . . . 11
⊢
(0R +R
(-1R ·R
(1R ·R
0R))) = 0R |
30 | 18, 29 | eqtrdi 2795 |
. . . . . . . . . 10
⊢ (𝑤 ∈ R →
((0R ·R 𝑤) +R
(-1R ·R
(1R ·R
0R))) = 0R) |
31 | | mulcomsr 10829 |
. . . . . . . . . . . . 13
⊢
(1R ·R 𝑤) = (𝑤 ·R
1R) |
32 | | 1idsr 10838 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ R →
(𝑤
·R 1R) = 𝑤) |
33 | 31, 32 | eqtrid 2791 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ R →
(1R ·R 𝑤) = 𝑤) |
34 | 33 | oveq1d 7283 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ R →
((1R ·R 𝑤) +R
(0R ·R
0R)) = (𝑤 +R
(0R ·R
0R))) |
35 | | 00sr 10839 |
. . . . . . . . . . . . . 14
⊢
(0R ∈ R →
(0R ·R
0R) = 0R) |
36 | 10, 35 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(0R ·R
0R) = 0R |
37 | 36 | oveq2i 7279 |
. . . . . . . . . . . 12
⊢ (𝑤 +R
(0R ·R
0R)) = (𝑤 +R
0R) |
38 | | 0idsr 10837 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ R →
(𝑤
+R 0R) = 𝑤) |
39 | 37, 38 | eqtrid 2791 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ R →
(𝑤
+R (0R
·R 0R)) = 𝑤) |
40 | 34, 39 | eqtrd 2779 |
. . . . . . . . . 10
⊢ (𝑤 ∈ R →
((1R ·R 𝑤) +R
(0R ·R
0R)) = 𝑤) |
41 | 30, 40 | opeq12d 4817 |
. . . . . . . . 9
⊢ (𝑤 ∈ R →
〈((0R ·R 𝑤) +R
(-1R ·R
(1R ·R
0R))), ((1R
·R 𝑤) +R
(0R ·R
0R))〉 = 〈0R, 𝑤〉) |
42 | 14, 41 | eqtrd 2779 |
. . . . . . . 8
⊢ (𝑤 ∈ R →
(〈0R, 1R〉 ·
〈𝑤,
0R〉) = 〈0R, 𝑤〉) |
43 | 9, 42 | eqtrid 2791 |
. . . . . . 7
⊢ (𝑤 ∈ R →
(i · 〈𝑤,
0R〉) = 〈0R, 𝑤〉) |
44 | 43 | oveq2d 7284 |
. . . . . 6
⊢ (𝑤 ∈ R →
(〈𝑧,
0R〉 + (i · 〈𝑤, 0R〉)) =
(〈𝑧,
0R〉 + 〈0R, 𝑤〉)) |
45 | 44 | adantl 481 |
. . . . 5
⊢ ((𝑧 ∈ R ∧
𝑤 ∈ R)
→ (〈𝑧,
0R〉 + (i · 〈𝑤, 0R〉)) =
(〈𝑧,
0R〉 + 〈0R, 𝑤〉)) |
46 | | addcnsr 10875 |
. . . . . . 7
⊢ (((𝑧 ∈ R ∧
0R ∈ R) ∧
(0R ∈ R ∧ 𝑤 ∈ R)) → (〈𝑧,
0R〉 + 〈0R, 𝑤〉) = 〈(𝑧 +R
0R), (0R
+R 𝑤)〉) |
47 | 10, 46 | mpanl2 697 |
. . . . . 6
⊢ ((𝑧 ∈ R ∧
(0R ∈ R ∧ 𝑤 ∈ R)) → (〈𝑧,
0R〉 + 〈0R, 𝑤〉) = 〈(𝑧 +R
0R), (0R
+R 𝑤)〉) |
48 | 10, 47 | mpanr1 699 |
. . . . 5
⊢ ((𝑧 ∈ R ∧
𝑤 ∈ R)
→ (〈𝑧,
0R〉 + 〈0R, 𝑤〉) = 〈(𝑧 +R
0R), (0R
+R 𝑤)〉) |
49 | | 0idsr 10837 |
. . . . . 6
⊢ (𝑧 ∈ R →
(𝑧
+R 0R) = 𝑧) |
50 | | addcomsr 10827 |
. . . . . . 7
⊢
(0R +R 𝑤) = (𝑤 +R
0R) |
51 | 50, 38 | eqtrid 2791 |
. . . . . 6
⊢ (𝑤 ∈ R →
(0R +R 𝑤) = 𝑤) |
52 | | opeq12 4811 |
. . . . . 6
⊢ (((𝑧 +R
0R) = 𝑧 ∧ (0R
+R 𝑤) = 𝑤) → 〈(𝑧 +R
0R), (0R
+R 𝑤)〉 = 〈𝑧, 𝑤〉) |
53 | 49, 51, 52 | syl2an 595 |
. . . . 5
⊢ ((𝑧 ∈ R ∧
𝑤 ∈ R)
→ 〈(𝑧
+R 0R),
(0R +R 𝑤)〉 = 〈𝑧, 𝑤〉) |
54 | 45, 48, 53 | 3eqtrrd 2784 |
. . . 4
⊢ ((𝑧 ∈ R ∧
𝑤 ∈ R)
→ 〈𝑧, 𝑤〉 = (〈𝑧,
0R〉 + (i · 〈𝑤,
0R〉))) |
55 | | opex 5381 |
. . . . 5
⊢
〈𝑧,
0R〉 ∈ V |
56 | | opex 5381 |
. . . . 5
⊢
〈𝑤,
0R〉 ∈ V |
57 | | eleq1 2827 |
. . . . . . 7
⊢ (𝑥 = 〈𝑧, 0R〉 →
(𝑥 ∈ ℝ ↔
〈𝑧,
0R〉 ∈ ℝ)) |
58 | | eleq1 2827 |
. . . . . . 7
⊢ (𝑦 = 〈𝑤, 0R〉 →
(𝑦 ∈ ℝ ↔
〈𝑤,
0R〉 ∈ ℝ)) |
59 | 57, 58 | bi2anan9 635 |
. . . . . 6
⊢ ((𝑥 = 〈𝑧, 0R〉 ∧
𝑦 = 〈𝑤,
0R〉) → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ↔ (〈𝑧,
0R〉 ∈ ℝ ∧ 〈𝑤, 0R〉 ∈
ℝ))) |
60 | | oveq1 7275 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑧, 0R〉 →
(𝑥 + (i · 𝑦)) = (〈𝑧, 0R〉 + (i
· 𝑦))) |
61 | | oveq2 7276 |
. . . . . . . . 9
⊢ (𝑦 = 〈𝑤, 0R〉 → (i
· 𝑦) = (i ·
〈𝑤,
0R〉)) |
62 | 61 | oveq2d 7284 |
. . . . . . . 8
⊢ (𝑦 = 〈𝑤, 0R〉 →
(〈𝑧,
0R〉 + (i · 𝑦)) = (〈𝑧, 0R〉 + (i
· 〈𝑤,
0R〉))) |
63 | 60, 62 | sylan9eq 2799 |
. . . . . . 7
⊢ ((𝑥 = 〈𝑧, 0R〉 ∧
𝑦 = 〈𝑤,
0R〉) → (𝑥 + (i · 𝑦)) = (〈𝑧, 0R〉 + (i
· 〈𝑤,
0R〉))) |
64 | 63 | eqeq2d 2750 |
. . . . . 6
⊢ ((𝑥 = 〈𝑧, 0R〉 ∧
𝑦 = 〈𝑤,
0R〉) → (〈𝑧, 𝑤〉 = (𝑥 + (i · 𝑦)) ↔ 〈𝑧, 𝑤〉 = (〈𝑧, 0R〉 + (i
· 〈𝑤,
0R〉)))) |
65 | 59, 64 | anbi12d 630 |
. . . . 5
⊢ ((𝑥 = 〈𝑧, 0R〉 ∧
𝑦 = 〈𝑤,
0R〉) → (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 〈𝑧, 𝑤〉 = (𝑥 + (i · 𝑦))) ↔ ((〈𝑧, 0R〉 ∈
ℝ ∧ 〈𝑤,
0R〉 ∈ ℝ) ∧ 〈𝑧, 𝑤〉 = (〈𝑧, 0R〉 + (i
· 〈𝑤,
0R〉))))) |
66 | 55, 56, 65 | spc2ev 3544 |
. . . 4
⊢
(((〈𝑧,
0R〉 ∈ ℝ ∧ 〈𝑤, 0R〉 ∈
ℝ) ∧ 〈𝑧,
𝑤〉 = (〈𝑧,
0R〉 + (i · 〈𝑤, 0R〉))) →
∃𝑥∃𝑦((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 〈𝑧, 𝑤〉 = (𝑥 + (i · 𝑦)))) |
67 | 7, 54, 66 | syl2anc 583 |
. . 3
⊢ ((𝑧 ∈ R ∧
𝑤 ∈ R)
→ ∃𝑥∃𝑦((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 〈𝑧, 𝑤〉 = (𝑥 + (i · 𝑦)))) |
68 | | r2ex 3233 |
. . 3
⊢
(∃𝑥 ∈
ℝ ∃𝑦 ∈
ℝ 〈𝑧, 𝑤〉 = (𝑥 + (i · 𝑦)) ↔ ∃𝑥∃𝑦((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 〈𝑧, 𝑤〉 = (𝑥 + (i · 𝑦)))) |
69 | 67, 68 | sylibr 233 |
. 2
⊢ ((𝑧 ∈ R ∧
𝑤 ∈ R)
→ ∃𝑥 ∈
ℝ ∃𝑦 ∈
ℝ 〈𝑧, 𝑤〉 = (𝑥 + (i · 𝑦))) |
70 | 1, 3, 69 | optocl 5679 |
1
⊢ (𝐴 ∈ ℂ →
∃𝑥 ∈ ℝ
∃𝑦 ∈ ℝ
𝐴 = (𝑥 + (i · 𝑦))) |