Proof of Theorem colinearalglem1
Step | Hyp | Ref
| Expression |
1 | | simpl2 1193 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → 𝐵 ∈
ℂ) |
2 | | simpl1 1192 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → 𝐴 ∈
ℂ) |
3 | 1, 2 | subcld 11075 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → (𝐵 − 𝐴) ∈ ℂ) |
4 | | simpr3 1197 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → 𝐹 ∈
ℂ) |
5 | | simpr1 1195 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → 𝐷 ∈
ℂ) |
6 | 3, 4, 5 | subdid 11174 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → ((𝐵 − 𝐴) · (𝐹 − 𝐷)) = (((𝐵 − 𝐴) · 𝐹) − ((𝐵 − 𝐴) · 𝐷))) |
7 | 1, 2, 4 | subdird 11175 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → ((𝐵 − 𝐴) · 𝐹) = ((𝐵 · 𝐹) − (𝐴 · 𝐹))) |
8 | 1, 2, 5 | subdird 11175 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → ((𝐵 − 𝐴) · 𝐷) = ((𝐵 · 𝐷) − (𝐴 · 𝐷))) |
9 | 7, 8 | oveq12d 7188 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) →
(((𝐵 − 𝐴) · 𝐹) − ((𝐵 − 𝐴) · 𝐷)) = (((𝐵 · 𝐹) − (𝐴 · 𝐹)) − ((𝐵 · 𝐷) − (𝐴 · 𝐷)))) |
10 | | simp2 1138 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → 𝐵 ∈
ℂ) |
11 | | simp3 1139 |
. . . . . . . 8
⊢ ((𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ) → 𝐹 ∈
ℂ) |
12 | | mulcl 10699 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ 𝐹 ∈ ℂ) → (𝐵 · 𝐹) ∈ ℂ) |
13 | 10, 11, 12 | syl2an 599 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → (𝐵 · 𝐹) ∈ ℂ) |
14 | | simp1 1137 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → 𝐴 ∈
ℂ) |
15 | | mulcl 10699 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐹 ∈ ℂ) → (𝐴 · 𝐹) ∈ ℂ) |
16 | 14, 11, 15 | syl2an 599 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → (𝐴 · 𝐹) ∈ ℂ) |
17 | 13, 16 | subcld 11075 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → ((𝐵 · 𝐹) − (𝐴 · 𝐹)) ∈ ℂ) |
18 | | simp1 1137 |
. . . . . . 7
⊢ ((𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ) → 𝐷 ∈
ℂ) |
19 | | mulcl 10699 |
. . . . . . 7
⊢ ((𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (𝐵 · 𝐷) ∈ ℂ) |
20 | 10, 18, 19 | syl2an 599 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → (𝐵 · 𝐷) ∈ ℂ) |
21 | | mulcl 10699 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (𝐴 · 𝐷) ∈ ℂ) |
22 | 14, 18, 21 | syl2an 599 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → (𝐴 · 𝐷) ∈ ℂ) |
23 | 17, 20, 22 | subsub3d 11105 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) →
(((𝐵 · 𝐹) − (𝐴 · 𝐹)) − ((𝐵 · 𝐷) − (𝐴 · 𝐷))) = ((((𝐵 · 𝐹) − (𝐴 · 𝐹)) + (𝐴 · 𝐷)) − (𝐵 · 𝐷))) |
24 | 17, 22, 20 | addsubd 11096 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) →
((((𝐵 · 𝐹) − (𝐴 · 𝐹)) + (𝐴 · 𝐷)) − (𝐵 · 𝐷)) = ((((𝐵 · 𝐹) − (𝐴 · 𝐹)) − (𝐵 · 𝐷)) + (𝐴 · 𝐷))) |
25 | 9, 23, 24 | 3eqtrrd 2778 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) →
((((𝐵 · 𝐹) − (𝐴 · 𝐹)) − (𝐵 · 𝐷)) + (𝐴 · 𝐷)) = (((𝐵 − 𝐴) · 𝐹) − ((𝐵 − 𝐴) · 𝐷))) |
26 | 13, 16, 20 | subsub4d 11106 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) →
(((𝐵 · 𝐹) − (𝐴 · 𝐹)) − (𝐵 · 𝐷)) = ((𝐵 · 𝐹) − ((𝐴 · 𝐹) + (𝐵 · 𝐷)))) |
27 | 26 | oveq1d 7185 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) →
((((𝐵 · 𝐹) − (𝐴 · 𝐹)) − (𝐵 · 𝐷)) + (𝐴 · 𝐷)) = (((𝐵 · 𝐹) − ((𝐴 · 𝐹) + (𝐵 · 𝐷))) + (𝐴 · 𝐷))) |
28 | 6, 25, 27 | 3eqtr2d 2779 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → ((𝐵 − 𝐴) · (𝐹 − 𝐷)) = (((𝐵 · 𝐹) − ((𝐴 · 𝐹) + (𝐵 · 𝐷))) + (𝐴 · 𝐷))) |
29 | | simpr2 1196 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → 𝐸 ∈
ℂ) |
30 | 29, 5 | subcld 11075 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → (𝐸 − 𝐷) ∈ ℂ) |
31 | | simpl3 1194 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → 𝐶 ∈
ℂ) |
32 | 31, 2 | subcld 11075 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → (𝐶 − 𝐴) ∈ ℂ) |
33 | 30, 32 | mulcomd 10740 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → ((𝐸 − 𝐷) · (𝐶 − 𝐴)) = ((𝐶 − 𝐴) · (𝐸 − 𝐷))) |
34 | 32, 29, 5 | subdid 11174 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → ((𝐶 − 𝐴) · (𝐸 − 𝐷)) = (((𝐶 − 𝐴) · 𝐸) − ((𝐶 − 𝐴) · 𝐷))) |
35 | 31, 2, 29 | subdird 11175 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → ((𝐶 − 𝐴) · 𝐸) = ((𝐶 · 𝐸) − (𝐴 · 𝐸))) |
36 | 31, 2, 5 | subdird 11175 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → ((𝐶 − 𝐴) · 𝐷) = ((𝐶 · 𝐷) − (𝐴 · 𝐷))) |
37 | 35, 36 | oveq12d 7188 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) →
(((𝐶 − 𝐴) · 𝐸) − ((𝐶 − 𝐴) · 𝐷)) = (((𝐶 · 𝐸) − (𝐴 · 𝐸)) − ((𝐶 · 𝐷) − (𝐴 · 𝐷)))) |
38 | | simp3 1139 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → 𝐶 ∈
ℂ) |
39 | | simp2 1138 |
. . . . . . . . 9
⊢ ((𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ) → 𝐸 ∈
ℂ) |
40 | | mulcl 10699 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ℂ ∧ 𝐸 ∈ ℂ) → (𝐶 · 𝐸) ∈ ℂ) |
41 | 38, 39, 40 | syl2an 599 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → (𝐶 · 𝐸) ∈ ℂ) |
42 | | mulcl 10699 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐸 ∈ ℂ) → (𝐴 · 𝐸) ∈ ℂ) |
43 | 14, 39, 42 | syl2an 599 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → (𝐴 · 𝐸) ∈ ℂ) |
44 | 41, 43 | subcld 11075 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → ((𝐶 · 𝐸) − (𝐴 · 𝐸)) ∈ ℂ) |
45 | | mulcl 10699 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (𝐶 · 𝐷) ∈ ℂ) |
46 | 38, 18, 45 | syl2an 599 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → (𝐶 · 𝐷) ∈ ℂ) |
47 | 44, 46, 22 | subsub3d 11105 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) →
(((𝐶 · 𝐸) − (𝐴 · 𝐸)) − ((𝐶 · 𝐷) − (𝐴 · 𝐷))) = ((((𝐶 · 𝐸) − (𝐴 · 𝐸)) + (𝐴 · 𝐷)) − (𝐶 · 𝐷))) |
48 | 44, 22, 46 | addsubd 11096 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) →
((((𝐶 · 𝐸) − (𝐴 · 𝐸)) + (𝐴 · 𝐷)) − (𝐶 · 𝐷)) = ((((𝐶 · 𝐸) − (𝐴 · 𝐸)) − (𝐶 · 𝐷)) + (𝐴 · 𝐷))) |
49 | 37, 47, 48 | 3eqtrrd 2778 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) →
((((𝐶 · 𝐸) − (𝐴 · 𝐸)) − (𝐶 · 𝐷)) + (𝐴 · 𝐷)) = (((𝐶 − 𝐴) · 𝐸) − ((𝐶 − 𝐴) · 𝐷))) |
50 | 41, 43, 46 | subsub4d 11106 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) →
(((𝐶 · 𝐸) − (𝐴 · 𝐸)) − (𝐶 · 𝐷)) = ((𝐶 · 𝐸) − ((𝐴 · 𝐸) + (𝐶 · 𝐷)))) |
51 | 50 | oveq1d 7185 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) →
((((𝐶 · 𝐸) − (𝐴 · 𝐸)) − (𝐶 · 𝐷)) + (𝐴 · 𝐷)) = (((𝐶 · 𝐸) − ((𝐴 · 𝐸) + (𝐶 · 𝐷))) + (𝐴 · 𝐷))) |
52 | 49, 51 | eqtr3d 2775 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) →
(((𝐶 − 𝐴) · 𝐸) − ((𝐶 − 𝐴) · 𝐷)) = (((𝐶 · 𝐸) − ((𝐴 · 𝐸) + (𝐶 · 𝐷))) + (𝐴 · 𝐷))) |
53 | 33, 34, 52 | 3eqtrd 2777 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → ((𝐸 − 𝐷) · (𝐶 − 𝐴)) = (((𝐶 · 𝐸) − ((𝐴 · 𝐸) + (𝐶 · 𝐷))) + (𝐴 · 𝐷))) |
54 | 28, 53 | eqeq12d 2754 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) →
(((𝐵 − 𝐴) · (𝐹 − 𝐷)) = ((𝐸 − 𝐷) · (𝐶 − 𝐴)) ↔ (((𝐵 · 𝐹) − ((𝐴 · 𝐹) + (𝐵 · 𝐷))) + (𝐴 · 𝐷)) = (((𝐶 · 𝐸) − ((𝐴 · 𝐸) + (𝐶 · 𝐷))) + (𝐴 · 𝐷)))) |
55 | 16, 20 | addcld 10738 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → ((𝐴 · 𝐹) + (𝐵 · 𝐷)) ∈ ℂ) |
56 | 13, 55 | subcld 11075 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → ((𝐵 · 𝐹) − ((𝐴 · 𝐹) + (𝐵 · 𝐷))) ∈ ℂ) |
57 | 43, 46 | addcld 10738 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → ((𝐴 · 𝐸) + (𝐶 · 𝐷)) ∈ ℂ) |
58 | 41, 57 | subcld 11075 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) → ((𝐶 · 𝐸) − ((𝐴 · 𝐸) + (𝐶 · 𝐷))) ∈ ℂ) |
59 | 56, 58, 22 | addcan2d 10922 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) →
((((𝐵 · 𝐹) − ((𝐴 · 𝐹) + (𝐵 · 𝐷))) + (𝐴 · 𝐷)) = (((𝐶 · 𝐸) − ((𝐴 · 𝐸) + (𝐶 · 𝐷))) + (𝐴 · 𝐷)) ↔ ((𝐵 · 𝐹) − ((𝐴 · 𝐹) + (𝐵 · 𝐷))) = ((𝐶 · 𝐸) − ((𝐴 · 𝐸) + (𝐶 · 𝐷))))) |
60 | 54, 59 | bitrd 282 |
1
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ)) →
(((𝐵 − 𝐴) · (𝐹 − 𝐷)) = ((𝐸 − 𝐷) · (𝐶 − 𝐴)) ↔ ((𝐵 · 𝐹) − ((𝐴 · 𝐹) + (𝐵 · 𝐷))) = ((𝐶 · 𝐸) − ((𝐴 · 𝐸) + (𝐶 · 𝐷))))) |