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

Theorem colinearalg 28945
Description: An algebraic characterization of colinearity. Note the similarity to brbtwn2 28940. (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 28940 . . 3 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴 Btwn ⟨𝐵, 𝐶⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
2 brbtwn2 28940 . . . . 5 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝐵 Btwn ⟨𝐶, 𝐴⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑗) − (𝐵𝑗))) = (((𝐶𝑗) − (𝐵𝑗)) · ((𝐴𝑖) − (𝐵𝑖))))))
323comr 1125 . . . 4 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐵 Btwn ⟨𝐶, 𝐴⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑗) − (𝐵𝑗))) = (((𝐶𝑗) − (𝐵𝑗)) · ((𝐴𝑖) − (𝐵𝑖))))))
4 colinearalglem3 28943 . . . . . 6 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑗) − (𝐵𝑗))) = (((𝐶𝑗) − (𝐵𝑗)) · ((𝐴𝑖) − (𝐵𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))))
543comr 1125 . . . . 5 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑗) − (𝐵𝑗))) = (((𝐶𝑗) − (𝐵𝑗)) · ((𝐴𝑖) − (𝐵𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))))
65anbi2d 629 . . . 4 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ((∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑗) − (𝐵𝑗))) = (((𝐶𝑗) − (𝐵𝑗)) · ((𝐴𝑖) − (𝐵𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
73, 6bitrd 279 . . 3 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐵 Btwn ⟨𝐶, 𝐴⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
8 brbtwn2 28940 . . . . 5 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝐶 Btwn ⟨𝐴, 𝐵⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑗) − (𝐶𝑗))) = (((𝐴𝑗) − (𝐶𝑗)) · ((𝐵𝑖) − (𝐶𝑖))))))
9 colinearalglem2 28942 . . . . . 6 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑗) − (𝐶𝑗))) = (((𝐴𝑗) − (𝐶𝑗)) · ((𝐵𝑖) − (𝐶𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))))
109anbi2d 629 . . . . 5 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ((∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑗) − (𝐶𝑗))) = (((𝐴𝑗) − (𝐶𝑗)) · ((𝐵𝑖) − (𝐶𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
118, 10bitrd 279 . . . 4 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝐶 Btwn ⟨𝐴, 𝐵⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
12113coml 1127 . . 3 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶 Btwn ⟨𝐴, 𝐵⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
131, 7, 123orbi123d 1435 . 2 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ((𝐴 Btwn ⟨𝐵, 𝐶⟩ ∨ 𝐵 Btwn ⟨𝐶, 𝐴⟩ ∨ 𝐶 Btwn ⟨𝐴, 𝐵⟩) ↔ ((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))))))
14 fveecn 28937 . . . . . . . . . . . . 13 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵𝑖) ∈ ℂ)
15 fveecn 28937 . . . . . . . . . . . . 13 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶𝑖) ∈ ℂ)
16 subid 11557 . . . . . . . . . . . . . . . 16 ((𝐶𝑖) ∈ ℂ → ((𝐶𝑖) − (𝐶𝑖)) = 0)
1716oveq2d 7466 . . . . . . . . . . . . . . 15 ((𝐶𝑖) ∈ ℂ → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) = (((𝐵𝑖) − (𝐶𝑖)) · 0))
1817adantl 481 . . . . . . . . . . . . . 14 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) = (((𝐵𝑖) − (𝐶𝑖)) · 0))
19 subcl 11537 . . . . . . . . . . . . . . 15 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) → ((𝐵𝑖) − (𝐶𝑖)) ∈ ℂ)
2019mul01d 11491 . . . . . . . . . . . . . 14 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) → (((𝐵𝑖) − (𝐶𝑖)) · 0) = 0)
2118, 20eqtrd 2780 . . . . . . . . . . . . 13 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) = 0)
2214, 15, 21syl2an 595 . . . . . . . . . . . 12 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁))) → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) = 0)
2322anandirs 678 . . . . . . . . . . 11 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) = 0)
24 0le0 12396 . . . . . . . . . . 11 0 ≤ 0
2523, 24eqbrtrdi 5205 . . . . . . . . . 10 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) ≤ 0)
2625ralrimiva 3152 . . . . . . . . 9 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) ≤ 0)
27263adant1 1130 . . . . . . . 8 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) ≤ 0)
28 fveq1 6921 . . . . . . . . . . . 12 (𝐶 = 𝐴 → (𝐶𝑖) = (𝐴𝑖))
2928oveq2d 7466 . . . . . . . . . . 11 (𝐶 = 𝐴 → ((𝐵𝑖) − (𝐶𝑖)) = ((𝐵𝑖) − (𝐴𝑖)))
3028oveq2d 7466 . . . . . . . . . . 11 (𝐶 = 𝐴 → ((𝐶𝑖) − (𝐶𝑖)) = ((𝐶𝑖) − (𝐴𝑖)))
3129, 30oveq12d 7468 . . . . . . . . . 10 (𝐶 = 𝐴 → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) = (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))))
3231breq1d 5176 . . . . . . . . 9 (𝐶 = 𝐴 → ((((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) ≤ 0 ↔ (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
3332ralbidv 3184 . . . . . . . 8 (𝐶 = 𝐴 → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
3427, 33syl5ibcom 245 . . . . . . 7 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶 = 𝐴 → ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
35 3mix1 1330 . . . . . . 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 1138 . . . . . . . . 9 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁))
39 simp1 1136 . . . . . . . . 9 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁))
40 eqeefv 28938 . . . . . . . . 9 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝐶 = 𝐴 ↔ ∀𝑝 ∈ (1...𝑁)(𝐶𝑝) = (𝐴𝑝)))
4138, 39, 40syl2anc 583 . . . . . . . 8 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶 = 𝐴 ↔ ∀𝑝 ∈ (1...𝑁)(𝐶𝑝) = (𝐴𝑝)))
4241necon3abid 2983 . . . . . . 7 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶𝐴 ↔ ¬ ∀𝑝 ∈ (1...𝑁)(𝐶𝑝) = (𝐴𝑝)))
43 df-ne 2947 . . . . . . . . 9 ((𝐶𝑝) ≠ (𝐴𝑝) ↔ ¬ (𝐶𝑝) = (𝐴𝑝))
4443rexbii 3100 . . . . . . . 8 (∃𝑝 ∈ (1...𝑁)(𝐶𝑝) ≠ (𝐴𝑝) ↔ ∃𝑝 ∈ (1...𝑁) ¬ (𝐶𝑝) = (𝐴𝑝))
45 rexnal 3106 . . . . . . . 8 (∃𝑝 ∈ (1...𝑁) ¬ (𝐶𝑝) = (𝐴𝑝) ↔ ¬ ∀𝑝 ∈ (1...𝑁)(𝐶𝑝) = (𝐴𝑝))
4644, 45bitr2i 276 . . . . . . 7 (¬ ∀𝑝 ∈ (1...𝑁)(𝐶𝑝) = (𝐴𝑝) ↔ ∃𝑝 ∈ (1...𝑁)(𝐶𝑝) ≠ (𝐴𝑝))
4742, 46bitrdi 287 . . . . . 6 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶𝐴 ↔ ∃𝑝 ∈ (1...𝑁)(𝐶𝑝) ≠ (𝐴𝑝)))
48 ralcom 3295 . . . . . . . 8 (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) ↔ ∀𝑗 ∈ (1...𝑁)∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))
49 fveq2 6922 . . . . . . . . . . . . . . 15 (𝑗 = 𝑝 → (𝐶𝑗) = (𝐶𝑝))
50 fveq2 6922 . . . . . . . . . . . . . . 15 (𝑗 = 𝑝 → (𝐴𝑗) = (𝐴𝑝))
5149, 50oveq12d 7468 . . . . . . . . . . . . . 14 (𝑗 = 𝑝 → ((𝐶𝑗) − (𝐴𝑗)) = ((𝐶𝑝) − (𝐴𝑝)))
5251oveq2d 7466 . . . . . . . . . . . . 13 (𝑗 = 𝑝 → (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))))
53 fveq2 6922 . . . . . . . . . . . . . . 15 (𝑗 = 𝑝 → (𝐵𝑗) = (𝐵𝑝))
5453, 50oveq12d 7468 . . . . . . . . . . . . . 14 (𝑗 = 𝑝 → ((𝐵𝑗) − (𝐴𝑗)) = ((𝐵𝑝) − (𝐴𝑝)))
5554oveq1d 7465 . . . . . . . . . . . . 13 (𝑗 = 𝑝 → (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))))
5652, 55eqeq12d 2756 . . . . . . . . . . . 12 (𝑗 = 𝑝 → ((((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) ↔ (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
5756ralbidv 3184 . . . . . . . . . . 11 (𝑗 = 𝑝 → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
5857rspcv 3631 . . . . . . . . . 10 (𝑝 ∈ (1...𝑁) → (∀𝑗 ∈ (1...𝑁)∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) → ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
5958ad2antrl 727 . . . . . . . . 9 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (1...𝑁) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (∀𝑗 ∈ (1...𝑁)∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) → ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
60 fveere 28936 . . . . . . . . . . . . . 14 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (1...𝑁)) → (𝐴𝑝) ∈ ℝ)
61603ad2antl1 1185 . . . . . . . . . . . . 13 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) → (𝐴𝑝) ∈ ℝ)
62 fveere 28936 . . . . . . . . . . . . . 14 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (1...𝑁)) → (𝐵𝑝) ∈ ℝ)
63623ad2antl2 1186 . . . . . . . . . . . . 13 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) → (𝐵𝑝) ∈ ℝ)
64 fveere 28936 . . . . . . . . . . . . . 14 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (1...𝑁)) → (𝐶𝑝) ∈ ℝ)
65643ad2antl3 1187 . . . . . . . . . . . . 13 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) → (𝐶𝑝) ∈ ℝ)
6661, 63, 653jca 1128 . . . . . . . . . . . 12 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) → ((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ))
6766anim1i 614 . . . . . . . . . . 11 ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)))
6867anasss 466 . . . . . . . . . 10 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (1...𝑁) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)))
69 fveecn 28937 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴𝑖) ∈ ℂ)
70693ad2antl1 1185 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴𝑖) ∈ ℂ)
71143ad2antl2 1186 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵𝑖) ∈ ℂ)
72153ad2antl3 1187 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶𝑖) ∈ ℂ)
7370, 71, 723jca 1128 . . . . . . . . . . . . . 14 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ))
7473adantlr 714 . . . . . . . . . . . . 13 ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ))
75 recn 11276 . . . . . . . . . . . . . . . 16 ((𝐴𝑝) ∈ ℝ → (𝐴𝑝) ∈ ℂ)
76 recn 11276 . . . . . . . . . . . . . . . 16 ((𝐵𝑝) ∈ ℝ → (𝐵𝑝) ∈ ℂ)
77 recn 11276 . . . . . . . . . . . . . . . 16 ((𝐶𝑝) ∈ ℝ → (𝐶𝑝) ∈ ℂ)
7875, 76, 773anim123i 1151 . . . . . . . . . . . . . . 15 (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) → ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ))
7978adantr 480 . . . . . . . . . . . . . 14 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ))
8079ad2antlr 726 . . . . . . . . . . . . 13 ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ))
81 simplrr 777 . . . . . . . . . . . . 13 ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶𝑝) ≠ (𝐴𝑝))
82 eqcom 2747 . . . . . . . . . . . . . 14 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) ↔ (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) = (𝐵𝑖))
83 simp12 1204 . . . . . . . . . . . . . . . 16 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐵𝑖) ∈ ℂ)
84 simp11 1203 . . . . . . . . . . . . . . . 16 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐴𝑖) ∈ ℂ)
85 simp22 1207 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐵𝑝) ∈ ℂ)
86 simp21 1206 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐴𝑝) ∈ ℂ)
8785, 86subcld 11649 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐵𝑝) − (𝐴𝑝)) ∈ ℂ)
88 simp23 1208 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐶𝑝) ∈ ℂ)
8988, 86subcld 11649 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐶𝑝) − (𝐴𝑝)) ∈ ℂ)
90 simpr3 1196 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ)) → (𝐶𝑝) ∈ ℂ)
91 simpr1 1194 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ)) → (𝐴𝑝) ∈ ℂ)
9290, 91subeq0ad 11659 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ)) → (((𝐶𝑝) − (𝐴𝑝)) = 0 ↔ (𝐶𝑝) = (𝐴𝑝)))
9392necon3bid 2991 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ)) → (((𝐶𝑝) − (𝐴𝑝)) ≠ 0 ↔ (𝐶𝑝) ≠ (𝐴𝑝)))
9493biimp3ar 1470 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐶𝑝) − (𝐴𝑝)) ≠ 0)
9587, 89, 94divcld 12072 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) ∈ ℂ)
96 simp13 1205 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐶𝑖) ∈ ℂ)
9796, 84subcld 11649 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐶𝑖) − (𝐴𝑖)) ∈ ℂ)
9895, 97mulcld 11312 . . . . . . . . . . . . . . . 16 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) ∈ ℂ)
99 subadd2 11542 . . . . . . . . . . . . . . . . 17 (((𝐵𝑖) ∈ ℂ ∧ (𝐴𝑖) ∈ ℂ ∧ ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) ∈ ℂ) → (((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) ↔ (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) = (𝐵𝑖)))
10099bicomd 223 . . . . . . . . . . . . . . . 16 (((𝐵𝑖) ∈ ℂ ∧ (𝐴𝑖) ∈ ℂ ∧ ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) ∈ ℂ) → ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) = (𝐵𝑖) ↔ ((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖)))))
10183, 84, 98, 100syl3anc 1371 . . . . . . . . . . . . . . 15 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) = (𝐵𝑖) ↔ ((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖)))))
10287, 97, 89, 94div23d 12109 . . . . . . . . . . . . . . . 16 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) = ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))))
103102eqeq2d 2751 . . . . . . . . . . . . . . 15 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) ↔ ((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖)))))
104 eqcom 2747 . . . . . . . . . . . . . . . 16 (((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) ↔ ((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) = ((𝐵𝑖) − (𝐴𝑖)))
10587, 97mulcld 11312 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) ∈ ℂ)
10683, 84subcld 11649 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐵𝑖) − (𝐴𝑖)) ∈ ℂ)
107105, 89, 106, 94divmuld 12094 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) = ((𝐵𝑖) − (𝐴𝑖)) ↔ (((𝐶𝑝) − (𝐴𝑝)) · ((𝐵𝑖) − (𝐴𝑖))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
10889, 106mulcomd 11313 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐶𝑝) − (𝐴𝑝)) · ((𝐵𝑖) − (𝐴𝑖))) = (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))))
109108eqeq1d 2742 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((((𝐶𝑝) − (𝐴𝑝)) · ((𝐵𝑖) − (𝐴𝑖))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) ↔ (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
110107, 109bitrd 279 . . . . . . . . . . . . . . . 16 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) = ((𝐵𝑖) − (𝐴𝑖)) ↔ (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
111104, 110bitrid 283 . . . . . . . . . . . . . . 15 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) ↔ (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
112101, 103, 1113bitr2d 307 . . . . . . . . . . . . . 14 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) = (𝐵𝑖) ↔ (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
11382, 112bitrid 283 . . . . . . . . . . . . 13 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) ↔ (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
11474, 80, 81, 113syl3anc 1371 . . . . . . . . . . . 12 ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) ↔ (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
115114ralbidva 3182 . . . . . . . . . . 11 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) ↔ ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
116 3simpb 1149 . . . . . . . . . . . 12 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)))
117 simpl2 1192 . . . . . . . . . . . . . 14 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐵𝑝) ∈ ℝ)
118 simpl1 1191 . . . . . . . . . . . . . 14 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐴𝑝) ∈ ℝ)
119117, 118resubcld 11720 . . . . . . . . . . . . 13 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐵𝑝) − (𝐴𝑝)) ∈ ℝ)
120 simpl3 1193 . . . . . . . . . . . . . 14 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐶𝑝) ∈ ℝ)
121120, 118resubcld 11720 . . . . . . . . . . . . 13 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐶𝑝) − (𝐴𝑝)) ∈ ℝ)
122 simp3 1138 . . . . . . . . . . . . . . . . 17 (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) → (𝐶𝑝) ∈ ℝ)
123122recnd 11320 . . . . . . . . . . . . . . . 16 (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) → (𝐶𝑝) ∈ ℂ)
124753ad2ant1 1133 . . . . . . . . . . . . . . . 16 (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) → (𝐴𝑝) ∈ ℂ)
125123, 124subeq0ad 11659 . . . . . . . . . . . . . . 15 (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) → (((𝐶𝑝) − (𝐴𝑝)) = 0 ↔ (𝐶𝑝) = (𝐴𝑝)))
126125necon3bid 2991 . . . . . . . . . . . . . 14 (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) → (((𝐶𝑝) − (𝐴𝑝)) ≠ 0 ↔ (𝐶𝑝) ≠ (𝐴𝑝)))
127126biimpar 477 . . . . . . . . . . . . 13 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐶𝑝) − (𝐴𝑝)) ≠ 0)
128119, 121, 127redivcld 12124 . . . . . . . . . . . 12 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) ∈ ℝ)
129 colinearalglem4 28944 . . . . . . . . . . . . 13 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)(((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))) ≤ 0))
130 oveq1 7457 . . . . . . . . . . . . . . . . . 18 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((𝐵𝑖) − (𝐴𝑖)) = ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)))
131130oveq1d 7465 . . . . . . . . . . . . . . . . 17 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) = (((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))))
132131breq1d 5176 . . . . . . . . . . . . . . . 16 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ↔ (((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
133132ralimi 3089 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ∀𝑖 ∈ (1...𝑁)((((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ↔ (((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
134 ralbi 3109 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)((((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ↔ (((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
135133, 134syl 17 . . . . . . . . . . . . . 14 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
136 oveq2 7458 . . . . . . . . . . . . . . . . . 18 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((𝐶𝑖) − (𝐵𝑖)) = ((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))))
137 oveq2 7458 . . . . . . . . . . . . . . . . . 18 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((𝐴𝑖) − (𝐵𝑖)) = ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))))
138136, 137oveq12d 7468 . . . . . . . . . . . . . . . . 17 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) = (((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))))
139138breq1d 5176 . . . . . . . . . . . . . . . 16 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ↔ (((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0))
140139ralimi 3089 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ∀𝑖 ∈ (1...𝑁)((((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ↔ (((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0))
141 ralbi 3109 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)((((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ↔ (((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0) → (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0))
142140, 141syl 17 . . . . . . . . . . . . . 14 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0))
143 oveq1 7457 . . . . . . . . . . . . . . . . . 18 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((𝐵𝑖) − (𝐶𝑖)) = ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖)))
144143oveq2d 7466 . . . . . . . . . . . . . . . . 17 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) = (((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))))
145144breq1d 5176 . . . . . . . . . . . . . . . 16 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ↔ (((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))) ≤ 0))
146145ralimi 3089 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ∀𝑖 ∈ (1...𝑁)((((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ↔ (((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))) ≤ 0))
147 ralbi 3109 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)((((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ↔ (((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))) ≤ 0) → (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))) ≤ 0))
148146, 147syl 17 . . . . . . . . . . . . . 14 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))) ≤ 0))
149135, 142, 1483orbi123d 1435 . . . . . . . . . . . . 13 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0) ↔ (∀𝑖 ∈ (1...𝑁)(((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))) ≤ 0)))
150129, 149syl5ibrcom 247 . . . . . . . . . . . 12 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0)))
151116, 128, 150syl2an 595 . . . . . . . . . . 11 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0)))
152115, 151sylbird 260 . . . . . . . . . 10 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0)))
15368, 152syldan 590 . . . . . . . . 9 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (1...𝑁) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0)))
15459, 153syld 47 . . . . . . . 8 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (1...𝑁) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (∀𝑗 ∈ (1...𝑁)∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0)))
15548, 154biimtrid 242 . . . . . . 7 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (1...𝑁) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0)))
156155rexlimdvaa 3162 . . . . . 6 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∃𝑝 ∈ (1...𝑁)(𝐶𝑝) ≠ (𝐴𝑝) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0))))
15747, 156sylbid 240 . . . . 5 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶𝐴 → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0))))
15837, 157pm2.61dne 3034 . . . 4 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0)))
159158pm4.71rd 562 . . 3 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) ↔ ((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
160 andir 1009 . . . . 5 (((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ↔ ((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
161160orbi1i 912 . . . 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 1088 . . . . . 6 ((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0) ↔ ((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0) ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0))
163162anbi1i 623 . . . . 5 (((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ↔ (((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0) ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))))
164 andir 1009 . . . . 5 ((((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0) ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ↔ (((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
165163, 164bitri 275 . . . 4 (((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ↔ (((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
166 df-3or 1088 . . . 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 303 . . 3 (((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0) ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ↔ ((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
168159, 167bitr2di 288 . 2 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (((∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))) ∨ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))))
16913, 168bitrd 279 1 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ((𝐴 Btwn ⟨𝐵, 𝐶⟩ ∨ 𝐵 Btwn ⟨𝐶, 𝐴⟩ ∨ 𝐶 Btwn ⟨𝐴, 𝐵⟩) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 846  w3o 1086  w3a 1087   = wceq 1537  wcel 2108  wne 2946  wral 3067  wrex 3076  cop 4654   class class class wbr 5166  cfv 6575  (class class class)co 7450  cc 11184  cr 11185  0cc0 11186  1c1 11187   + caddc 11189   · cmul 11191  cle 11327  cmin 11522   / cdiv 11949  ...cfz 13569  𝔼cee 28923   Btwn cbtwn 28924
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7772  ax-cnex 11242  ax-resscn 11243  ax-1cn 11244  ax-icn 11245  ax-addcl 11246  ax-addrcl 11247  ax-mulcl 11248  ax-mulrcl 11249  ax-mulcom 11250  ax-addass 11251  ax-mulass 11252  ax-distr 11253  ax-i2m1 11254  ax-1ne0 11255  ax-1rid 11256  ax-rnegex 11257  ax-rrecex 11258  ax-cnre 11259  ax-pre-lttri 11260  ax-pre-lttrn 11261  ax-pre-ltadd 11262  ax-pre-mulgt0 11263
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6334  df-ord 6400  df-on 6401  df-lim 6402  df-suc 6403  df-iota 6527  df-fun 6577  df-fn 6578  df-f 6579  df-f1 6580  df-fo 6581  df-f1o 6582  df-fv 6583  df-riota 7406  df-ov 7453  df-oprab 7454  df-mpo 7455  df-om 7906  df-1st 8032  df-2nd 8033  df-frecs 8324  df-wrecs 8355  df-recs 8429  df-rdg 8468  df-er 8765  df-map 8888  df-en 9006  df-dom 9007  df-sdom 9008  df-pnf 11328  df-mnf 11329  df-xr 11330  df-ltxr 11331  df-le 11332  df-sub 11524  df-neg 11525  df-div 11950  df-nn 12296  df-2 12358  df-n0 12556  df-z 12642  df-uz 12906  df-icc 13416  df-fz 13570  df-seq 14055  df-exp 14115  df-ee 28926  df-btwn 28927
This theorem is referenced by:  axlowdimlem6  28982
  Copyright terms: Public domain W3C validator