Step | Hyp | Ref
| Expression |
1 | | cnre 6821 |
. . 3
⊢ (𝐶 ∈ ℂ → ∃u ∈ ℝ ∃v ∈ ℝ 𝐶 = (u +
(i · v))) |
2 | 1 | 3ad2ant3 926 |
. 2
⊢
((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) → ∃u ∈ ℝ ∃v ∈ ℝ 𝐶 = (u +
(i · v))) |
3 | | cnre 6821 |
. . . . . . 7
⊢ (B ∈ ℂ →
∃z ∈ ℝ ∃w ∈ ℝ B =
(z + (i · w))) |
4 | 3 | 3ad2ant2 925 |
. . . . . 6
⊢
((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) → ∃z ∈ ℝ ∃w ∈ ℝ B =
(z + (i · w))) |
5 | 4 | ad2antrr 457 |
. . . . 5
⊢
((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) → ∃z ∈ ℝ ∃w ∈ ℝ B =
(z + (i · w))) |
6 | | cnre 6821 |
. . . . . . . . . . 11
⊢ (A ∈ ℂ →
∃x ∈ ℝ ∃y ∈ ℝ A =
(x + (i · y))) |
7 | 6 | 3ad2ant1 924 |
. . . . . . . . . 10
⊢
((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) → ∃x ∈ ℝ ∃y ∈ ℝ A =
(x + (i · y))) |
8 | 7 | adantr 261 |
. . . . . . . . 9
⊢
(((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) → ∃x ∈ ℝ ∃y ∈ ℝ A =
(x + (i · y))) |
9 | 8 | ad3antrrr 461 |
. . . . . . . 8
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) → ∃x ∈ ℝ ∃y ∈ ℝ A =
(x + (i · y))) |
10 | | simpr 103 |
. . . . . . . . . . . . . . 15
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → A = (x + (i
· y))) |
11 | | simpllr 486 |
. . . . . . . . . . . . . . 15
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → B = (z + (i
· w))) |
12 | 10, 11 | breq12d 3768 |
. . . . . . . . . . . . . 14
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → (A # B ↔
(x + (i · y)) # (z + (i
· w)))) |
13 | | simplrl 487 |
. . . . . . . . . . . . . . 15
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → x ∈
ℝ) |
14 | | simplrr 488 |
. . . . . . . . . . . . . . 15
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → y ∈
ℝ) |
15 | | simprl 483 |
. . . . . . . . . . . . . . . 16
⊢
(((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) → z ∈
ℝ) |
16 | 15 | ad3antrrr 461 |
. . . . . . . . . . . . . . 15
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → z ∈
ℝ) |
17 | | simprr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) → w ∈
ℝ) |
18 | 17 | ad3antrrr 461 |
. . . . . . . . . . . . . . 15
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → w ∈
ℝ) |
19 | | apreim 7387 |
. . . . . . . . . . . . . . 15
⊢
(((x ∈ ℝ ∧
y ∈
ℝ) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) → ((x + (i · y)) # (z + (i
· w)) ↔ (x # z ∨ y # w))) |
20 | 13, 14, 16, 18, 19 | syl22anc 1135 |
. . . . . . . . . . . . . 14
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → ((x + (i · y)) # (z + (i
· w)) ↔ (x # z ∨ y # w))) |
21 | 12, 20 | bitrd 177 |
. . . . . . . . . . . . 13
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → (A # B ↔
(x # z
∨ y #
w))) |
22 | | simprl 483 |
. . . . . . . . . . . . . . . . 17
⊢
(((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) → u ∈
ℝ) |
23 | 22 | ad2antrr 457 |
. . . . . . . . . . . . . . . 16
⊢
(((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) → u ∈
ℝ) |
24 | 23 | ad3antrrr 461 |
. . . . . . . . . . . . . . 15
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → u ∈
ℝ) |
25 | | reapcotr 7382 |
. . . . . . . . . . . . . . 15
⊢
((x ∈ ℝ ∧
z ∈
ℝ ∧ u ∈ ℝ)
→ (x # z → (x #
u ∨
z # u))) |
26 | 13, 16, 24, 25 | syl3anc 1134 |
. . . . . . . . . . . . . 14
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → (x # z →
(x # u
∨ z #
u))) |
27 | | simprr 484 |
. . . . . . . . . . . . . . . . 17
⊢
(((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) → v ∈
ℝ) |
28 | 27 | ad2antrr 457 |
. . . . . . . . . . . . . . . 16
⊢
(((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) → v ∈
ℝ) |
29 | 28 | ad3antrrr 461 |
. . . . . . . . . . . . . . 15
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → v ∈
ℝ) |
30 | | reapcotr 7382 |
. . . . . . . . . . . . . . 15
⊢
((y ∈ ℝ ∧
w ∈
ℝ ∧ v ∈ ℝ)
→ (y # w → (y #
v ∨
w # v))) |
31 | 14, 18, 29, 30 | syl3anc 1134 |
. . . . . . . . . . . . . 14
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → (y # w →
(y # v
∨ w #
v))) |
32 | 26, 31 | orim12d 699 |
. . . . . . . . . . . . 13
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → ((x # z ∨ y # w) → ((x #
u ∨
z # u)
∨ (y #
v ∨
w # v)))) |
33 | 21, 32 | sylbid 139 |
. . . . . . . . . . . 12
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → (A # B →
((x # u
∨ z #
u) ∨
(y # v
∨ w #
v)))) |
34 | | or4 687 |
. . . . . . . . . . . 12
⊢
(((x # u ∨ z # u) ∨ (y # v ∨ w # v)) ↔
((x # u
∨ y #
v) ∨
(z # u
∨ w #
v))) |
35 | 33, 34 | syl6ib 150 |
. . . . . . . . . . 11
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → (A # B →
((x # u
∨ y #
v) ∨
(z # u
∨ w #
v)))) |
36 | | simplr 482 |
. . . . . . . . . . . . . . 15
⊢
(((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) → 𝐶 = (u +
(i · v))) |
37 | 36 | ad3antrrr 461 |
. . . . . . . . . . . . . 14
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → 𝐶 = (u +
(i · v))) |
38 | 10, 37 | breq12d 3768 |
. . . . . . . . . . . . 13
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → (A # 𝐶 ↔ (x + (i · y)) # (u + (i
· v)))) |
39 | | apreim 7387 |
. . . . . . . . . . . . . 14
⊢
(((x ∈ ℝ ∧
y ∈
ℝ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) → ((x + (i · y)) # (u + (i
· v)) ↔ (x # u ∨ y # v))) |
40 | 13, 14, 24, 29, 39 | syl22anc 1135 |
. . . . . . . . . . . . 13
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → ((x + (i · y)) # (u + (i
· v)) ↔ (x # u ∨ y # v))) |
41 | 38, 40 | bitrd 177 |
. . . . . . . . . . . 12
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → (A # 𝐶 ↔ (x # u ∨ y # v))) |
42 | 11, 37 | breq12d 3768 |
. . . . . . . . . . . . 13
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → (B # 𝐶 ↔ (z + (i · w)) # (u + (i
· v)))) |
43 | | apreim 7387 |
. . . . . . . . . . . . . 14
⊢
(((z ∈ ℝ ∧
w ∈
ℝ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) → ((z + (i · w)) # (u + (i
· v)) ↔ (z # u ∨ w # v))) |
44 | 16, 18, 24, 29, 43 | syl22anc 1135 |
. . . . . . . . . . . . 13
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → ((z + (i · w)) # (u + (i
· v)) ↔ (z # u ∨ w # v))) |
45 | 42, 44 | bitrd 177 |
. . . . . . . . . . . 12
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → (B # 𝐶 ↔ (z # u ∨ w # v))) |
46 | 41, 45 | orbi12d 706 |
. . . . . . . . . . 11
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → ((A # 𝐶 ∨ B # 𝐶) ↔ ((x # u ∨ y # v) ∨ (z # u ∨ w # v)))) |
47 | 35, 46 | sylibrd 158 |
. . . . . . . . . 10
⊢
((((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) ∧ A = (x + (i
· y))) → (A # B →
(A # 𝐶 ∨ B # 𝐶))) |
48 | 47 | ex 108 |
. . . . . . . . 9
⊢
(((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) ∧ (x ∈ ℝ ∧
y ∈
ℝ)) → (A = (x + (i · y)) → (A #
B → (A # 𝐶 ∨ B # 𝐶)))) |
49 | 48 | rexlimdvva 2434 |
. . . . . . . 8
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) → (∃x ∈ ℝ ∃y ∈ ℝ A =
(x + (i · y)) → (A #
B → (A # 𝐶 ∨ B # 𝐶)))) |
50 | 9, 49 | mpd 13 |
. . . . . . 7
⊢
((((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) ∧
B = (z
+ (i · w))) → (A # B →
(A # 𝐶 ∨ B # 𝐶))) |
51 | 50 | ex 108 |
. . . . . 6
⊢
(((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) ∧ (z ∈ ℝ ∧ w ∈ ℝ)) → (B = (z + (i
· w)) → (A # B →
(A # 𝐶 ∨ B # 𝐶)))) |
52 | 51 | rexlimdvva 2434 |
. . . . 5
⊢
((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) → (∃z ∈ ℝ ∃w ∈ ℝ B =
(z + (i · w)) → (A #
B → (A # 𝐶 ∨ B # 𝐶)))) |
53 | 5, 52 | mpd 13 |
. . . 4
⊢
((((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) ∧
𝐶 = (u + (i · v))) → (A #
B → (A # 𝐶 ∨ B # 𝐶))) |
54 | 53 | ex 108 |
. . 3
⊢
(((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) ∧ (u ∈ ℝ ∧ v ∈ ℝ)) → (𝐶 = (u +
(i · v)) → (A # B →
(A # 𝐶 ∨ B # 𝐶)))) |
55 | 54 | rexlimdvva 2434 |
. 2
⊢
((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) → (∃u ∈ ℝ ∃v ∈ ℝ 𝐶 = (u +
(i · v)) → (A # B →
(A # 𝐶 ∨ B # 𝐶)))) |
56 | 2, 55 | mpd 13 |
1
⊢
((A ∈ ℂ ∧
B ∈
ℂ ∧ 𝐶 ∈
ℂ) → (A # B → (A #
𝐶
∨ B # 𝐶))) |