Step | Hyp | Ref
| Expression |
1 | | cnre 6821 |
. . 3
⊢ (A ∈ ℂ →
∃y ∈ ℝ ∃z ∈ ℝ A =
(y + (i · z))) |
2 | | recn 6812 |
. . . . . . 7
⊢ (y ∈ ℝ →
y ∈
ℂ) |
3 | | ax-icn 6778 |
. . . . . . . 8
⊢ i ∈ ℂ |
4 | | recn 6812 |
. . . . . . . 8
⊢ (z ∈ ℝ →
z ∈
ℂ) |
5 | | mulcl 6806 |
. . . . . . . 8
⊢ ((i ∈ ℂ ∧
z ∈
ℂ) → (i · z) ∈ ℂ) |
6 | 3, 4, 5 | sylancr 393 |
. . . . . . 7
⊢ (z ∈ ℝ →
(i · z) ∈ ℂ) |
7 | | subcl 7007 |
. . . . . . 7
⊢
((y ∈ ℂ ∧ (i
· z) ∈ ℂ) → (y − (i · z)) ∈
ℂ) |
8 | 2, 6, 7 | syl2an 273 |
. . . . . 6
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → (y − (i ·
z)) ∈
ℂ) |
9 | 2 | adantr 261 |
. . . . . . . 8
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → y ∈ ℂ) |
10 | 6 | adantl 262 |
. . . . . . . 8
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → (i · z) ∈ ℂ) |
11 | 9, 10, 9 | ppncand 7158 |
. . . . . . 7
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → ((y + (i · z)) + (y −
(i · z))) = (y + y)) |
12 | | readdcl 6805 |
. . . . . . . . 9
⊢
((y ∈ ℝ ∧
y ∈
ℝ) → (y + y) ∈
ℝ) |
13 | 12 | anidms 377 |
. . . . . . . 8
⊢ (y ∈ ℝ →
(y + y)
∈ ℝ) |
14 | 13 | adantr 261 |
. . . . . . 7
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → (y + y) ∈
ℝ) |
15 | 11, 14 | eqeltrd 2111 |
. . . . . 6
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → ((y + (i · z)) + (y −
(i · z))) ∈ ℝ) |
16 | 9, 10, 10 | pnncand 7157 |
. . . . . . . . . 10
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → ((y + (i · z)) − (y
− (i · z))) = ((i ·
z) + (i · z))) |
17 | 3 | a1i 9 |
. . . . . . . . . . 11
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → i ∈ ℂ) |
18 | 4 | adantl 262 |
. . . . . . . . . . 11
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → z ∈ ℂ) |
19 | 17, 18, 18 | adddid 6849 |
. . . . . . . . . 10
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → (i · (z + z)) = ((i · z) + (i · z))) |
20 | 16, 19 | eqtr4d 2072 |
. . . . . . . . 9
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → ((y + (i · z)) − (y
− (i · z))) = (i ·
(z + z))) |
21 | 20 | oveq2d 5471 |
. . . . . . . 8
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → (i · ((y + (i
· z)) − (y − (i · z)))) = (i · (i · (z + z)))) |
22 | 18, 18 | addcld 6844 |
. . . . . . . . 9
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → (z + z) ∈
ℂ) |
23 | | mulass 6810 |
. . . . . . . . . 10
⊢ ((i ∈ ℂ ∧ i
∈ ℂ ∧
(z + z)
∈ ℂ) → ((i · i) ·
(z + z)) = (i · (i · (z + z)))) |
24 | 3, 3, 23 | mp3an12 1221 |
. . . . . . . . 9
⊢
((z + z) ∈ ℂ
→ ((i · i) · (z +
z)) = (i · (i · (z + z)))) |
25 | 22, 24 | syl 14 |
. . . . . . . 8
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → ((i · i) · (z
+ z)) = (i · (i · (z + z)))) |
26 | 21, 25 | eqtr4d 2072 |
. . . . . . 7
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → (i · ((y + (i
· z)) − (y − (i · z)))) = ((i · i) · (z + z))) |
27 | | ixi 7367 |
. . . . . . . . 9
⊢ (i
· i) = -1 |
28 | | 1re 6824 |
. . . . . . . . . 10
⊢ 1 ∈ ℝ |
29 | 28 | renegcli 7069 |
. . . . . . . . 9
⊢ -1 ∈ ℝ |
30 | 27, 29 | eqeltri 2107 |
. . . . . . . 8
⊢ (i
· i) ∈ ℝ |
31 | | simpr 103 |
. . . . . . . . 9
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → z ∈ ℝ) |
32 | 31, 31 | readdcld 6852 |
. . . . . . . 8
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → (z + z) ∈
ℝ) |
33 | | remulcl 6807 |
. . . . . . . 8
⊢ (((i
· i) ∈ ℝ ∧ (z + z) ∈ ℝ)
→ ((i · i) · (z +
z)) ∈
ℝ) |
34 | 30, 32, 33 | sylancr 393 |
. . . . . . 7
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → ((i · i) · (z
+ z)) ∈
ℝ) |
35 | 26, 34 | eqeltrd 2111 |
. . . . . 6
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → (i · ((y + (i
· z)) − (y − (i · z)))) ∈
ℝ) |
36 | | oveq2 5463 |
. . . . . . . . 9
⊢ (x = (y −
(i · z)) → ((y + (i · z)) + x) =
((y + (i · z)) + (y −
(i · z)))) |
37 | 36 | eleq1d 2103 |
. . . . . . . 8
⊢ (x = (y −
(i · z)) → (((y + (i · z)) + x) ∈ ℝ ↔ ((y + (i · z)) + (y −
(i · z))) ∈ ℝ)) |
38 | | oveq2 5463 |
. . . . . . . . . 10
⊢ (x = (y −
(i · z)) → ((y + (i · z)) − x) =
((y + (i · z)) − (y
− (i · z)))) |
39 | 38 | oveq2d 5471 |
. . . . . . . . 9
⊢ (x = (y −
(i · z)) → (i ·
((y + (i · z)) − x))
= (i · ((y + (i · z)) − (y
− (i · z))))) |
40 | 39 | eleq1d 2103 |
. . . . . . . 8
⊢ (x = (y −
(i · z)) → ((i ·
((y + (i · z)) − x))
∈ ℝ ↔ (i · ((y + (i · z)) − (y
− (i · z)))) ∈ ℝ)) |
41 | 37, 40 | anbi12d 442 |
. . . . . . 7
⊢ (x = (y −
(i · z)) → ((((y + (i · z)) + x) ∈ ℝ ∧ (i
· ((y + (i · z)) − x))
∈ ℝ) ↔ (((y + (i · z)) + (y −
(i · z))) ∈ ℝ ∧ (i
· ((y + (i · z)) − (y
− (i · z)))) ∈ ℝ))) |
42 | 41 | rspcev 2650 |
. . . . . 6
⊢
(((y − (i · z)) ∈ ℂ
∧ (((y +
(i · z)) + (y − (i · z))) ∈ ℝ
∧ (i · ((y + (i · z)) − (y
− (i · z)))) ∈ ℝ)) → ∃x ∈ ℂ (((y
+ (i · z)) + x) ∈ ℝ ∧ (i · ((y + (i · z)) − x))
∈ ℝ)) |
43 | 8, 15, 35, 42 | syl12anc 1132 |
. . . . 5
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → ∃x ∈ ℂ
(((y + (i · z)) + x) ∈ ℝ ∧ (i
· ((y + (i · z)) − x))
∈ ℝ)) |
44 | | oveq1 5462 |
. . . . . . . 8
⊢ (A = (y + (i
· z)) → (A + x) =
((y + (i · z)) + x)) |
45 | 44 | eleq1d 2103 |
. . . . . . 7
⊢ (A = (y + (i
· z)) → ((A + x) ∈ ℝ ↔ ((y + (i · z)) + x) ∈ ℝ)) |
46 | | oveq1 5462 |
. . . . . . . . 9
⊢ (A = (y + (i
· z)) → (A − x) =
((y + (i · z)) − x)) |
47 | 46 | oveq2d 5471 |
. . . . . . . 8
⊢ (A = (y + (i
· z)) → (i · (A − x)) =
(i · ((y + (i · z)) − x))) |
48 | 47 | eleq1d 2103 |
. . . . . . 7
⊢ (A = (y + (i
· z)) → ((i · (A − x))
∈ ℝ ↔ (i · ((y + (i · z)) − x))
∈ ℝ)) |
49 | 45, 48 | anbi12d 442 |
. . . . . 6
⊢ (A = (y + (i
· z)) → (((A + x) ∈ ℝ ∧ (i
· (A − x)) ∈ ℝ)
↔ (((y + (i · z)) + x) ∈ ℝ ∧ (i
· ((y + (i · z)) − x))
∈ ℝ))) |
50 | 49 | rexbidv 2321 |
. . . . 5
⊢ (A = (y + (i
· z)) → (∃x ∈ ℂ ((A +
x) ∈
ℝ ∧ (i · (A − x))
∈ ℝ) ↔ ∃x ∈ ℂ (((y
+ (i · z)) + x) ∈ ℝ ∧ (i · ((y + (i · z)) − x))
∈ ℝ))) |
51 | 43, 50 | syl5ibrcom 146 |
. . . 4
⊢
((y ∈ ℝ ∧
z ∈
ℝ) → (A = (y + (i · z)) → ∃x ∈ ℂ ((A +
x) ∈
ℝ ∧ (i · (A − x))
∈ ℝ))) |
52 | 51 | rexlimivv 2432 |
. . 3
⊢ (∃y ∈ ℝ ∃z ∈ ℝ A =
(y + (i · z)) → ∃x ∈ ℂ ((A +
x) ∈
ℝ ∧ (i · (A − x))
∈ ℝ)) |
53 | 1, 52 | syl 14 |
. 2
⊢ (A ∈ ℂ →
∃x ∈ ℂ ((A +
x) ∈
ℝ ∧ (i · (A − x))
∈ ℝ)) |
54 | | an4 520 |
. . . 4
⊢
((((A + x) ∈ ℝ ∧ (i · (A
− x)) ∈ ℝ) ∧
((A + y) ∈ ℝ ∧ (i · (A
− y)) ∈ ℝ)) ↔ (((A + x) ∈ ℝ ∧
(A + y)
∈ ℝ) ∧
((i · (A − x)) ∈ ℝ
∧ (i · (A − y))
∈ ℝ))) |
55 | | resubcl 7071 |
. . . . . . 7
⊢
(((A + x) ∈ ℝ ∧ (A + y) ∈ ℝ)
→ ((A + x) − (A +
y)) ∈
ℝ) |
56 | | pnpcan 7046 |
. . . . . . . . 9
⊢
((A ∈ ℂ ∧
x ∈
ℂ ∧ y ∈ ℂ)
→ ((A + x) − (A +
y)) = (x − y)) |
57 | 56 | 3expb 1104 |
. . . . . . . 8
⊢
((A ∈ ℂ ∧
(x ∈
ℂ ∧ y ∈ ℂ))
→ ((A + x) − (A +
y)) = (x − y)) |
58 | 57 | eleq1d 2103 |
. . . . . . 7
⊢
((A ∈ ℂ ∧
(x ∈
ℂ ∧ y ∈ ℂ))
→ (((A + x) − (A +
y)) ∈
ℝ ↔ (x − y) ∈
ℝ)) |
59 | 55, 58 | syl5ib 143 |
. . . . . 6
⊢
((A ∈ ℂ ∧
(x ∈
ℂ ∧ y ∈ ℂ))
→ (((A + x) ∈ ℝ ∧ (A + y) ∈ ℝ)
→ (x − y) ∈
ℝ)) |
60 | | resubcl 7071 |
. . . . . . . 8
⊢ (((i
· (A − y)) ∈ ℝ
∧ (i · (A − x))
∈ ℝ) → ((i · (A − y))
− (i · (A − x))) ∈
ℝ) |
61 | 60 | ancoms 255 |
. . . . . . 7
⊢ (((i
· (A − x)) ∈ ℝ
∧ (i · (A − y))
∈ ℝ) → ((i · (A − y))
− (i · (A − x))) ∈
ℝ) |
62 | 3 | a1i 9 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧
(x ∈
ℂ ∧ y ∈ ℂ))
→ i ∈ ℂ) |
63 | | subcl 7007 |
. . . . . . . . . . 11
⊢
((A ∈ ℂ ∧
y ∈
ℂ) → (A − y) ∈
ℂ) |
64 | 63 | adantrl 447 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧
(x ∈
ℂ ∧ y ∈ ℂ))
→ (A − y) ∈
ℂ) |
65 | | subcl 7007 |
. . . . . . . . . . 11
⊢
((A ∈ ℂ ∧
x ∈
ℂ) → (A − x) ∈
ℂ) |
66 | 65 | adantrr 448 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧
(x ∈
ℂ ∧ y ∈ ℂ))
→ (A − x) ∈
ℂ) |
67 | 62, 64, 66 | subdid 7207 |
. . . . . . . . 9
⊢
((A ∈ ℂ ∧
(x ∈
ℂ ∧ y ∈ ℂ))
→ (i · ((A − y) − (A
− x))) = ((i · (A − y))
− (i · (A − x)))) |
68 | | nnncan1 7043 |
. . . . . . . . . . . 12
⊢
((A ∈ ℂ ∧
y ∈
ℂ ∧ x ∈ ℂ)
→ ((A − y) − (A
− x)) = (x − y)) |
69 | 68 | 3com23 1109 |
. . . . . . . . . . 11
⊢
((A ∈ ℂ ∧
x ∈
ℂ ∧ y ∈ ℂ)
→ ((A − y) − (A
− x)) = (x − y)) |
70 | 69 | 3expb 1104 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧
(x ∈
ℂ ∧ y ∈ ℂ))
→ ((A − y) − (A
− x)) = (x − y)) |
71 | 70 | oveq2d 5471 |
. . . . . . . . 9
⊢
((A ∈ ℂ ∧
(x ∈
ℂ ∧ y ∈ ℂ))
→ (i · ((A − y) − (A
− x))) = (i · (x − y))) |
72 | 67, 71 | eqtr3d 2071 |
. . . . . . . 8
⊢
((A ∈ ℂ ∧
(x ∈
ℂ ∧ y ∈ ℂ))
→ ((i · (A − y)) − (i · (A − x))) =
(i · (x − y))) |
73 | 72 | eleq1d 2103 |
. . . . . . 7
⊢
((A ∈ ℂ ∧
(x ∈
ℂ ∧ y ∈ ℂ))
→ (((i · (A − y)) − (i · (A − x)))
∈ ℝ ↔ (i · (x − y))
∈ ℝ)) |
74 | 61, 73 | syl5ib 143 |
. . . . . 6
⊢
((A ∈ ℂ ∧
(x ∈
ℂ ∧ y ∈ ℂ))
→ (((i · (A − x)) ∈ ℝ
∧ (i · (A − y))
∈ ℝ) → (i · (x − y))
∈ ℝ)) |
75 | 59, 74 | anim12d 318 |
. . . . 5
⊢
((A ∈ ℂ ∧
(x ∈
ℂ ∧ y ∈ ℂ))
→ ((((A + x) ∈ ℝ ∧ (A + y) ∈ ℝ)
∧ ((i · (A − x))
∈ ℝ ∧
(i · (A − y)) ∈ ℝ))
→ ((x − y) ∈ ℝ ∧ (i · (x
− y)) ∈ ℝ))) |
76 | | rimul 7369 |
. . . . . 6
⊢
(((x − y) ∈ ℝ ∧ (i · (x
− y)) ∈ ℝ) → (x − y) =
0) |
77 | 76 | a1i 9 |
. . . . 5
⊢
((A ∈ ℂ ∧
(x ∈
ℂ ∧ y ∈ ℂ))
→ (((x − y) ∈ ℝ ∧ (i · (x
− y)) ∈ ℝ) → (x − y) =
0)) |
78 | | subeq0 7033 |
. . . . . . 7
⊢
((x ∈ ℂ ∧
y ∈
ℂ) → ((x − y) = 0 ↔ x
= y)) |
79 | 78 | biimpd 132 |
. . . . . 6
⊢
((x ∈ ℂ ∧
y ∈
ℂ) → ((x − y) = 0 → x
= y)) |
80 | 79 | adantl 262 |
. . . . 5
⊢
((A ∈ ℂ ∧
(x ∈
ℂ ∧ y ∈ ℂ))
→ ((x − y) = 0 → x
= y)) |
81 | 75, 77, 80 | 3syld 51 |
. . . 4
⊢
((A ∈ ℂ ∧
(x ∈
ℂ ∧ y ∈ ℂ))
→ ((((A + x) ∈ ℝ ∧ (A + y) ∈ ℝ)
∧ ((i · (A − x))
∈ ℝ ∧
(i · (A − y)) ∈ ℝ))
→ x = y)) |
82 | 54, 81 | syl5bi 141 |
. . 3
⊢
((A ∈ ℂ ∧
(x ∈
ℂ ∧ y ∈ ℂ))
→ ((((A + x) ∈ ℝ ∧ (i · (A
− x)) ∈ ℝ) ∧
((A + y) ∈ ℝ ∧ (i · (A
− y)) ∈ ℝ)) → x = y)) |
83 | 82 | ralrimivva 2395 |
. 2
⊢ (A ∈ ℂ →
∀x
∈ ℂ ∀y ∈ ℂ ((((A
+ x) ∈
ℝ ∧ (i · (A − x))
∈ ℝ) ∧
((A + y) ∈ ℝ ∧ (i · (A
− y)) ∈ ℝ)) → x = y)) |
84 | | oveq2 5463 |
. . . . 5
⊢ (x = y →
(A + x)
= (A + y)) |
85 | 84 | eleq1d 2103 |
. . . 4
⊢ (x = y →
((A + x) ∈ ℝ
↔ (A + y) ∈
ℝ)) |
86 | | oveq2 5463 |
. . . . . 6
⊢ (x = y →
(A − x) = (A −
y)) |
87 | 86 | oveq2d 5471 |
. . . . 5
⊢ (x = y → (i
· (A − x)) = (i · (A − y))) |
88 | 87 | eleq1d 2103 |
. . . 4
⊢ (x = y → ((i
· (A − x)) ∈ ℝ
↔ (i · (A − y)) ∈
ℝ)) |
89 | 85, 88 | anbi12d 442 |
. . 3
⊢ (x = y →
(((A + x) ∈ ℝ ∧ (i · (A
− x)) ∈ ℝ) ↔ ((A + y) ∈ ℝ ∧ (i
· (A − y)) ∈
ℝ))) |
90 | 89 | reu4 2729 |
. 2
⊢ (∃!x ∈ ℂ ((A +
x) ∈
ℝ ∧ (i · (A − x))
∈ ℝ) ↔ (∃x ∈ ℂ ((A +
x) ∈
ℝ ∧ (i · (A − x))
∈ ℝ) ∧
∀x
∈ ℂ ∀y ∈ ℂ ((((A
+ x) ∈
ℝ ∧ (i · (A − x))
∈ ℝ) ∧
((A + y) ∈ ℝ ∧ (i · (A
− y)) ∈ ℝ)) → x = y))) |
91 | 53, 83, 90 | sylanbrc 394 |
1
⊢ (A ∈ ℂ →
∃!x
∈ ℂ ((A + x) ∈ ℝ ∧ (i
· (A − x)) ∈
ℝ)) |