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

Theorem colinearalg 28934
Description: An algebraic characterization of colinearity. Note the similarity to brbtwn2 28929. (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 28929 . . 3 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴 Btwn ⟨𝐵, 𝐶⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))))
2 brbtwn2 28929 . . . . 5 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝐵 Btwn ⟨𝐶, 𝐴⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑗) − (𝐵𝑗))) = (((𝐶𝑗) − (𝐵𝑗)) · ((𝐴𝑖) − (𝐵𝑖))))))
323comr 1125 . . . 4 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐵 Btwn ⟨𝐶, 𝐴⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑗) − (𝐵𝑗))) = (((𝐶𝑗) − (𝐵𝑗)) · ((𝐴𝑖) − (𝐵𝑖))))))
4 colinearalglem3 28932 . . . . . 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 28929 . . . . 5 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝐶 Btwn ⟨𝐴, 𝐵⟩ ↔ (∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ∧ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑗) − (𝐶𝑗))) = (((𝐴𝑗) − (𝐶𝑗)) · ((𝐵𝑖) − (𝐶𝑖))))))
9 colinearalglem2 28931 . . . . . 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 28926 . . . . . . . . . . . . 13 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵𝑖) ∈ ℂ)
15 fveecn 28926 . . . . . . . . . . . . 13 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶𝑖) ∈ ℂ)
16 subid 11551 . . . . . . . . . . . . . . . 16 ((𝐶𝑖) ∈ ℂ → ((𝐶𝑖) − (𝐶𝑖)) = 0)
1716oveq2d 7461 . . . . . . . . . . . . . . 15 ((𝐶𝑖) ∈ ℂ → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) = (((𝐵𝑖) − (𝐶𝑖)) · 0))
1817adantl 481 . . . . . . . . . . . . . 14 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) = (((𝐵𝑖) − (𝐶𝑖)) · 0))
19 subcl 11531 . . . . . . . . . . . . . . 15 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) → ((𝐵𝑖) − (𝐶𝑖)) ∈ ℂ)
2019mul01d 11485 . . . . . . . . . . . . . 14 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) → (((𝐵𝑖) − (𝐶𝑖)) · 0) = 0)
2118, 20eqtrd 2774 . . . . . . . . . . . . 13 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) = 0)
2214, 15, 21syl2an 595 . . . . . . . . . . . 12 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁))) → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) = 0)
2322anandirs 678 . . . . . . . . . . 11 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) = 0)
24 0le0 12390 . . . . . . . . . . 11 0 ≤ 0
2523, 24eqbrtrdi 5208 . . . . . . . . . 10 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) ≤ 0)
2625ralrimiva 3148 . . . . . . . . 9 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) ≤ 0)
27263adant1 1130 . . . . . . . 8 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) ≤ 0)
28 fveq1 6918 . . . . . . . . . . . 12 (𝐶 = 𝐴 → (𝐶𝑖) = (𝐴𝑖))
2928oveq2d 7461 . . . . . . . . . . 11 (𝐶 = 𝐴 → ((𝐵𝑖) − (𝐶𝑖)) = ((𝐵𝑖) − (𝐴𝑖)))
3028oveq2d 7461 . . . . . . . . . . 11 (𝐶 = 𝐴 → ((𝐶𝑖) − (𝐶𝑖)) = ((𝐶𝑖) − (𝐴𝑖)))
3129, 30oveq12d 7463 . . . . . . . . . 10 (𝐶 = 𝐴 → (((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) = (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))))
3231breq1d 5179 . . . . . . . . 9 (𝐶 = 𝐴 → ((((𝐵𝑖) − (𝐶𝑖)) · ((𝐶𝑖) − (𝐶𝑖))) ≤ 0 ↔ (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
3332ralbidv 3180 . . . . . . . 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 28927 . . . . . . . . 9 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝐶 = 𝐴 ↔ ∀𝑝 ∈ (1...𝑁)(𝐶𝑝) = (𝐴𝑝)))
4138, 39, 40syl2anc 583 . . . . . . . 8 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶 = 𝐴 ↔ ∀𝑝 ∈ (1...𝑁)(𝐶𝑝) = (𝐴𝑝)))
4241necon3abid 2979 . . . . . . 7 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶𝐴 ↔ ¬ ∀𝑝 ∈ (1...𝑁)(𝐶𝑝) = (𝐴𝑝)))
43 df-ne 2943 . . . . . . . . 9 ((𝐶𝑝) ≠ (𝐴𝑝) ↔ ¬ (𝐶𝑝) = (𝐴𝑝))
4443rexbii 3096 . . . . . . . 8 (∃𝑝 ∈ (1...𝑁)(𝐶𝑝) ≠ (𝐴𝑝) ↔ ∃𝑝 ∈ (1...𝑁) ¬ (𝐶𝑝) = (𝐴𝑝))
45 rexnal 3102 . . . . . . . 8 (∃𝑝 ∈ (1...𝑁) ¬ (𝐶𝑝) = (𝐴𝑝) ↔ ¬ ∀𝑝 ∈ (1...𝑁)(𝐶𝑝) = (𝐴𝑝))
4644, 45bitr2i 276 . . . . . . 7 (¬ ∀𝑝 ∈ (1...𝑁)(𝐶𝑝) = (𝐴𝑝) ↔ ∃𝑝 ∈ (1...𝑁)(𝐶𝑝) ≠ (𝐴𝑝))
4742, 46bitrdi 287 . . . . . 6 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐶𝐴 ↔ ∃𝑝 ∈ (1...𝑁)(𝐶𝑝) ≠ (𝐴𝑝)))
48 ralcom 3290 . . . . . . . 8 (∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) ↔ ∀𝑗 ∈ (1...𝑁)∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))))
49 fveq2 6919 . . . . . . . . . . . . . . 15 (𝑗 = 𝑝 → (𝐶𝑗) = (𝐶𝑝))
50 fveq2 6919 . . . . . . . . . . . . . . 15 (𝑗 = 𝑝 → (𝐴𝑗) = (𝐴𝑝))
5149, 50oveq12d 7463 . . . . . . . . . . . . . 14 (𝑗 = 𝑝 → ((𝐶𝑗) − (𝐴𝑗)) = ((𝐶𝑝) − (𝐴𝑝)))
5251oveq2d 7461 . . . . . . . . . . . . 13 (𝑗 = 𝑝 → (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))))
53 fveq2 6919 . . . . . . . . . . . . . . 15 (𝑗 = 𝑝 → (𝐵𝑗) = (𝐵𝑝))
5453, 50oveq12d 7463 . . . . . . . . . . . . . 14 (𝑗 = 𝑝 → ((𝐵𝑗) − (𝐴𝑗)) = ((𝐵𝑝) − (𝐴𝑝)))
5554oveq1d 7460 . . . . . . . . . . . . 13 (𝑗 = 𝑝 → (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))))
5652, 55eqeq12d 2750 . . . . . . . . . . . 12 (𝑗 = 𝑝 → ((((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) ↔ (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
5756ralbidv 3180 . . . . . . . . . . 11 (𝑗 = 𝑝 → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
5857rspcv 3627 . . . . . . . . . 10 (𝑝 ∈ (1...𝑁) → (∀𝑗 ∈ (1...𝑁)∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) → ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
5958ad2antrl 727 . . . . . . . . 9 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (1...𝑁) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (∀𝑗 ∈ (1...𝑁)∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑗) − (𝐴𝑗))) = (((𝐵𝑗) − (𝐴𝑗)) · ((𝐶𝑖) − (𝐴𝑖))) → ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
60 fveere 28925 . . . . . . . . . . . . . 14 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (1...𝑁)) → (𝐴𝑝) ∈ ℝ)
61603ad2antl1 1185 . . . . . . . . . . . . 13 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) → (𝐴𝑝) ∈ ℝ)
62 fveere 28925 . . . . . . . . . . . . . 14 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (1...𝑁)) → (𝐵𝑝) ∈ ℝ)
63623ad2antl2 1186 . . . . . . . . . . . . 13 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) → (𝐵𝑝) ∈ ℝ)
64 fveere 28925 . . . . . . . . . . . . . 14 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (1...𝑁)) → (𝐶𝑝) ∈ ℝ)
65643ad2antl3 1187 . . . . . . . . . . . . 13 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) → (𝐶𝑝) ∈ ℝ)
6661, 63, 653jca 1128 . . . . . . . . . . . 12 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) → ((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ))
6766anim1i 614 . . . . . . . . . . 11 ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ 𝑝 ∈ (1...𝑁)) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)))
6867anasss 466 . . . . . . . . . 10 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑝 ∈ (1...𝑁) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)))
69 fveecn 28926 . . . . . . . . . . . . . . . 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 11270 . . . . . . . . . . . . . . . 16 ((𝐴𝑝) ∈ ℝ → (𝐴𝑝) ∈ ℂ)
76 recn 11270 . . . . . . . . . . . . . . . 16 ((𝐵𝑝) ∈ ℝ → (𝐵𝑝) ∈ ℂ)
77 recn 11270 . . . . . . . . . . . . . . . 16 ((𝐶𝑝) ∈ ℝ → (𝐶𝑝) ∈ ℂ)
7875, 76, 773anim123i 1151 . . . . . . . . . . . . . . 15 (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) → ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ))
7978adantr 480 . . . . . . . . . . . . . 14 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ))
8079ad2antlr 726 . . . . . . . . . . . . 13 ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ))
81 simplrr 777 . . . . . . . . . . . . 13 ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶𝑝) ≠ (𝐴𝑝))
82 eqcom 2741 . . . . . . . . . . . . . 14 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) ↔ (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) = (𝐵𝑖))
83 simp12 1204 . . . . . . . . . . . . . . . 16 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐵𝑖) ∈ ℂ)
84 simp11 1203 . . . . . . . . . . . . . . . 16 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐴𝑖) ∈ ℂ)
85 simp22 1207 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐵𝑝) ∈ ℂ)
86 simp21 1206 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐴𝑝) ∈ ℂ)
8785, 86subcld 11643 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐵𝑝) − (𝐴𝑝)) ∈ ℂ)
88 simp23 1208 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐶𝑝) ∈ ℂ)
8988, 86subcld 11643 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐶𝑝) − (𝐴𝑝)) ∈ ℂ)
90 simpr3 1196 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ)) → (𝐶𝑝) ∈ ℂ)
91 simpr1 1194 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ)) → (𝐴𝑝) ∈ ℂ)
9290, 91subeq0ad 11653 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ)) → (((𝐶𝑝) − (𝐴𝑝)) = 0 ↔ (𝐶𝑝) = (𝐴𝑝)))
9392necon3bid 2987 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ)) → (((𝐶𝑝) − (𝐴𝑝)) ≠ 0 ↔ (𝐶𝑝) ≠ (𝐴𝑝)))
9493biimp3ar 1470 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐶𝑝) − (𝐴𝑝)) ≠ 0)
9587, 89, 94divcld 12066 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) ∈ ℂ)
96 simp13 1205 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐶𝑖) ∈ ℂ)
9796, 84subcld 11643 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐶𝑖) − (𝐴𝑖)) ∈ ℂ)
9895, 97mulcld 11306 . . . . . . . . . . . . . . . 16 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) ∈ ℂ)
99 subadd2 11536 . . . . . . . . . . . . . . . . 17 (((𝐵𝑖) ∈ ℂ ∧ (𝐴𝑖) ∈ ℂ ∧ ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) ∈ ℂ) → (((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) ↔ (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) = (𝐵𝑖)))
10099bicomd 223 . . . . . . . . . . . . . . . 16 (((𝐵𝑖) ∈ ℂ ∧ (𝐴𝑖) ∈ ℂ ∧ ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) ∈ ℂ) → ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) = (𝐵𝑖) ↔ ((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖)))))
10183, 84, 98, 100syl3anc 1371 . . . . . . . . . . . . . . 15 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) = (𝐵𝑖) ↔ ((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖)))))
10287, 97, 89, 94div23d 12103 . . . . . . . . . . . . . . . 16 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) = ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))))
103102eqeq2d 2745 . . . . . . . . . . . . . . 15 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) ↔ ((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖)))))
104 eqcom 2741 . . . . . . . . . . . . . . . 16 (((𝐵𝑖) − (𝐴𝑖)) = ((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) ↔ ((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) = ((𝐵𝑖) − (𝐴𝑖)))
10587, 97mulcld 11306 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) ∈ ℂ)
10683, 84subcld 11643 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐵𝑖) − (𝐴𝑖)) ∈ ℂ)
107105, 89, 106, 94divmuld 12088 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖))) / ((𝐶𝑝) − (𝐴𝑝))) = ((𝐵𝑖) − (𝐴𝑖)) ↔ (((𝐶𝑝) − (𝐴𝑝)) · ((𝐵𝑖) − (𝐴𝑖))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
10889, 106mulcomd 11307 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑖) ∈ ℂ ∧ (𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ) ∧ ((𝐴𝑝) ∈ ℂ ∧ (𝐵𝑝) ∈ ℂ ∧ (𝐶𝑝) ∈ ℂ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐶𝑝) − (𝐴𝑝)) · ((𝐵𝑖) − (𝐴𝑖))) = (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))))
109108eqeq1d 2736 . . . . . . . . . . . . . . . . 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 3178 . . . . . . . . . . 11 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝))) → (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) ↔ ∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑝) − (𝐴𝑝))) = (((𝐵𝑝) − (𝐴𝑝)) · ((𝐶𝑖) − (𝐴𝑖)))))
116 3simpb 1149 . . . . . . . . . . . 12 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)))
117 simpl2 1192 . . . . . . . . . . . . . 14 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐵𝑝) ∈ ℝ)
118 simpl1 1191 . . . . . . . . . . . . . 14 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐴𝑝) ∈ ℝ)
119117, 118resubcld 11714 . . . . . . . . . . . . 13 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐵𝑝) − (𝐴𝑝)) ∈ ℝ)
120 simpl3 1193 . . . . . . . . . . . . . 14 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (𝐶𝑝) ∈ ℝ)
121120, 118resubcld 11714 . . . . . . . . . . . . 13 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐶𝑝) − (𝐴𝑝)) ∈ ℝ)
122 simp3 1138 . . . . . . . . . . . . . . . . 17 (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) → (𝐶𝑝) ∈ ℝ)
123122recnd 11314 . . . . . . . . . . . . . . . 16 (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) → (𝐶𝑝) ∈ ℂ)
124753ad2ant1 1133 . . . . . . . . . . . . . . . 16 (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) → (𝐴𝑝) ∈ ℂ)
125123, 124subeq0ad 11653 . . . . . . . . . . . . . . 15 (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) → (((𝐶𝑝) − (𝐴𝑝)) = 0 ↔ (𝐶𝑝) = (𝐴𝑝)))
126125necon3bid 2987 . . . . . . . . . . . . . 14 (((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) → (((𝐶𝑝) − (𝐴𝑝)) ≠ 0 ↔ (𝐶𝑝) ≠ (𝐴𝑝)))
127126biimpar 477 . . . . . . . . . . . . 13 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → ((𝐶𝑝) − (𝐴𝑝)) ≠ 0)
128119, 121, 127redivcld 12118 . . . . . . . . . . . 12 ((((𝐴𝑝) ∈ ℝ ∧ (𝐵𝑝) ∈ ℝ ∧ (𝐶𝑝) ∈ ℝ) ∧ (𝐶𝑝) ≠ (𝐴𝑝)) → (((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) ∈ ℝ)
129 colinearalglem4 28933 . . . . . . . . . . . . 13 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)(((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0 ∨ ∀𝑖 ∈ (1...𝑁)(((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))) ≤ 0))
130 oveq1 7452 . . . . . . . . . . . . . . . . . 18 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((𝐵𝑖) − (𝐴𝑖)) = ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)))
131130oveq1d 7460 . . . . . . . . . . . . . . . . 17 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) = (((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))))
132131breq1d 5179 . . . . . . . . . . . . . . . 16 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ↔ (((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
133132ralimi 3085 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ∀𝑖 ∈ (1...𝑁)((((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ↔ (((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
134 ralbi 3105 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)((((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ↔ (((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
135133, 134syl 17 . . . . . . . . . . . . . 14 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (∀𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐴𝑖)) · ((𝐶𝑖) − (𝐴𝑖))) ≤ 0))
136 oveq2 7453 . . . . . . . . . . . . . . . . . 18 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((𝐶𝑖) − (𝐵𝑖)) = ((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))))
137 oveq2 7453 . . . . . . . . . . . . . . . . . 18 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((𝐴𝑖) − (𝐵𝑖)) = ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))))
138136, 137oveq12d 7463 . . . . . . . . . . . . . . . . 17 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) = (((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))))
139138breq1d 5179 . . . . . . . . . . . . . . . 16 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ↔ (((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0))
140139ralimi 3085 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ∀𝑖 ∈ (1...𝑁)((((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ↔ (((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0))
141 ralbi 3105 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)((((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ↔ (((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0) → (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0))
142140, 141syl 17 . . . . . . . . . . . . . 14 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐵𝑖)) · ((𝐴𝑖) − (𝐵𝑖))) ≤ 0 ↔ ∀𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖))) · ((𝐴𝑖) − (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)))) ≤ 0))
143 oveq1 7452 . . . . . . . . . . . . . . . . . 18 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((𝐵𝑖) − (𝐶𝑖)) = ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖)))
144143oveq2d 7461 . . . . . . . . . . . . . . . . 17 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → (((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) = (((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))))
145144breq1d 5179 . . . . . . . . . . . . . . . 16 ((𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ((((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ↔ (((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))) ≤ 0))
146145ralimi 3085 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) → ∀𝑖 ∈ (1...𝑁)((((𝐴𝑖) − (𝐶𝑖)) · ((𝐵𝑖) − (𝐶𝑖))) ≤ 0 ↔ (((𝐴𝑖) − (𝐶𝑖)) · ((((((𝐵𝑝) − (𝐴𝑝)) / ((𝐶𝑝) − (𝐴𝑝))) · ((𝐶𝑖) − (𝐴𝑖))) + (𝐴𝑖)) − (𝐶𝑖))) ≤ 0))
147 ralbi 3105 . . . . . . . . . . . . . . 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 3158 . . . . . 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 3030 . . . 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 2103  wne 2942  wral 3063  wrex 3072  cop 4654   class class class wbr 5169  cfv 6572  (class class class)co 7445  cc 11178  cr 11179  0cc0 11180  1c1 11181   + caddc 11183   · cmul 11185  cle 11321  cmin 11516   / cdiv 11943  ...cfz 13563  𝔼cee 28912   Btwn cbtwn 28913
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 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705  ax-sep 5320  ax-nul 5327  ax-pow 5386  ax-pr 5450  ax-un 7766  ax-cnex 11236  ax-resscn 11237  ax-1cn 11238  ax-icn 11239  ax-addcl 11240  ax-addrcl 11241  ax-mulcl 11242  ax-mulrcl 11243  ax-mulcom 11244  ax-addass 11245  ax-mulass 11246  ax-distr 11247  ax-i2m1 11248  ax-1ne0 11249  ax-1rid 11250  ax-rnegex 11251  ax-rrecex 11252  ax-cnre 11253  ax-pre-lttri 11254  ax-pre-lttrn 11255  ax-pre-ltadd 11256  ax-pre-mulgt0 11257
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 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3383  df-reu 3384  df-rab 3439  df-v 3484  df-sbc 3799  df-csb 3916  df-dif 3973  df-un 3975  df-in 3977  df-ss 3987  df-pss 3990  df-nul 4348  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5021  df-br 5170  df-opab 5232  df-mpt 5253  df-tr 5287  df-id 5597  df-eprel 5603  df-po 5611  df-so 5612  df-fr 5654  df-we 5656  df-xp 5705  df-rel 5706  df-cnv 5707  df-co 5708  df-dm 5709  df-rn 5710  df-res 5711  df-ima 5712  df-pred 6331  df-ord 6397  df-on 6398  df-lim 6399  df-suc 6400  df-iota 6524  df-fun 6574  df-fn 6575  df-f 6576  df-f1 6577  df-fo 6578  df-f1o 6579  df-fv 6580  df-riota 7401  df-ov 7448  df-oprab 7449  df-mpo 7450  df-om 7900  df-1st 8026  df-2nd 8027  df-frecs 8318  df-wrecs 8349  df-recs 8423  df-rdg 8462  df-er 8759  df-map 8882  df-en 9000  df-dom 9001  df-sdom 9002  df-pnf 11322  df-mnf 11323  df-xr 11324  df-ltxr 11325  df-le 11326  df-sub 11518  df-neg 11519  df-div 11944  df-nn 12290  df-2 12352  df-n0 12550  df-z 12636  df-uz 12900  df-icc 13410  df-fz 13564  df-seq 14049  df-exp 14109  df-ee 28915  df-btwn 28916
This theorem is referenced by:  axlowdimlem6  28971
  Copyright terms: Public domain W3C validator