Step | Hyp | Ref
| Expression |
1 | | brbtwn2 26685 |
. . 3
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴 Btwn 〈𝐵, 𝐶〉 ↔ (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))) |
2 | | brbtwn2 26685 |
. . . . 5
⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝐵 Btwn 〈𝐶, 𝐴〉 ↔ (∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑗) − (𝐵‘𝑗))) = (((𝐶‘𝑗) − (𝐵‘𝑗)) · ((𝐴‘𝑖) − (𝐵‘𝑖)))))) |
3 | 2 | 3comr 1121 |
. . . 4
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐵 Btwn 〈𝐶, 𝐴〉 ↔ (∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑗) − (𝐵‘𝑗))) = (((𝐶‘𝑗) − (𝐵‘𝑗)) · ((𝐴‘𝑖) − (𝐵‘𝑖)))))) |
4 | | colinearalglem3 26688 |
. . . . . 6
⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑗) − (𝐵‘𝑗))) = (((𝐶‘𝑗) − (𝐵‘𝑗)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
5 | 4 | 3comr 1121 |
. . . . 5
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑗) − (𝐵‘𝑗))) = (((𝐶‘𝑗) − (𝐵‘𝑗)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
6 | 5 | anbi2d 630 |
. . . 4
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ((∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑗) − (𝐵‘𝑗))) = (((𝐶‘𝑗) − (𝐵‘𝑗)) · ((𝐴‘𝑖) − (𝐵‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))) |
7 | 3, 6 | bitrd 281 |
. . 3
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐵 Btwn 〈𝐶, 𝐴〉 ↔ (∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))) |
8 | | brbtwn2 26685 |
. . . . 5
⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝐶 Btwn 〈𝐴, 𝐵〉 ↔ (∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑗) − (𝐶‘𝑗))) = (((𝐴‘𝑗) − (𝐶‘𝑗)) · ((𝐵‘𝑖) − (𝐶‘𝑖)))))) |
9 | | colinearalglem2 26687 |
. . . . . 6
⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑗) − (𝐶‘𝑗))) = (((𝐴‘𝑗) − (𝐶‘𝑗)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
10 | 9 | anbi2d 630 |
. . . . 5
⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ((∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑗) − (𝐶‘𝑗))) = (((𝐴‘𝑗) − (𝐶‘𝑗)) · ((𝐵‘𝑖) − (𝐶‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))) |
11 | 8, 10 | bitrd 281 |
. . . 4
⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝐶 Btwn 〈𝐴, 𝐵〉 ↔ (∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))) |
12 | 11 | 3coml 1123 |
. . 3
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶 Btwn 〈𝐴, 𝐵〉 ↔ (∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))) |
13 | 1, 7, 12 | 3orbi123d 1431 |
. 2
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ((𝐴 Btwn 〈𝐵, 𝐶〉 ∨ 𝐵 Btwn 〈𝐶, 𝐴〉 ∨ 𝐶 Btwn 〈𝐴, 𝐵〉) ↔ ((∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))))) |
14 | | fveecn 26682 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℂ) |
15 | | fveecn 26682 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℂ) |
16 | | subid 10899 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶‘𝑖) ∈ ℂ → ((𝐶‘𝑖) − (𝐶‘𝑖)) = 0) |
17 | 16 | oveq2d 7166 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶‘𝑖) ∈ ℂ → (((𝐵‘𝑖) − (𝐶‘𝑖)) · ((𝐶‘𝑖) − (𝐶‘𝑖))) = (((𝐵‘𝑖) − (𝐶‘𝑖)) · 0)) |
18 | 17 | adantl 484 |
. . . . . . . . . . . . . 14
⊢ (((𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) → (((𝐵‘𝑖) − (𝐶‘𝑖)) · ((𝐶‘𝑖) − (𝐶‘𝑖))) = (((𝐵‘𝑖) − (𝐶‘𝑖)) · 0)) |
19 | | subcl 10879 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) → ((𝐵‘𝑖) − (𝐶‘𝑖)) ∈ ℂ) |
20 | 19 | mul01d 10833 |
. . . . . . . . . . . . . 14
⊢ (((𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) → (((𝐵‘𝑖) − (𝐶‘𝑖)) · 0) = 0) |
21 | 18, 20 | eqtrd 2856 |
. . . . . . . . . . . . 13
⊢ (((𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) → (((𝐵‘𝑖) − (𝐶‘𝑖)) · ((𝐶‘𝑖) − (𝐶‘𝑖))) = 0) |
22 | 14, 15, 21 | syl2an 597 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁))) → (((𝐵‘𝑖) − (𝐶‘𝑖)) · ((𝐶‘𝑖) − (𝐶‘𝑖))) = 0) |
23 | 22 | anandirs 677 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵‘𝑖) − (𝐶‘𝑖)) · ((𝐶‘𝑖) − (𝐶‘𝑖))) = 0) |
24 | | 0le0 11732 |
. . . . . . . . . . 11
⊢ 0 ≤
0 |
25 | 23, 24 | eqbrtrdi 5097 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵‘𝑖) − (𝐶‘𝑖)) · ((𝐶‘𝑖) − (𝐶‘𝑖))) ≤ 0) |
26 | 25 | ralrimiva 3182 |
. . . . . . . . 9
⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐶‘𝑖)) · ((𝐶‘𝑖) − (𝐶‘𝑖))) ≤ 0) |
27 | 26 | 3adant1 1126 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐶‘𝑖)) · ((𝐶‘𝑖) − (𝐶‘𝑖))) ≤ 0) |
28 | | fveq1 6663 |
. . . . . . . . . . . 12
⊢ (𝐶 = 𝐴 → (𝐶‘𝑖) = (𝐴‘𝑖)) |
29 | 28 | oveq2d 7166 |
. . . . . . . . . . 11
⊢ (𝐶 = 𝐴 → ((𝐵‘𝑖) − (𝐶‘𝑖)) = ((𝐵‘𝑖) − (𝐴‘𝑖))) |
30 | 28 | oveq2d 7166 |
. . . . . . . . . . 11
⊢ (𝐶 = 𝐴 → ((𝐶‘𝑖) − (𝐶‘𝑖)) = ((𝐶‘𝑖) − (𝐴‘𝑖))) |
31 | 29, 30 | oveq12d 7168 |
. . . . . . . . . 10
⊢ (𝐶 = 𝐴 → (((𝐵‘𝑖) − (𝐶‘𝑖)) · ((𝐶‘𝑖) − (𝐶‘𝑖))) = (((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) |
32 | 31 | breq1d 5068 |
. . . . . . . . 9
⊢ (𝐶 = 𝐴 → ((((𝐵‘𝑖) − (𝐶‘𝑖)) · ((𝐶‘𝑖) − (𝐶‘𝑖))) ≤ 0 ↔ (((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0)) |
33 | 32 | ralbidv 3197 |
. . . . . . . 8
⊢ (𝐶 = 𝐴 → (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐶‘𝑖)) · ((𝐶‘𝑖) − (𝐶‘𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0)) |
34 | 27, 33 | syl5ibcom 247 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶 = 𝐴 → ∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0)) |
35 | | 3mix1 1326 |
. . . . . . 7
⊢
(∀𝑖 ∈
(1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 → (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0)) |
36 | 34, 35 | syl6 35 |
. . . . . 6
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶 = 𝐴 → (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0))) |
37 | 36 | a1dd 50 |
. . . . 5
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶 = 𝐴 → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0)))) |
38 | | simp3 1134 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁)) |
39 | | simp1 1132 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁)) |
40 | | eqeefv 26683 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝐶 = 𝐴 ↔ ∀𝑝 ∈ (1...𝑁)(𝐶‘𝑝) = (𝐴‘𝑝))) |
41 | 38, 39, 40 | syl2anc 586 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶 = 𝐴 ↔ ∀𝑝 ∈ (1...𝑁)(𝐶‘𝑝) = (𝐴‘𝑝))) |
42 | 41 | necon3abid 3052 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶 ≠ 𝐴 ↔ ¬ ∀𝑝 ∈ (1...𝑁)(𝐶‘𝑝) = (𝐴‘𝑝))) |
43 | | df-ne 3017 |
. . . . . . . . 9
⊢ ((𝐶‘𝑝) ≠ (𝐴‘𝑝) ↔ ¬ (𝐶‘𝑝) = (𝐴‘𝑝)) |
44 | 43 | rexbii 3247 |
. . . . . . . 8
⊢
(∃𝑝 ∈
(1...𝑁)(𝐶‘𝑝) ≠ (𝐴‘𝑝) ↔ ∃𝑝 ∈ (1...𝑁) ¬ (𝐶‘𝑝) = (𝐴‘𝑝)) |
45 | | rexnal 3238 |
. . . . . . . 8
⊢
(∃𝑝 ∈
(1...𝑁) ¬ (𝐶‘𝑝) = (𝐴‘𝑝) ↔ ¬ ∀𝑝 ∈ (1...𝑁)(𝐶‘𝑝) = (𝐴‘𝑝)) |
46 | 44, 45 | bitr2i 278 |
. . . . . . 7
⊢ (¬
∀𝑝 ∈ (1...𝑁)(𝐶‘𝑝) = (𝐴‘𝑝) ↔ ∃𝑝 ∈ (1...𝑁)(𝐶‘𝑝) ≠ (𝐴‘𝑝)) |
47 | 42, 46 | syl6bb 289 |
. . . . . 6
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶 ≠ 𝐴 ↔ ∃𝑝 ∈ (1...𝑁)(𝐶‘𝑝) ≠ (𝐴‘𝑝))) |
48 | | ralcom 3354 |
. . . . . . . 8
⊢
(∀𝑖 ∈
(1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ ∀𝑗 ∈ (1...𝑁)∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) |
49 | | fveq2 6664 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑝 → (𝐶‘𝑗) = (𝐶‘𝑝)) |
50 | | fveq2 6664 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑝 → (𝐴‘𝑗) = (𝐴‘𝑝)) |
51 | 49, 50 | oveq12d 7168 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑝 → ((𝐶‘𝑗) − (𝐴‘𝑗)) = ((𝐶‘𝑝) − (𝐴‘𝑝))) |
52 | 51 | oveq2d 7166 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑝 → (((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑝) − (𝐴‘𝑝)))) |
53 | | fveq2 6664 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑝 → (𝐵‘𝑗) = (𝐵‘𝑝)) |
54 | 53, 50 | oveq12d 7168 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑝 → ((𝐵‘𝑗) − (𝐴‘𝑗)) = ((𝐵‘𝑝) − (𝐴‘𝑝))) |
55 | 54 | oveq1d 7165 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑝 → (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) = (((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) |
56 | 52, 55 | eqeq12d 2837 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑝 → ((((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ (((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑝) − (𝐴‘𝑝))) = (((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
57 | 56 | ralbidv 3197 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑝 → (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑝) − (𝐴‘𝑝))) = (((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
58 | 57 | rspcv 3617 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (1...𝑁) → (∀𝑗 ∈ (1...𝑁)∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) → ∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑝) − (𝐴‘𝑝))) = (((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
59 | 58 | ad2antrl 726 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (1...𝑁) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝))) → (∀𝑗 ∈ (1...𝑁)∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) → ∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑝) − (𝐴‘𝑝))) = (((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
60 | | fveere 26681 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (1...𝑁)) → (𝐴‘𝑝) ∈ ℝ) |
61 | 60 | 3ad2antl1 1181 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) → (𝐴‘𝑝) ∈ ℝ) |
62 | | fveere 26681 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (1...𝑁)) → (𝐵‘𝑝) ∈ ℝ) |
63 | 62 | 3ad2antl2 1182 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) → (𝐵‘𝑝) ∈ ℝ) |
64 | | fveere 26681 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (1...𝑁)) → (𝐶‘𝑝) ∈ ℝ) |
65 | 64 | 3ad2antl3 1183 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) → (𝐶‘𝑝) ∈ ℝ) |
66 | 61, 63, 65 | 3jca 1124 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) → ((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ)) |
67 | 66 | anim1i 616 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → (((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝))) |
68 | 67 | anasss 469 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (1...𝑁) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝))) → (((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝))) |
69 | | fveecn 26682 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ) |
70 | 69 | 3ad2antl1 1181 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ) |
71 | 14 | 3ad2antl2 1182 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℂ) |
72 | 15 | 3ad2antl3 1183 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℂ) |
73 | 70, 71, 72 | 3jca 1124 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ)) |
74 | 73 | adantlr 713 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ)) |
75 | | recn 10621 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴‘𝑝) ∈ ℝ → (𝐴‘𝑝) ∈ ℂ) |
76 | | recn 10621 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵‘𝑝) ∈ ℝ → (𝐵‘𝑝) ∈ ℂ) |
77 | | recn 10621 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶‘𝑝) ∈ ℝ → (𝐶‘𝑝) ∈ ℂ) |
78 | 75, 76, 77 | 3anim123i 1147 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) → ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ)) |
79 | 78 | adantr 483 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ)) |
80 | 79 | ad2antlr 725 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ)) |
81 | | simplrr 776 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑝) ≠ (𝐴‘𝑝)) |
82 | | eqcom 2828 |
. . . . . . . . . . . . . 14
⊢ ((𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) ↔ (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) = (𝐵‘𝑖)) |
83 | | simp12 1200 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → (𝐵‘𝑖) ∈ ℂ) |
84 | | simp11 1199 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → (𝐴‘𝑖) ∈ ℂ) |
85 | | simp22 1203 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → (𝐵‘𝑝) ∈ ℂ) |
86 | | simp21 1202 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → (𝐴‘𝑝) ∈ ℂ) |
87 | 85, 86 | subcld 10991 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → ((𝐵‘𝑝) − (𝐴‘𝑝)) ∈ ℂ) |
88 | | simp23 1204 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → (𝐶‘𝑝) ∈ ℂ) |
89 | 88, 86 | subcld 10991 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → ((𝐶‘𝑝) − (𝐴‘𝑝)) ∈ ℂ) |
90 | | simpr3 1192 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ)) → (𝐶‘𝑝) ∈ ℂ) |
91 | | simpr1 1190 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ)) → (𝐴‘𝑝) ∈ ℂ) |
92 | 90, 91 | subeq0ad 11001 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ)) → (((𝐶‘𝑝) − (𝐴‘𝑝)) = 0 ↔ (𝐶‘𝑝) = (𝐴‘𝑝))) |
93 | 92 | necon3bid 3060 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ)) → (((𝐶‘𝑝) − (𝐴‘𝑝)) ≠ 0 ↔ (𝐶‘𝑝) ≠ (𝐴‘𝑝))) |
94 | 93 | biimp3ar 1466 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → ((𝐶‘𝑝) − (𝐴‘𝑝)) ≠ 0) |
95 | 87, 89, 94 | divcld 11410 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → (((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) ∈ ℂ) |
96 | | simp13 1201 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → (𝐶‘𝑖) ∈ ℂ) |
97 | 96, 84 | subcld 10991 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → ((𝐶‘𝑖) − (𝐴‘𝑖)) ∈ ℂ) |
98 | 95, 97 | mulcld 10655 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → ((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ∈ ℂ) |
99 | | subadd2 10884 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵‘𝑖) ∈ ℂ ∧ (𝐴‘𝑖) ∈ ℂ ∧ ((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ∈ ℂ) → (((𝐵‘𝑖) − (𝐴‘𝑖)) = ((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) = (𝐵‘𝑖))) |
100 | 99 | bicomd 225 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵‘𝑖) ∈ ℂ ∧ (𝐴‘𝑖) ∈ ℂ ∧ ((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ∈ ℂ) → ((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) = (𝐵‘𝑖) ↔ ((𝐵‘𝑖) − (𝐴‘𝑖)) = ((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
101 | 83, 84, 98, 100 | syl3anc 1367 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → ((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) = (𝐵‘𝑖) ↔ ((𝐵‘𝑖) − (𝐴‘𝑖)) = ((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
102 | 87, 97, 89, 94 | div23d 11447 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → ((((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) / ((𝐶‘𝑝) − (𝐴‘𝑝))) = ((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) |
103 | 102 | eqeq2d 2832 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → (((𝐵‘𝑖) − (𝐴‘𝑖)) = ((((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) / ((𝐶‘𝑝) − (𝐴‘𝑝))) ↔ ((𝐵‘𝑖) − (𝐴‘𝑖)) = ((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
104 | | eqcom 2828 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵‘𝑖) − (𝐴‘𝑖)) = ((((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) / ((𝐶‘𝑝) − (𝐴‘𝑝))) ↔ ((((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) / ((𝐶‘𝑝) − (𝐴‘𝑝))) = ((𝐵‘𝑖) − (𝐴‘𝑖))) |
105 | 87, 97 | mulcld 10655 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → (((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ∈ ℂ) |
106 | 83, 84 | subcld 10991 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → ((𝐵‘𝑖) − (𝐴‘𝑖)) ∈ ℂ) |
107 | 105, 89, 106, 94 | divmuld 11432 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → (((((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) / ((𝐶‘𝑝) − (𝐴‘𝑝))) = ((𝐵‘𝑖) − (𝐴‘𝑖)) ↔ (((𝐶‘𝑝) − (𝐴‘𝑝)) · ((𝐵‘𝑖) − (𝐴‘𝑖))) = (((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
108 | 89, 106 | mulcomd 10656 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → (((𝐶‘𝑝) − (𝐴‘𝑝)) · ((𝐵‘𝑖) − (𝐴‘𝑖))) = (((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑝) − (𝐴‘𝑝)))) |
109 | 108 | eqeq1d 2823 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → ((((𝐶‘𝑝) − (𝐴‘𝑝)) · ((𝐵‘𝑖) − (𝐴‘𝑖))) = (((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ (((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑝) − (𝐴‘𝑝))) = (((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
110 | 107, 109 | bitrd 281 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → (((((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) / ((𝐶‘𝑝) − (𝐴‘𝑝))) = ((𝐵‘𝑖) − (𝐴‘𝑖)) ↔ (((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑝) − (𝐴‘𝑝))) = (((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
111 | 104, 110 | syl5bb 285 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → (((𝐵‘𝑖) − (𝐴‘𝑖)) = ((((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) / ((𝐶‘𝑝) − (𝐴‘𝑝))) ↔ (((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑝) − (𝐴‘𝑝))) = (((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
112 | 101, 103,
111 | 3bitr2d 309 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → ((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) = (𝐵‘𝑖) ↔ (((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑝) − (𝐴‘𝑝))) = (((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
113 | 82, 112 | syl5bb 285 |
. . . . . . . . . . . . 13
⊢ ((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ ∧ (𝐶‘𝑖) ∈ ℂ) ∧ ((𝐴‘𝑝) ∈ ℂ ∧ (𝐵‘𝑝) ∈ ℂ ∧ (𝐶‘𝑝) ∈ ℂ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → ((𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) ↔ (((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑝) − (𝐴‘𝑝))) = (((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
114 | 74, 80, 81, 113 | syl3anc 1367 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) ↔ (((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑝) − (𝐴‘𝑝))) = (((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
115 | 114 | ralbidva 3196 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝))) → (∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) ↔ ∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑝) − (𝐴‘𝑝))) = (((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
116 | | 3simpb 1145 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) |
117 | | simpl2 1188 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → (𝐵‘𝑝) ∈ ℝ) |
118 | | simpl1 1187 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → (𝐴‘𝑝) ∈ ℝ) |
119 | 117, 118 | resubcld 11062 |
. . . . . . . . . . . . 13
⊢ ((((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → ((𝐵‘𝑝) − (𝐴‘𝑝)) ∈ ℝ) |
120 | | simpl3 1189 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → (𝐶‘𝑝) ∈ ℝ) |
121 | 120, 118 | resubcld 11062 |
. . . . . . . . . . . . 13
⊢ ((((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → ((𝐶‘𝑝) − (𝐴‘𝑝)) ∈ ℝ) |
122 | | simp3 1134 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) → (𝐶‘𝑝) ∈ ℝ) |
123 | 122 | recnd 10663 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) → (𝐶‘𝑝) ∈ ℂ) |
124 | 75 | 3ad2ant1 1129 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) → (𝐴‘𝑝) ∈ ℂ) |
125 | 123, 124 | subeq0ad 11001 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) → (((𝐶‘𝑝) − (𝐴‘𝑝)) = 0 ↔ (𝐶‘𝑝) = (𝐴‘𝑝))) |
126 | 125 | necon3bid 3060 |
. . . . . . . . . . . . . 14
⊢ (((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) → (((𝐶‘𝑝) − (𝐴‘𝑝)) ≠ 0 ↔ (𝐶‘𝑝) ≠ (𝐴‘𝑝))) |
127 | 126 | biimpar 480 |
. . . . . . . . . . . . 13
⊢ ((((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → ((𝐶‘𝑝) − (𝐴‘𝑝)) ≠ 0) |
128 | 119, 121,
127 | redivcld 11462 |
. . . . . . . . . . . 12
⊢ ((((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝)) → (((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) ∈ ℝ) |
129 | | colinearalglem4 26689 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)(((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) ≤ 0)) |
130 | | oveq1 7157 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → ((𝐵‘𝑖) − (𝐴‘𝑖)) = ((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖))) |
131 | 130 | oveq1d 7165 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → (((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) = (((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) |
132 | 131 | breq1d 5068 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → ((((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ↔ (((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0)) |
133 | 132 | ralimi 3160 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑖 ∈
(1...𝑁)(𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → ∀𝑖 ∈ (1...𝑁)((((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ↔ (((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0)) |
134 | | ralbi 3167 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑖 ∈
(1...𝑁)((((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ↔ (((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0) → (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0)) |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(∀𝑖 ∈
(1...𝑁)(𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0)) |
136 | | oveq2 7158 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → ((𝐶‘𝑖) − (𝐵‘𝑖)) = ((𝐶‘𝑖) − (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) |
137 | | oveq2 7158 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → ((𝐴‘𝑖) − (𝐵‘𝑖)) = ((𝐴‘𝑖) − (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) |
138 | 136, 137 | oveq12d 7168 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → (((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) = (((𝐶‘𝑖) − (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))))) |
139 | 138 | breq1d 5068 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → ((((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ↔ (((𝐶‘𝑖) − (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) ≤ 0)) |
140 | 139 | ralimi 3160 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑖 ∈
(1...𝑁)(𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → ∀𝑖 ∈ (1...𝑁)((((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ↔ (((𝐶‘𝑖) − (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) ≤ 0)) |
141 | | ralbi 3167 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑖 ∈
(1...𝑁)((((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ↔ (((𝐶‘𝑖) − (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) ≤ 0) → (∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) ≤ 0)) |
142 | 140, 141 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(∀𝑖 ∈
(1...𝑁)(𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → (∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) ≤ 0)) |
143 | | oveq1 7157 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → ((𝐵‘𝑖) − (𝐶‘𝑖)) = ((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) |
144 | 143 | oveq2d 7166 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → (((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) = (((𝐴‘𝑖) − (𝐶‘𝑖)) · ((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖)))) |
145 | 144 | breq1d 5068 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → ((((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ↔ (((𝐴‘𝑖) − (𝐶‘𝑖)) · ((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) ≤ 0)) |
146 | 145 | ralimi 3160 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑖 ∈
(1...𝑁)(𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → ∀𝑖 ∈ (1...𝑁)((((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ↔ (((𝐴‘𝑖) − (𝐶‘𝑖)) · ((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) ≤ 0)) |
147 | | ralbi 3167 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑖 ∈
(1...𝑁)((((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ↔ (((𝐴‘𝑖) − (𝐶‘𝑖)) · ((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) ≤ 0) → (∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) ≤ 0)) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(∀𝑖 ∈
(1...𝑁)(𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → (∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) ≤ 0)) |
149 | 135, 142,
148 | 3orbi123d 1431 |
. . . . . . . . . . . . 13
⊢
(∀𝑖 ∈
(1...𝑁)(𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → ((∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0) ↔ (∀𝑖 ∈ (1...𝑁)(((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖))) · ((𝐴‘𝑖) − (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) − (𝐶‘𝑖))) ≤ 0))) |
150 | 129, 149 | syl5ibrcom 249 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0))) |
151 | 116, 128,
150 | syl2an 597 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝))) → (∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((((𝐵‘𝑝) − (𝐴‘𝑝)) / ((𝐶‘𝑝) − (𝐴‘𝑝))) · ((𝐶‘𝑖) − (𝐴‘𝑖))) + (𝐴‘𝑖)) → (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0))) |
152 | 115, 151 | sylbird 262 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴‘𝑝) ∈ ℝ ∧ (𝐵‘𝑝) ∈ ℝ ∧ (𝐶‘𝑝) ∈ ℝ) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝))) → (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑝) − (𝐴‘𝑝))) = (((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0))) |
153 | 68, 152 | syldan 593 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (1...𝑁) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝))) → (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑝) − (𝐴‘𝑝))) = (((𝐵‘𝑝) − (𝐴‘𝑝)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0))) |
154 | 59, 153 | syld 47 |
. . . . . . . 8
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (1...𝑁) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝))) → (∀𝑗 ∈ (1...𝑁)∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0))) |
155 | 48, 154 | syl5bi 244 |
. . . . . . 7
⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (1...𝑁) ∧ (𝐶‘𝑝) ≠ (𝐴‘𝑝))) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0))) |
156 | 155 | rexlimdvaa 3285 |
. . . . . 6
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∃𝑝 ∈ (1...𝑁)(𝐶‘𝑝) ≠ (𝐴‘𝑝) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0)))) |
157 | 47, 156 | sylbid 242 |
. . . . 5
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶 ≠ 𝐴 → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0)))) |
158 | 37, 157 | pm2.61dne 3103 |
. . . 4
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0))) |
159 | 158 | pm4.71rd 565 |
. . 3
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ↔ ((∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))) |
160 | | andir 1005 |
. . . . 5
⊢
(((∀𝑖 ∈
(1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ↔ ((∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))) |
161 | 160 | orbi1i 910 |
. . . 4
⊢
((((∀𝑖 ∈
(1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) ↔ (((∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))) |
162 | | df-3or 1084 |
. . . . . 6
⊢
((∀𝑖 ∈
(1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0) ↔ ((∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0) ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0)) |
163 | 162 | anbi1i 625 |
. . . . 5
⊢
(((∀𝑖 ∈
(1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ↔ (((∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0) ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
164 | | andir 1005 |
. . . . 5
⊢
((((∀𝑖 ∈
(1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0) ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ↔ (((∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))) |
165 | 163, 164 | bitri 277 |
. . . 4
⊢
(((∀𝑖 ∈
(1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ↔ (((∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))) |
166 | | df-3or 1084 |
. . . 4
⊢
(((∀𝑖 ∈
(1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) ↔ (((∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))) |
167 | 161, 165,
166 | 3bitr4i 305 |
. . 3
⊢
(((∀𝑖 ∈
(1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ↔ ((∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))))) |
168 | 159, 167 | syl6rbb 290 |
. 2
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (((∀𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑖) − (𝐴‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐵‘𝑖)) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐶‘𝑖)) · ((𝐵‘𝑖) − (𝐶‘𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |
169 | 13, 168 | bitrd 281 |
1
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ((𝐴 Btwn 〈𝐵, 𝐶〉 ∨ 𝐵 Btwn 〈𝐶, 𝐴〉 ∨ 𝐶 Btwn 〈𝐴, 𝐵〉) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐴‘𝑖)) · ((𝐶‘𝑗) − (𝐴‘𝑗))) = (((𝐵‘𝑗) − (𝐴‘𝑗)) · ((𝐶‘𝑖) − (𝐴‘𝑖))))) |