MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  colinearalg Structured version   Visualization version   GIF version

Theorem colinearalg 27567
Description: An algebraic characterization of colinearity. Note the similarity to brbtwn2 27562. (Contributed by Scott Fenton, 24-Jun-2013.)
Assertion
Ref Expression
colinearalg ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ((𝐴 Btwn ⟨𝐵, 𝐶⟩ ∨ 𝐵 Btwn ⟨𝐶, 𝐴⟩ ∨ 𝐶 Btwn ⟨𝐴, 𝐵⟩) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))))
Distinct variable groups:   𝑖,𝑁,𝑗   𝐴,𝑖,𝑗   𝐵,𝑖,𝑗   𝐶,𝑖,𝑗

Proof of Theorem colinearalg
Dummy variable 𝑝 is distinct from all other variables.
StepHypRef Expression
1 brbtwn2 27562 . . 3 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴 Btwn ⟨𝐵, 𝐶⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
2 brbtwn2 27562 . . . . 5 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝐵 Btwn ⟨𝐶, 𝐴⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑗) − (𝐵𝑗))) = (((𝐶𝑗) − (𝐵𝑗)) · ((𝐴𝑖) − (𝐵𝑖))))))
323comr 1124 . . . 4 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐵 Btwn ⟨𝐶, 𝐴⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑗) − (𝐵𝑗))) = (((𝐶𝑗) − (𝐵𝑗)) · ((𝐴𝑖) − (𝐵𝑖))))))
4 colinearalglem3 27565 . . . . . 6 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑗) − (𝐵𝑗))) = (((𝐶𝑗) − (𝐵𝑗)) · ((𝐴𝑖) − (𝐵𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))))
543comr 1124 . . . . 5 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑗) − (𝐵𝑗))) = (((𝐶𝑗) − (𝐵𝑗)) · ((𝐴𝑖) − (𝐵𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))))
65anbi2d 629 . . . 4 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ((∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑗) − (𝐵𝑗))) = (((𝐶𝑗) − (𝐵𝑗)) · ((𝐴𝑖) − (𝐵𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
73, 6bitrd 278 . . 3 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐵 Btwn ⟨𝐶, 𝐴⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
8 brbtwn2 27562 . . . . 5 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝐶 Btwn ⟨𝐴, 𝐵⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑗) − (𝐶𝑗))) = (((𝐴𝑗) − (𝐶𝑗)) · ((𝐵𝑖) − (𝐶𝑖))))))
9 colinearalglem2 27564 . . . . . 6 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑗) − (𝐶𝑗))) = (((𝐴𝑗) − (𝐶𝑗)) · ((𝐵𝑖) − (𝐶𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))))
109anbi2d 629 . . . . 5 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ((∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑗) − (𝐶𝑗))) = (((𝐴𝑗) − (𝐶𝑗)) · ((𝐵𝑖) − (𝐶𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
118, 10bitrd 278 . . . 4 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝐶 Btwn ⟨𝐴, 𝐵⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
12113coml 1126 . . 3 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶 Btwn ⟨𝐴, 𝐵⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
131, 7, 123orbi123d 1434 . 2 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ((𝐴 Btwn ⟨𝐵, 𝐶⟩ ∨ 𝐵 Btwn ⟨𝐶, 𝐴⟩ ∨ 𝐶 Btwn ⟨𝐴, 𝐵⟩) ↔ ((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))))))
14 fveecn 27559 . . . . . . . . . . . . 13 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵𝑖) ∈ ℂ)
15 fveecn 27559 . . . . . . . . . . . . 13 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶𝑖) ∈ ℂ)
16 subid 11341 . . . . . . . . . . . . . . . 16 ((𝐶𝑖) ∈ ℂ → ((𝐶𝑖) − (𝐶𝑖)) = 0)
1716oveq2d 7353 . . . . . . . . . . . . . . 15 ((𝐶𝑖) ∈ ℂ → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) = (((𝐵𝑖) − (𝐶𝑖)) · 0))
1817adantl 482 . . . . . . . . . . . . . 14 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) = (((𝐵𝑖) − (𝐶𝑖)) · 0))
19 subcl 11321 . . . . . . . . . . . . . . 15 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) → ((𝐵𝑖) − (𝐶𝑖)) ∈ ℂ)
2019mul01d 11275 . . . . . . . . . . . . . 14 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) → (((𝐵𝑖) − (𝐶𝑖)) · 0) = 0)
2118, 20eqtrd 2776 . . . . . . . . . . . . 13 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) = 0)
2214, 15, 21syl2an 596 . . . . . . . . . . . 12 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁))) → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) = 0)
2322anandirs 676 . . . . . . . . . . 11 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) = 0)
24 0le0 12175 . . . . . . . . . . 11 0 ≤ 0
2523, 24eqbrtrdi 5131 . . . . . . . . . 10 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) ≤ 0)
2625ralrimiva 3139 . . . . . . . . 9 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) ≤ 0)
27263adant1 1129 . . . . . . . 8 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) ≤ 0)
28 fveq1 6824 . . . . . . . . . . . 12 (𝐶 = 𝐴 → (𝐶𝑖) = (𝐴𝑖))
2928oveq2d 7353 . . . . . . . . . . 11 (𝐶 = 𝐴 → ((𝐵𝑖) − (𝐶𝑖)) = ((𝐵𝑖) − (𝐴𝑖)))
3028oveq2d 7353 . . . . . . . . . . 11 (𝐶 = 𝐴 → ((𝐶𝑖) − (𝐶𝑖)) = ((𝐶𝑖) − (𝐴𝑖)))
3129, 30oveq12d 7355 . . . . . . . . . 10 (𝐶 = 𝐴 → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) = (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))))
3231breq1d 5102 . . . . . . . . 9 (𝐶 = 𝐴 → ((((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) ≤ 0 ↔ (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
3332ralbidv 3170 . . . . . . . 8 (𝐶 = 𝐴 → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
3427, 33syl5ibcom 244 . . . . . . 7 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶 = 𝐴 → ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
35 3mix1 1329 . . . . . . 7 (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0))
3634, 35syl6 35 . . . . . 6 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶 = 𝐴 → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0)))
3736a1dd 50 . . . . 5 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶 = 𝐴 → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0))))
38 simp3 1137 . . . . . . . . 9 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁))
39 simp1 1135 . . . . . . . . 9 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁))
40 eqeefv 27560 . . . . . . . . 9 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝐶 = 𝐴 ↔ ∀𝑝 ∈ (1...𝑁)(𝐶𝑝) = (𝐴𝑝)))
4138, 39, 40syl2anc 584 . . . . . . . 8 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶 = 𝐴 ↔ ∀𝑝 ∈ (1...𝑁)(𝐶𝑝) = (𝐴𝑝)))
4241necon3abid 2977 . . . . . . 7 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶𝐴 ↔ ¬ ∀𝑝 ∈ (1...𝑁)(𝐶𝑝) = (𝐴𝑝)))
43 df-ne 2941 . . . . . . . . 9 ((𝐶𝑝) ≠ (𝐴𝑝) ↔ ¬ (𝐶𝑝) = (𝐴𝑝))
4443rexbii 3093 . . . . . . . 8 (∃𝑝 ∈ (1...𝑁)(𝐶𝑝) ≠ (𝐴𝑝) ↔ ∃𝑝 ∈ (1...𝑁) ¬ (𝐶𝑝) = (𝐴𝑝))
45 rexnal 3099 . . . . . . . 8 (∃𝑝 ∈ (1...𝑁) ¬ (𝐶𝑝) = (𝐴𝑝) ↔ ¬ ∀𝑝 ∈ (1...𝑁)(𝐶𝑝) = (𝐴𝑝))
4644, 45bitr2i 275 . . . . . . 7 (¬ ∀𝑝 ∈ (1...𝑁)(𝐶𝑝) = (𝐴𝑝) ↔ ∃𝑝 ∈ (1...𝑁)(𝐶𝑝) ≠ (𝐴𝑝))
4742, 46bitrdi 286 . . . . . 6 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶𝐴 ↔ ∃𝑝 ∈ (1...𝑁)(𝐶𝑝) ≠ (𝐴𝑝)))
48 ralcom 3268 . . . . . . . 8 (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) ↔ ∀𝑗 ∈ (1...𝑁)∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))
49 fveq2 6825 . . . . . . . . . . . . . . 15 (𝑗 = 𝑝 → (𝐶𝑗) = (𝐶𝑝))
50 fveq2 6825 . . . . . . . . . . . . . . 15 (𝑗 = 𝑝 → (𝐴𝑗) = (𝐴𝑝))
5149, 50oveq12d 7355 . . . . . . . . . . . . . 14 (𝑗 = 𝑝 → ((𝐶𝑗) − (𝐴𝑗)) = ((𝐶𝑝) − (𝐴𝑝)))
5251oveq2d 7353 . . . . . . . . . . . . 13 (𝑗 = 𝑝 → (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))))
53 fveq2 6825 . . . . . . . . . . . . . . 15 (𝑗 = 𝑝 → (𝐵𝑗) = (𝐵𝑝))
5453, 50oveq12d 7355 . . . . . . . . . . . . . 14 (𝑗 = 𝑝 → ((𝐵𝑗) − (𝐴𝑗)) = ((𝐵𝑝) − (𝐴𝑝)))
5554oveq1d 7352 . . . . . . . . . . . . 13 (𝑗 = 𝑝 → (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))))
5652, 55eqeq12d 2752 . . . . . . . . . . . 12 (𝑗 = 𝑝 → ((((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) ↔ (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
5756ralbidv 3170 . . . . . . . . . . 11 (𝑗 = 𝑝 → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
5857rspcv 3566 . . . . . . . . . 10 (𝑝 ∈ (1...𝑁) → (∀𝑗 ∈ (1...𝑁)∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) → ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
5958ad2antrl 725 . . . . . . . . 9 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (1...𝑁) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (∀𝑗 ∈ (1...𝑁)∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) → ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
60 fveere 27558 . . . . . . . . . . . . . 14 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (1...𝑁)) → (𝐴𝑝) ∈ ℝ)
61603ad2antl1 1184 . . . . . . . . . . . . 13 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) → (𝐴𝑝) ∈ ℝ)
62 fveere 27558 . . . . . . . . . . . . . 14 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (1...𝑁)) → (𝐵𝑝) ∈ ℝ)
63623ad2antl2 1185 . . . . . . . . . . . . 13 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) → (𝐵𝑝) ∈ ℝ)
64 fveere 27558 . . . . . . . . . . . . . 14 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (1...𝑁)) → (𝐶𝑝) ∈ ℝ)
65643ad2antl3 1186 . . . . . . . . . . . . 13 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) → (𝐶𝑝) ∈ ℝ)
6661, 63, 653jca 1127 . . . . . . . . . . . 12 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) → ((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ))
6766anim1i 615 . . . . . . . . . . 11 ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)))
6867anasss 467 . . . . . . . . . 10 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (1...𝑁) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)))
69 fveecn 27559 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴𝑖) ∈ ℂ)
70693ad2antl1 1184 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴𝑖) ∈ ℂ)
71143ad2antl2 1185 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵𝑖) ∈ ℂ)
72153ad2antl3 1186 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶𝑖) ∈ ℂ)
7370, 71, 723jca 1127 . . . . . . . . . . . . . 14 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ))
7473adantlr 712 . . . . . . . . . . . . 13 ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ))
75 recn 11062 . . . . . . . . . . . . . . . 16 ((𝐴𝑝) ∈ ℝ → (𝐴𝑝) ∈ ℂ)
76 recn 11062 . . . . . . . . . . . . . . . 16 ((𝐵𝑝) ∈ ℝ → (𝐵𝑝) ∈ ℂ)
77 recn 11062 . . . . . . . . . . . . . . . 16 ((𝐶𝑝) ∈ ℝ → (𝐶𝑝) ∈ ℂ)
7875, 76, 773anim123i 1150 . . . . . . . . . . . . . . 15 (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) → ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ))
7978adantr 481 . . . . . . . . . . . . . 14 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ))
8079ad2antlr 724 . . . . . . . . . . . . 13 ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ))
81 simplrr 775 . . . . . . . . . . . . 13 ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶𝑝) ≠ (𝐴𝑝))
82 eqcom 2743 . . . . . . . . . . . . . 14 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) ↔ (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) = (𝐵𝑖))
83 simp12 1203 . . . . . . . . . . . . . . . 16 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐵𝑖) ∈ ℂ)
84 simp11 1202 . . . . . . . . . . . . . . . 16 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐴𝑖) ∈ ℂ)
85 simp22 1206 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐵𝑝) ∈ ℂ)
86 simp21 1205 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐴𝑝) ∈ ℂ)
8785, 86subcld 11433 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐵𝑝) − (𝐴𝑝)) ∈ ℂ)
88 simp23 1207 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐶𝑝) ∈ ℂ)
8988, 86subcld 11433 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐶𝑝) − (𝐴𝑝)) ∈ ℂ)
90 simpr3 1195 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ)) → (𝐶𝑝) ∈ ℂ)
91 simpr1 1193 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ)) → (𝐴𝑝) ∈ ℂ)
9290, 91subeq0ad 11443 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ)) → (((𝐶𝑝) − (𝐴𝑝)) = 0 ↔ (𝐶𝑝) = (𝐴𝑝)))
9392necon3bid 2985 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ)) → (((𝐶𝑝) − (𝐴𝑝)) ≠ 0 ↔ (𝐶𝑝) ≠ (𝐴𝑝)))
9493biimp3ar 1469 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐶𝑝) − (𝐴𝑝)) ≠ 0)
9587, 89, 94divcld 11852 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) ∈ ℂ)
96 simp13 1204 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐶𝑖) ∈ ℂ)
9796, 84subcld 11433 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐶𝑖) − (𝐴𝑖)) ∈ ℂ)
9895, 97mulcld 11096 . . . . . . . . . . . . . . . 16 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) ∈ ℂ)
99 subadd2 11326 . . . . . . . . . . . . . . . . 17 (((𝐵𝑖) ∈ ℂ ∧ (𝐴𝑖) ∈ ℂ ∧ ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) ∈ ℂ) → (((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) ↔ (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) = (𝐵𝑖)))
10099bicomd 222 . . . . . . . . . . . . . . . 16 (((𝐵𝑖) ∈ ℂ ∧ (𝐴𝑖) ∈ ℂ ∧ ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) ∈ ℂ) → ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) = (𝐵𝑖) ↔ ((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖)))))
10183, 84, 98, 100syl3anc 1370 . . . . . . . . . . . . . . 15 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) = (𝐵𝑖) ↔ ((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖)))))
10287, 97, 89, 94div23d 11889 . . . . . . . . . . . . . . . 16 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) = ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))))
103102eqeq2d 2747 . . . . . . . . . . . . . . 15 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) ↔ ((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖)))))
104 eqcom 2743 . . . . . . . . . . . . . . . 16 (((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) ↔ ((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) = ((𝐵𝑖) − (𝐴𝑖)))
10587, 97mulcld 11096 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) ∈ ℂ)
10683, 84subcld 11433 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐵𝑖) − (𝐴𝑖)) ∈ ℂ)
107105, 89, 106, 94divmuld 11874 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) = ((𝐵𝑖) − (𝐴𝑖)) ↔ (((𝐶𝑝) − (𝐴𝑝)) · ((𝐵𝑖) − (𝐴𝑖))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
10889, 106mulcomd 11097 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐶𝑝) − (𝐴𝑝)) · ((𝐵𝑖) − (𝐴𝑖))) = (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))))
109108eqeq1d 2738 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((((𝐶𝑝) − (𝐴𝑝)) · ((𝐵𝑖) − (𝐴𝑖))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) ↔ (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
110107, 109bitrd 278 . . . . . . . . . . . . . . . 16 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) = ((𝐵𝑖) − (𝐴𝑖)) ↔ (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
111104, 110bitrid 282 . . . . . . . . . . . . . . 15 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) ↔ (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
112101, 103, 1113bitr2d 306 . . . . . . . . . . . . . 14 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) = (𝐵𝑖) ↔ (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
11382, 112bitrid 282 . . . . . . . . . . . . 13 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) ↔ (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
11474, 80, 81, 113syl3anc 1370 . . . . . . . . . . . 12 ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) ↔ (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
115114ralbidva 3168 . . . . . . . . . . 11 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) ↔ ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
116 3simpb 1148 . . . . . . . . . . . 12 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)))
117 simpl2 1191 . . . . . . . . . . . . . 14 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐵𝑝) ∈ ℝ)
118 simpl1 1190 . . . . . . . . . . . . . 14 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐴𝑝) ∈ ℝ)
119117, 118resubcld 11504 . . . . . . . . . . . . 13 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐵𝑝) − (𝐴𝑝)) ∈ ℝ)
120 simpl3 1192 . . . . . . . . . . . . . 14 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐶𝑝) ∈ ℝ)
121120, 118resubcld 11504 . . . . . . . . . . . . 13 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐶𝑝) − (𝐴𝑝)) ∈ ℝ)
122 simp3 1137 . . . . . . . . . . . . . . . . 17 (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) → (𝐶𝑝) ∈ ℝ)
123122recnd 11104 . . . . . . . . . . . . . . . 16 (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) → (𝐶𝑝) ∈ ℂ)
124753ad2ant1 1132 . . . . . . . . . . . . . . . 16 (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) → (𝐴𝑝) ∈ ℂ)
125123, 124subeq0ad 11443 . . . . . . . . . . . . . . 15 (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) → (((𝐶𝑝) − (𝐴𝑝)) = 0 ↔ (𝐶𝑝) = (𝐴𝑝)))
126125necon3bid 2985 . . . . . . . . . . . . . 14 (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) → (((𝐶𝑝) − (𝐴𝑝)) ≠ 0 ↔ (𝐶𝑝) ≠ (𝐴𝑝)))
127126biimpar 478 . . . . . . . . . . . . 13 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐶𝑝) − (𝐴𝑝)) ≠ 0)
128119, 121, 127redivcld 11904 . . . . . . . . . . . 12 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) ∈ ℝ)
129 colinearalglem4 27566 . . . . . . . . . . . . 13 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)(((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))) ≤ 0))
130 oveq1 7344 . . . . . . . . . . . . . . . . . 18 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((𝐵𝑖) − (𝐴𝑖)) = ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)))
131130oveq1d 7352 . . . . . . . . . . . . . . . . 17 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) = (((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))))
132131breq1d 5102 . . . . . . . . . . . . . . . 16 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ↔ (((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
133132ralimi 3082 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ∀𝑖 ∈ (1...𝑁)((((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ↔ (((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
134 ralbi 3102 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)((((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ↔ (((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
135133, 134syl 17 . . . . . . . . . . . . . 14 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
136 oveq2 7345 . . . . . . . . . . . . . . . . . 18 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((𝐶𝑖) − (𝐵𝑖)) = ((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))))
137 oveq2 7345 . . . . . . . . . . . . . . . . . 18 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((𝐴𝑖) − (𝐵𝑖)) = ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))))
138136, 137oveq12d 7355 . . . . . . . . . . . . . . . . 17 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) = (((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))))
139138breq1d 5102 . . . . . . . . . . . . . . . 16 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ↔ (((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0))
140139ralimi 3082 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ∀𝑖 ∈ (1...𝑁)((((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ↔ (((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0))
141 ralbi 3102 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)((((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ↔ (((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0) → (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0))
142140, 141syl 17 . . . . . . . . . . . . . 14 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0))
143 oveq1 7344 . . . . . . . . . . . . . . . . . 18 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((𝐵𝑖) − (𝐶𝑖)) = ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖)))
144143oveq2d 7353 . . . . . . . . . . . . . . . . 17 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) = (((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))))
145144breq1d 5102 . . . . . . . . . . . . . . . 16 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ↔ (((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))) ≤ 0))
146145ralimi 3082 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ∀𝑖 ∈ (1...𝑁)((((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ↔ (((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))) ≤ 0))
147 ralbi 3102 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)((((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ↔ (((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))) ≤ 0) → (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))) ≤ 0))
148146, 147syl 17 . . . . . . . . . . . . . 14 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))) ≤ 0))
149135, 142, 1483orbi123d 1434 . . . . . . . . . . . . 13 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0) ↔ (∀𝑖 ∈ (1...𝑁)(((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))) ≤ 0)))
150129, 149syl5ibrcom 246 . . . . . . . . . . . 12 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0)))
151116, 128, 150syl2an 596 . . . . . . . . . . 11 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0)))
152115, 151sylbird 259 . . . . . . . . . 10 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0)))
15368, 152syldan 591 . . . . . . . . 9 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (1...𝑁) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0)))
15459, 153syld 47 . . . . . . . 8 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (1...𝑁) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (∀𝑗 ∈ (1...𝑁)∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0)))
15548, 154biimtrid 241 . . . . . . 7 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (1...𝑁) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0)))
156155rexlimdvaa 3149 . . . . . 6 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∃𝑝 ∈ (1...𝑁)(𝐶𝑝) ≠ (𝐴𝑝) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0))))
15747, 156sylbid 239 . . . . 5 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶𝐴 → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0))))
15837, 157pm2.61dne 3028 . . . 4 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0)))
159158pm4.71rd 563 . . 3 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) ↔ ((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
160 andir 1006 . . . . 5 (((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ↔ ((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
161160orbi1i 911 . . . 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 1087 . . . . . 6 ((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0) ↔ ((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0) ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0))
163162anbi1i 624 . . . . 5 (((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ↔ (((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0) ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))))
164 andir 1006 . . . . 5 ((((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0) ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ↔ (((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
165163, 164bitri 274 . . . 4 (((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ↔ (((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
166 df-3or 1087 . . . 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...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
167161, 165, 1663bitr4i 302 . . 3 (((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ↔ ((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
168159, 167bitr2di 287 . 2 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))))
16913, 168bitrd 278 1 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ((𝐴 Btwn ⟨𝐵, 𝐶⟩ ∨ 𝐵 Btwn ⟨𝐶, 𝐴⟩ ∨ 𝐶 Btwn ⟨𝐴, 𝐵⟩) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844  w3o 1085  w3a 1086   = wceq 1540  wcel 2105  wne 2940  wral 3061  wrex 3070  cop 4579   class class class wbr 5092  cfv 6479  (class class class)co 7337  cc 10970  cr 10971  0cc0 10972  1c1 10973   + caddc 10975   · cmul 10977  cle 11111  cmin 11306   / cdiv 11733  ...cfz 13340  𝔼cee 27545   Btwn cbtwn 27546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-cnex 11028  ax-resscn 11029  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-mulcom 11036  ax-addass 11037  ax-mulass 11038  ax-distr 11039  ax-i2m1 11040  ax-1ne0 11041  ax-1rid 11042  ax-rnegex 11043  ax-rrecex 11044  ax-cnre 11045  ax-pre-lttri 11046  ax-pre-lttrn 11047  ax-pre-ltadd 11048  ax-pre-mulgt0 11049
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-riota 7293  df-ov 7340  df-oprab 7341  df-mpo 7342  df-om 7781  df-1st 7899  df-2nd 7900  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-rdg 8311  df-er 8569  df-map 8688  df-en 8805  df-dom 8806  df-sdom 8807  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116  df-sub 11308  df-neg 11309  df-div 11734  df-nn 12075  df-2 12137  df-n0 12335  df-z 12421  df-uz 12684  df-icc 13187  df-fz 13341  df-seq 13823  df-exp 13884  df-ee 27548  df-btwn 27549
This theorem is referenced by:  axlowdimlem6  27604
  Copyright terms: Public domain W3C validator