Step | Hyp | Ref
| Expression |
1 | | simpll 481 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → A ∈ ℝ) |
2 | 1 | recnd 6851 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → A ∈ ℂ) |
3 | | ax-icn 6778 |
. . . . . . 7
⊢ i ∈ ℂ |
4 | 3 | a1i 9 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → i ∈
ℂ) |
5 | | simplr 482 |
. . . . . . 7
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → B ∈ ℝ) |
6 | 5 | recnd 6851 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → B ∈ ℂ) |
7 | 4, 6 | mulcld 6845 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → (i · B) ∈ ℂ) |
8 | 2, 7 | addcld 6844 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → (A + (i · B)) ∈
ℂ) |
9 | | simprl 483 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → 𝐶 ∈ ℝ) |
10 | 9 | recnd 6851 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → 𝐶 ∈ ℂ) |
11 | | simprr 484 |
. . . . . . 7
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → 𝐷 ∈ ℝ) |
12 | 11 | recnd 6851 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → 𝐷 ∈ ℂ) |
13 | 4, 12 | mulcld 6845 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → (i · 𝐷) ∈
ℂ) |
14 | 10, 13 | addcld 6844 |
. . . 4
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → (𝐶 + (i
· 𝐷)) ∈ ℂ) |
15 | | eqeq1 2043 |
. . . . . . . . 9
⊢ (x = (A + (i
· B)) → (x = (𝑟 + (i · 𝑠)) ↔ (A + (i · B)) = (𝑟 + (i · 𝑠)))) |
16 | 15 | anbi1d 438 |
. . . . . . . 8
⊢ (x = (A + (i
· B)) → ((x = (𝑟 + (i · 𝑠)) ∧
y = (𝑡 + (i · u))) ↔ ((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧
y = (𝑡 + (i · u))))) |
17 | 16 | anbi1d 438 |
. . . . . . 7
⊢ (x = (A + (i
· B)) → (((x = (𝑟 + (i · 𝑠)) ∧
y = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)) ↔ (((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧
y = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)))) |
18 | 17 | 2rexbidv 2343 |
. . . . . 6
⊢ (x = (A + (i
· B)) → (∃𝑡 ∈ ℝ
∃u ∈ ℝ ((x =
(𝑟 + (i · 𝑠)) ∧ y = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)) ↔ ∃𝑡 ∈ ℝ ∃u ∈ ℝ (((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧
y = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)))) |
19 | 18 | 2rexbidv 2343 |
. . . . 5
⊢ (x = (A + (i
· B)) → (∃𝑟 ∈ ℝ
∃𝑠 ∈ ℝ
∃𝑡 ∈ ℝ
∃u ∈ ℝ ((x =
(𝑟 + (i · 𝑠)) ∧ y = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)) ↔ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃u ∈ ℝ (((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧
y = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)))) |
20 | | eqeq1 2043 |
. . . . . . . . 9
⊢ (y = (𝐶 + (i · 𝐷)) → (y = (𝑡 + (i · u)) ↔ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u)))) |
21 | 20 | anbi2d 437 |
. . . . . . . 8
⊢ (y = (𝐶 + (i · 𝐷)) → (((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧
y = (𝑡 + (i · u))) ↔ ((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))))) |
22 | 21 | anbi1d 438 |
. . . . . . 7
⊢ (y = (𝐶 + (i · 𝐷)) → ((((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧
y = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)) ↔ (((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)))) |
23 | 22 | 2rexbidv 2343 |
. . . . . 6
⊢ (y = (𝐶 + (i · 𝐷)) → (∃𝑡 ∈ ℝ
∃u ∈ ℝ (((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧
y = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)) ↔ ∃𝑡 ∈ ℝ ∃u ∈ ℝ (((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)))) |
24 | 23 | 2rexbidv 2343 |
. . . . 5
⊢ (y = (𝐶 + (i · 𝐷)) → (∃𝑟 ∈ ℝ
∃𝑠 ∈ ℝ
∃𝑡 ∈ ℝ
∃u ∈ ℝ (((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧
y = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)) ↔ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃u ∈ ℝ (((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)))) |
25 | | df-ap 7366 |
. . . . 5
⊢ # =
{〈x, y〉 ∣ ∃𝑟 ∈ ℝ
∃𝑠 ∈ ℝ
∃𝑡 ∈ ℝ
∃u ∈ ℝ ((x =
(𝑟 + (i · 𝑠)) ∧ y = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))} |
26 | 19, 24, 25 | brabg 3997 |
. . . 4
⊢
(((A + (i · B)) ∈ ℂ
∧ (𝐶 + (i · 𝐷)) ∈
ℂ) → ((A + (i · B)) # (𝐶 + (i · 𝐷)) ↔ ∃𝑟 ∈ ℝ
∃𝑠 ∈ ℝ
∃𝑡 ∈ ℝ
∃u ∈ ℝ (((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)))) |
27 | 8, 14, 26 | syl2anc 391 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → ((A + (i · B)) # (𝐶 + (i · 𝐷)) ↔ ∃𝑟 ∈ ℝ
∃𝑠 ∈ ℝ
∃𝑡 ∈ ℝ
∃u ∈ ℝ (((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)))) |
28 | | simprr 484 |
. . . . . . 7
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → (𝑟 #ℝ 𝑡 ∨ 𝑠 #ℝ u)) |
29 | 1 | ad3antrrr 461 |
. . . . . . . . . 10
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → A
∈ ℝ) |
30 | 9 | ad3antrrr 461 |
. . . . . . . . . 10
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → 𝐶 ∈
ℝ) |
31 | | apreap 7371 |
. . . . . . . . . 10
⊢
((A ∈ ℝ ∧ 𝐶 ∈ ℝ) → (A # 𝐶 ↔ A #ℝ 𝐶)) |
32 | 29, 30, 31 | syl2anc 391 |
. . . . . . . . 9
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → (A #
𝐶 ↔ A #ℝ 𝐶)) |
33 | 5 | ad3antrrr 461 |
. . . . . . . . . 10
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → B
∈ ℝ) |
34 | 11 | ad3antrrr 461 |
. . . . . . . . . 10
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → 𝐷 ∈
ℝ) |
35 | | apreap 7371 |
. . . . . . . . . 10
⊢
((B ∈ ℝ ∧ 𝐷 ∈ ℝ) → (B # 𝐷 ↔ B #ℝ 𝐷)) |
36 | 33, 34, 35 | syl2anc 391 |
. . . . . . . . 9
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → (B #
𝐷 ↔ B #ℝ 𝐷)) |
37 | 32, 36 | orbi12d 706 |
. . . . . . . 8
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → ((A
# 𝐶
∨ B # 𝐷) ↔ (A #ℝ 𝐶 ∨ B #ℝ 𝐷))) |
38 | | simprll 489 |
. . . . . . . . . . . 12
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → (A +
(i · B)) = (𝑟 + (i · 𝑠))) |
39 | | simpllr 486 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) |
40 | | cru 7386 |
. . . . . . . . . . . . 13
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) → ((A + (i · B)) = (𝑟 + (i · 𝑠)) ↔ (A = 𝑟 ∧ B = 𝑠))) |
41 | 29, 33, 39, 40 | syl21anc 1133 |
. . . . . . . . . . . 12
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → ((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ↔ (A = 𝑟 ∧ B = 𝑠))) |
42 | 38, 41 | mpbid 135 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → (A =
𝑟 ∧ B = 𝑠)) |
43 | 42 | simpld 105 |
. . . . . . . . . 10
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → A =
𝑟) |
44 | | simprlr 490 |
. . . . . . . . . . . 12
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) |
45 | | simplr 482 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → (𝑡 ∈ ℝ
∧ u ∈ ℝ)) |
46 | | cru 7386 |
. . . . . . . . . . . . 13
⊢ (((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧
(𝑡 ∈ ℝ ∧
u ∈
ℝ)) → ((𝐶 + (i
· 𝐷)) = (𝑡 + (i · u)) ↔ (𝐶 = 𝑡 ∧ 𝐷 = u))) |
47 | 30, 34, 45, 46 | syl21anc 1133 |
. . . . . . . . . . . 12
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → ((𝐶 + (i · 𝐷)) = (𝑡 + (i · u)) ↔ (𝐶 = 𝑡 ∧ 𝐷 = u))) |
48 | 44, 47 | mpbid 135 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → (𝐶 = 𝑡 ∧ 𝐷 = u)) |
49 | 48 | simpld 105 |
. . . . . . . . . 10
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → 𝐶 = 𝑡) |
50 | 43, 49 | breq12d 3768 |
. . . . . . . . 9
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → (A
#ℝ 𝐶
↔ 𝑟 #ℝ
𝑡)) |
51 | 42 | simprd 107 |
. . . . . . . . . 10
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → B =
𝑠) |
52 | 48 | simprd 107 |
. . . . . . . . . 10
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → 𝐷 = u) |
53 | 51, 52 | breq12d 3768 |
. . . . . . . . 9
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → (B
#ℝ 𝐷
↔ 𝑠 #ℝ
u)) |
54 | 50, 53 | orbi12d 706 |
. . . . . . . 8
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → ((A
#ℝ 𝐶 ∨ B
#ℝ 𝐷)
↔ (𝑟 #ℝ
𝑡
∨ 𝑠
#ℝ u))) |
55 | 37, 54 | bitrd 177 |
. . . . . . 7
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → ((A
# 𝐶
∨ B # 𝐷) ↔ (𝑟 #ℝ 𝑡 ∨ 𝑠 #ℝ u))) |
56 | 28, 55 | mpbird 156 |
. . . . . 6
⊢
((((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) ∧
(((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) → (A #
𝐶
∨ B # 𝐷)) |
57 | 56 | ex 108 |
. . . . 5
⊢
(((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) ∧ (𝑡 ∈ ℝ
∧ u ∈ ℝ)) → ((((A + (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)) → (A #
𝐶
∨ B # 𝐷))) |
58 | 57 | rexlimdvva 2434 |
. . . 4
⊢
((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (𝑟 ∈ ℝ
∧ 𝑠 ∈
ℝ)) → (∃𝑡 ∈ ℝ
∃u ∈ ℝ (((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)) → (A #
𝐶
∨ B # 𝐷))) |
59 | 58 | rexlimdvva 2434 |
. . 3
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → (∃𝑟 ∈ ℝ
∃𝑠 ∈ ℝ
∃𝑡 ∈ ℝ
∃u ∈ ℝ (((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)) → (A #
𝐶
∨ B # 𝐷))) |
60 | 27, 59 | sylbid 139 |
. 2
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → ((A + (i · B)) # (𝐶 + (i · 𝐷)) → (A # 𝐶 ∨ B # 𝐷))) |
61 | 31 | ad2ant2r 478 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → (A # 𝐶 ↔ A #ℝ 𝐶)) |
62 | 35 | ad2ant2l 477 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → (B # 𝐷 ↔ B #ℝ 𝐷)) |
63 | 61, 62 | orbi12d 706 |
. . . . 5
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → ((A # 𝐶 ∨ B # 𝐷) ↔ (A #ℝ 𝐶 ∨ B #ℝ 𝐷))) |
64 | 63 | pm5.32i 427 |
. . . 4
⊢
((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (A # 𝐶 ∨ B # 𝐷)) ↔ (((A ∈ ℝ ∧ B ∈ ℝ) ∧
(𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) ∧
(A #ℝ 𝐶 ∨ B #ℝ 𝐷))) |
65 | | eqid 2037 |
. . . . . . . . . . . 12
⊢ (A + (i · B)) = (A + (i
· B)) |
66 | | eqid 2037 |
. . . . . . . . . . . 12
⊢ (𝐶 + (i · 𝐷)) = (𝐶 + (i · 𝐷)) |
67 | 65, 66 | pm3.2i 257 |
. . . . . . . . . . 11
⊢
((A + (i · B)) = (A + (i
· B)) ∧ (𝐶 + (i · 𝐷)) = (𝐶 + (i · 𝐷))) |
68 | 67 | biantrur 287 |
. . . . . . . . . 10
⊢
((A #ℝ 𝐶
∨ B #ℝ 𝐷) ↔ (((A + (i · B)) = (A + (i
· B)) ∧ (𝐶 + (i · 𝐷)) = (𝐶 + (i · 𝐷))) ∧
(A #ℝ 𝐶 ∨ B #ℝ 𝐷))) |
69 | | oveq1 5462 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝐶 → (𝑡 + (i · u)) = (𝐶 + (i · u))) |
70 | 69 | eqeq2d 2048 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝐶 → ((𝐶 + (i · 𝐷)) = (𝑡 + (i · u)) ↔ (𝐶 + (i · 𝐷)) = (𝐶 + (i · u)))) |
71 | 70 | anbi2d 437 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝐶 → (((A + (i · B)) = (A + (i
· B)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ↔ ((A
+ (i · B)) = (A + (i · B)) ∧ (𝐶 + (i · 𝐷)) = (𝐶 + (i · u))))) |
72 | | breq2 3759 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝐶 → (A #ℝ 𝑡 ↔ A
#ℝ 𝐶)) |
73 | 72 | orbi1d 704 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝐶 → ((A #ℝ 𝑡 ∨ B #ℝ u) ↔ (A
#ℝ 𝐶 ∨ B
#ℝ u))) |
74 | 71, 73 | anbi12d 442 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝐶 → ((((A + (i · B)) = (A + (i
· B)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (A #ℝ 𝑡 ∨ B #ℝ u)) ↔ (((A
+ (i · B)) = (A + (i · B)) ∧ (𝐶 + (i · 𝐷)) = (𝐶 + (i · u))) ∧ (A #ℝ 𝐶 ∨ B #ℝ u)))) |
75 | | oveq2 5463 |
. . . . . . . . . . . . . . 15
⊢ (u = 𝐷 → (i · u) = (i · 𝐷)) |
76 | 75 | oveq2d 5471 |
. . . . . . . . . . . . . 14
⊢ (u = 𝐷 → (𝐶 + (i · u)) = (𝐶 + (i · 𝐷))) |
77 | 76 | eqeq2d 2048 |
. . . . . . . . . . . . 13
⊢ (u = 𝐷 → ((𝐶 + (i · 𝐷)) = (𝐶 + (i · u)) ↔ (𝐶 + (i · 𝐷)) = (𝐶 + (i · 𝐷)))) |
78 | 77 | anbi2d 437 |
. . . . . . . . . . . 12
⊢ (u = 𝐷 → (((A + (i · B)) = (A + (i
· B)) ∧ (𝐶 + (i · 𝐷)) = (𝐶 + (i · u))) ↔ ((A
+ (i · B)) = (A + (i · B)) ∧ (𝐶 + (i · 𝐷)) = (𝐶 + (i · 𝐷))))) |
79 | | breq2 3759 |
. . . . . . . . . . . . 13
⊢ (u = 𝐷 → (B #ℝ u ↔ B
#ℝ 𝐷)) |
80 | 79 | orbi2d 703 |
. . . . . . . . . . . 12
⊢ (u = 𝐷 → ((A #ℝ 𝐶 ∨ B #ℝ u) ↔ (A
#ℝ 𝐶 ∨ B
#ℝ 𝐷))) |
81 | 78, 80 | anbi12d 442 |
. . . . . . . . . . 11
⊢ (u = 𝐷 → ((((A + (i · B)) = (A + (i
· B)) ∧ (𝐶 + (i · 𝐷)) = (𝐶 + (i · u))) ∧ (A #ℝ 𝐶 ∨ B #ℝ u)) ↔ (((A
+ (i · B)) = (A + (i · B)) ∧ (𝐶 + (i · 𝐷)) = (𝐶 + (i · 𝐷))) ∧
(A #ℝ 𝐶 ∨ B #ℝ 𝐷)))) |
82 | 74, 81 | rspc2ev 2658 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ∧
(((A + (i · B)) = (A + (i
· B)) ∧ (𝐶 + (i · 𝐷)) = (𝐶 + (i · 𝐷))) ∧
(A #ℝ 𝐶 ∨ B #ℝ 𝐷))) → ∃𝑡 ∈ ℝ
∃u ∈ ℝ (((A
+ (i · B)) = (A + (i · B)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (A #ℝ 𝑡 ∨ B #ℝ u))) |
83 | 68, 82 | syl3an3b 1172 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ∧
(A #ℝ 𝐶 ∨ B #ℝ 𝐷)) → ∃𝑡 ∈ ℝ
∃u ∈ ℝ (((A
+ (i · B)) = (A + (i · B)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (A #ℝ 𝑡 ∨ B #ℝ u))) |
84 | 83 | 3expa 1103 |
. . . . . . . 8
⊢ (((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧
(A #ℝ 𝐶 ∨ B #ℝ 𝐷)) → ∃𝑡 ∈ ℝ
∃u ∈ ℝ (((A
+ (i · B)) = (A + (i · B)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (A #ℝ 𝑡 ∨ B #ℝ u))) |
85 | | oveq1 5462 |
. . . . . . . . . . . . 13
⊢ (𝑟 = A → (𝑟 + (i · 𝑠)) = (A +
(i · 𝑠))) |
86 | 85 | eqeq2d 2048 |
. . . . . . . . . . . 12
⊢ (𝑟 = A → ((A +
(i · B)) = (𝑟 + (i · 𝑠)) ↔ (A + (i · B)) = (A + (i
· 𝑠)))) |
87 | 86 | anbi1d 438 |
. . . . . . . . . . 11
⊢ (𝑟 = A → (((A +
(i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ↔ ((A
+ (i · B)) = (A + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))))) |
88 | | breq1 3758 |
. . . . . . . . . . . 12
⊢ (𝑟 = A → (𝑟 #ℝ 𝑡 ↔ A
#ℝ 𝑡)) |
89 | 88 | orbi1d 704 |
. . . . . . . . . . 11
⊢ (𝑟 = A → ((𝑟 #ℝ 𝑡 ∨ 𝑠 #ℝ u) ↔ (A
#ℝ 𝑡 ∨ 𝑠
#ℝ u))) |
90 | 87, 89 | anbi12d 442 |
. . . . . . . . . 10
⊢ (𝑟 = A → ((((A +
(i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)) ↔ (((A
+ (i · B)) = (A + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (A #ℝ 𝑡 ∨ 𝑠 #ℝ u)))) |
91 | 90 | 2rexbidv 2343 |
. . . . . . . . 9
⊢ (𝑟 = A → (∃𝑡 ∈ ℝ ∃u ∈ ℝ (((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)) ↔ ∃𝑡 ∈ ℝ ∃u ∈ ℝ (((A
+ (i · B)) = (A + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (A #ℝ 𝑡 ∨ 𝑠 #ℝ u)))) |
92 | | oveq2 5463 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = B → (i · 𝑠) = (i · B)) |
93 | 92 | oveq2d 5471 |
. . . . . . . . . . . . 13
⊢ (𝑠 = B → (A + (i
· 𝑠)) = (A + (i · B))) |
94 | 93 | eqeq2d 2048 |
. . . . . . . . . . . 12
⊢ (𝑠 = B → ((A +
(i · B)) = (A + (i · 𝑠)) ↔ (A + (i · B)) = (A + (i
· B)))) |
95 | 94 | anbi1d 438 |
. . . . . . . . . . 11
⊢ (𝑠 = B → (((A +
(i · B)) = (A + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ↔ ((A
+ (i · B)) = (A + (i · B)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))))) |
96 | | breq1 3758 |
. . . . . . . . . . . 12
⊢ (𝑠 = B → (𝑠 #ℝ u ↔ B
#ℝ u)) |
97 | 96 | orbi2d 703 |
. . . . . . . . . . 11
⊢ (𝑠 = B → ((A
#ℝ 𝑡 ∨ 𝑠
#ℝ u) ↔ (A #ℝ 𝑡 ∨ B #ℝ u))) |
98 | 95, 97 | anbi12d 442 |
. . . . . . . . . 10
⊢ (𝑠 = B → ((((A +
(i · B)) = (A + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (A #ℝ 𝑡 ∨ 𝑠 #ℝ u)) ↔ (((A
+ (i · B)) = (A + (i · B)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (A #ℝ 𝑡 ∨ B #ℝ u)))) |
99 | 98 | 2rexbidv 2343 |
. . . . . . . . 9
⊢ (𝑠 = B → (∃𝑡 ∈ ℝ ∃u ∈ ℝ (((A
+ (i · B)) = (A + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (A #ℝ 𝑡 ∨ 𝑠 #ℝ u)) ↔ ∃𝑡 ∈ ℝ ∃u ∈ ℝ (((A
+ (i · B)) = (A + (i · B)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (A #ℝ 𝑡 ∨ B #ℝ u)))) |
100 | 91, 99 | rspc2ev 2658 |
. . . . . . . 8
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ ∃𝑡 ∈ ℝ
∃u ∈ ℝ (((A
+ (i · B)) = (A + (i · B)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (A #ℝ 𝑡 ∨ B #ℝ u))) → ∃𝑟 ∈ ℝ
∃𝑠 ∈ ℝ
∃𝑡 ∈ ℝ
∃u ∈ ℝ (((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) |
101 | 84, 100 | syl3an3 1169 |
. . . . . . 7
⊢
((A ∈ ℝ ∧
B ∈
ℝ ∧ ((𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ) ∧ (A #ℝ 𝐶 ∨ B #ℝ 𝐷))) → ∃𝑟 ∈ ℝ
∃𝑠 ∈ ℝ
∃𝑡 ∈ ℝ
∃u ∈ ℝ (((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) |
102 | 101 | 3expa 1103 |
. . . . . 6
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ ((𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ) ∧ (A #ℝ 𝐶 ∨ B #ℝ 𝐷))) → ∃𝑟 ∈ ℝ
∃𝑠 ∈ ℝ
∃𝑡 ∈ ℝ
∃u ∈ ℝ (((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) |
103 | 102 | anassrs 380 |
. . . . 5
⊢
((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (A #ℝ 𝐶 ∨ B #ℝ 𝐷)) → ∃𝑟 ∈ ℝ
∃𝑠 ∈ ℝ
∃𝑡 ∈ ℝ
∃u ∈ ℝ (((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))) |
104 | 27 | adantr 261 |
. . . . 5
⊢
((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (A #ℝ 𝐶 ∨ B #ℝ 𝐷)) → ((A + (i · B)) # (𝐶 + (i · 𝐷)) ↔ ∃𝑟 ∈ ℝ
∃𝑠 ∈ ℝ
∃𝑡 ∈ ℝ
∃u ∈ ℝ (((A
+ (i · B)) = (𝑟 + (i · 𝑠)) ∧ (𝐶 + (i · 𝐷)) = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)))) |
105 | 103, 104 | mpbird 156 |
. . . 4
⊢
((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (A #ℝ 𝐶 ∨ B #ℝ 𝐷)) → (A + (i · B)) # (𝐶 + (i · 𝐷))) |
106 | 64, 105 | sylbi 114 |
. . 3
⊢
((((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) ∧ (A # 𝐶 ∨ B # 𝐷)) → (A + (i · B)) # (𝐶 + (i · 𝐷))) |
107 | 106 | ex 108 |
. 2
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → ((A # 𝐶 ∨ B # 𝐷) → (A + (i · B)) # (𝐶 + (i · 𝐷)))) |
108 | 60, 107 | impbid 120 |
1
⊢
(((A ∈ ℝ ∧
B ∈
ℝ) ∧ (𝐶 ∈ ℝ
∧ 𝐷 ∈
ℝ)) → ((A + (i · B)) # (𝐶 + (i · 𝐷)) ↔ (A # 𝐶 ∨ B # 𝐷))) |