Metamath Proof Explorer

Theorem colinearalg

Description: An algebraic characterization of colinearity. Note the similarity to brbtwn2 . (Contributed by Scott Fenton, 24-Jun-2013)

Ref Expression
Assertion colinearalg ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 brbtwn2 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
2 brbtwn2 ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ) ) )
3 2 3comr ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ) ) )
4 colinearalglem3 ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
5 4 3comr ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
6 5 anbi2d ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ) = ( ( ( 𝐶 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
7 3 6 bitrd ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
8 brbtwn2 ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ) = ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ) ) )
9 colinearalglem2 ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ) = ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
10 9 anbi2d ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ) = ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
11 8 10 bitrd ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
12 11 3coml ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
13 1 7 12 3orbi123d ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ∨ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ∨ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) )
14 fveecn ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℂ )
15 fveecn ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑖 ) ∈ ℂ )
16 subid ⊢ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ → ( ( 𝐶 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) = 0 )
17 16 oveq2d ⊢ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ → ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) = ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · 0 ) )
18 17 adantl ⊢ ( ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) → ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) = ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · 0 ) )
19 subcl ⊢ ( ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) → ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ∈ ℂ )
20 19 mul01d ⊢ ( ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) → ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · 0 ) = 0 )
21 18 20 eqtrd ⊢ ( ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) → ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) = 0 )
22 14 15 21 syl2an ⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) ) → ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) = 0 )
23 22 anandirs ⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) = 0 )
24 0le0 ⊢ 0 ≤ 0
25 23 24 eqbrtrdi ⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 )
26 25 ralrimiva ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 )
27 26 3adant1 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 )
28 fveq1 ⊢ ( 𝐶 = 𝐴 → ( 𝐶 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑖 ) )
29 28 oveq2d ⊢ ( 𝐶 = 𝐴 → ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) )
30 28 oveq2d ⊢ ( 𝐶 = 𝐴 → ( ( 𝐶 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) = ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) )
31 29 30 oveq12d ⊢ ( 𝐶 = 𝐴 → ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) = ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
32 31 breq1d ⊢ ( 𝐶 = 𝐴 → ( ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ↔ ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ) )
33 32 ralbidv ⊢ ( 𝐶 = 𝐴 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ) )
34 27 33 syl5ibcom ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐶 = 𝐴 → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ) )
35 3mix1 ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) )
36 34 35 syl6 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐶 = 𝐴 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ) )
37 36 a1dd ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐶 = 𝐴 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ) ) )
38 simp3 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
39 simp1 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
40 eqeefv ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐶 = 𝐴 ↔ ∀ 𝑝 ∈ ( 1 ... 𝑁 ) ( 𝐶 ‘ 𝑝 ) = ( 𝐴 ‘ 𝑝 ) ) )
41 38 39 40 syl2anc ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐶 = 𝐴 ↔ ∀ 𝑝 ∈ ( 1 ... 𝑁 ) ( 𝐶 ‘ 𝑝 ) = ( 𝐴 ‘ 𝑝 ) ) )
42 41 necon3abid ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐶 ≠ 𝐴 ↔ ¬ ∀ 𝑝 ∈ ( 1 ... 𝑁 ) ( 𝐶 ‘ 𝑝 ) = ( 𝐴 ‘ 𝑝 ) ) )
43 df-ne ⊢ ( ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ↔ ¬ ( 𝐶 ‘ 𝑝 ) = ( 𝐴 ‘ 𝑝 ) )
44 43 rexbii ⊢ ( ∃ 𝑝 ∈ ( 1 ... 𝑁 ) ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ↔ ∃ 𝑝 ∈ ( 1 ... 𝑁 ) ¬ ( 𝐶 ‘ 𝑝 ) = ( 𝐴 ‘ 𝑝 ) )
45 rexnal ⊢ ( ∃ 𝑝 ∈ ( 1 ... 𝑁 ) ¬ ( 𝐶 ‘ 𝑝 ) = ( 𝐴 ‘ 𝑝 ) ↔ ¬ ∀ 𝑝 ∈ ( 1 ... 𝑁 ) ( 𝐶 ‘ 𝑝 ) = ( 𝐴 ‘ 𝑝 ) )
46 44 45 bitr2i ⊢ ( ¬ ∀ 𝑝 ∈ ( 1 ... 𝑁 ) ( 𝐶 ‘ 𝑝 ) = ( 𝐴 ‘ 𝑝 ) ↔ ∃ 𝑝 ∈ ( 1 ... 𝑁 ) ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) )
47 42 46 bitrdi ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐶 ≠ 𝐴 ↔ ∃ 𝑝 ∈ ( 1 ... 𝑁 ) ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) )
48 ralcom ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ↔ ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
49 fveq2 ⊢ ( 𝑗 = 𝑝 → ( 𝐶 ‘ 𝑗 ) = ( 𝐶 ‘ 𝑝 ) )
50 fveq2 ⊢ ( 𝑗 = 𝑝 → ( 𝐴 ‘ 𝑗 ) = ( 𝐴 ‘ 𝑝 ) )
51 49 50 oveq12d ⊢ ( 𝑗 = 𝑝 → ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) )
52 51 oveq2d ⊢ ( 𝑗 = 𝑝 → ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) )
53 fveq2 ⊢ ( 𝑗 = 𝑝 → ( 𝐵 ‘ 𝑗 ) = ( 𝐵 ‘ 𝑝 ) )
54 53 50 oveq12d ⊢ ( 𝑗 = 𝑝 → ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) )
55 54 oveq1d ⊢ ( 𝑗 = 𝑝 → ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
56 52 55 eqeq12d ⊢ ( 𝑗 = 𝑝 → ( ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ↔ ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
57 56 ralbidv ⊢ ( 𝑗 = 𝑝 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
58 57 rspcv ⊢ ( 𝑝 ∈ ( 1 ... 𝑁 ) → ( ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
59 58 ad2antrl ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 1 ... 𝑁 ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) ) → ( ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
60 fveere ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑝 ) ∈ ℝ )
61 60 3ad2antl1 ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑝 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑝 ) ∈ ℝ )
62 fveere ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑝 ) ∈ ℝ )
63 62 3ad2antl2 ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑝 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑝 ) ∈ ℝ )
64 fveere ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑝 ) ∈ ℝ )
65 64 3ad2antl3 ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑝 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑝 ) ∈ ℝ )
66 61 63 65 3jca ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑝 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) )
67 66 anim1i ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑝 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) )
68 67 anasss ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 1 ... 𝑁 ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) ) → ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) )
69 fveecn ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
70 69 3ad2antl1 ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
71 14 3ad2antl2 ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℂ )
72 15 3ad2antl3 ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑖 ) ∈ ℂ )
73 70 71 72 3jca ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) )
74 73 adantlr ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) )
75 recn ⊢ ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ → ( 𝐴 ‘ 𝑝 ) ∈ ℂ )
76 recn ⊢ ( ( 𝐵 ‘ 𝑝 ) ∈ ℝ → ( 𝐵 ‘ 𝑝 ) ∈ ℂ )
77 recn ⊢ ( ( 𝐶 ‘ 𝑝 ) ∈ ℝ → ( 𝐶 ‘ 𝑝 ) ∈ ℂ )
78 75 76 77 3anim123i ⊢ ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) → ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) )
79 78 adantr ⊢ ( ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) )
80 79 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) )
81 simplrr ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) )
82 eqcom ⊢ ( ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ↔ ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) = ( 𝐵 ‘ 𝑖 ) )
83 simp12 ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℂ )
84 simp11 ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
85 simp22 ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( 𝐵 ‘ 𝑝 ) ∈ ℂ )
86 simp21 ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( 𝐴 ‘ 𝑝 ) ∈ ℂ )
87 85 86 subcld ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ∈ ℂ )
88 simp23 ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( 𝐶 ‘ 𝑝 ) ∈ ℂ )
89 88 86 subcld ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ∈ ℂ )
90 simpr3 ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ) → ( 𝐶 ‘ 𝑝 ) ∈ ℂ )
91 simpr1 ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ) → ( 𝐴 ‘ 𝑝 ) ∈ ℂ )
92 90 91 subeq0ad ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ) → ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) = 0 ↔ ( 𝐶 ‘ 𝑝 ) = ( 𝐴 ‘ 𝑝 ) ) )
93 92 necon3bid ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ) → ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ≠ 0 ↔ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) )
94 93 biimp3ar ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ≠ 0 )
95 87 89 94 divcld ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) ∈ ℂ )
96 simp13 ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( 𝐶 ‘ 𝑖 ) ∈ ℂ )
97 96 84 subcld ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ∈ ℂ )
98 95 97 mulcld ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ∈ ℂ )
99 subadd2 ⊢ ( ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ∈ ℂ ) → ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) = ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ↔ ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) = ( 𝐵 ‘ 𝑖 ) ) )
100 99 bicomd ⊢ ( ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ∈ ℂ ) → ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) = ( 𝐵 ‘ 𝑖 ) ↔ ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) = ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
101 83 84 98 100 syl3anc ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) = ( 𝐵 ‘ 𝑖 ) ↔ ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) = ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
102 87 97 89 94 div23d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
103 102 eqeq2d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) = ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) ↔ ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) = ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
104 eqcom ⊢ ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) = ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) ↔ ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) )
105 87 97 mulcld ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ∈ ℂ )
106 83 84 subcld ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ∈ ℂ )
107 105 89 106 94 divmuld ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↔ ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
108 89 106 mulcomd ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) = ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) )
109 108 eqeq1d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ↔ ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
110 107 109 bitrd ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ↔ ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
111 104 110 syl5bb ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) = ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) ↔ ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
112 101 103 111 3bitr2d ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) = ( 𝐵 ‘ 𝑖 ) ↔ ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
113 82 112 syl5bb ⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ↔ ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
114 74 80 81 113 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ↔ ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
115 114 ralbidva ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
116 3simpb ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) )
117 simpl2 ⊢ ( ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( 𝐵 ‘ 𝑝 ) ∈ ℝ )
118 simpl1 ⊢ ( ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( 𝐴 ‘ 𝑝 ) ∈ ℝ )
119 117 118 resubcld ⊢ ( ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ∈ ℝ )
120 simpl3 ⊢ ( ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( 𝐶 ‘ 𝑝 ) ∈ ℝ )
121 120 118 resubcld ⊢ ( ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ∈ ℝ )
122 simp3 ⊢ ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) → ( 𝐶 ‘ 𝑝 ) ∈ ℝ )
123 122 recnd ⊢ ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) → ( 𝐶 ‘ 𝑝 ) ∈ ℂ )
124 75 3ad2ant1 ⊢ ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) → ( 𝐴 ‘ 𝑝 ) ∈ ℂ )
125 123 124 subeq0ad ⊢ ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) → ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) = 0 ↔ ( 𝐶 ‘ 𝑝 ) = ( 𝐴 ‘ 𝑝 ) ) )
126 125 necon3bid ⊢ ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) → ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ≠ 0 ↔ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) )
127 126 biimpar ⊢ ( ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ≠ 0 )
128 119 121 127 redivcld ⊢ ( ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) ∈ ℝ )
129 colinearalglem4 ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) ∈ ℝ ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) )
130 oveq1 ⊢ ( ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) = ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) − ( 𝐴 ‘ 𝑖 ) ) )
131 130 oveq1d ⊢ ( ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) = ( ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) )
132 131 breq1d ⊢ ( ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ( ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ↔ ( ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ) )
133 132 ralimi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ↔ ( ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ) )
134 ralbi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ↔ ( ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ) )
135 133 134 syl ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ) )
136 oveq2 ⊢ ( ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) = ( ( 𝐶 ‘ 𝑖 ) − ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ) )
137 oveq2 ⊢ ( ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) = ( ( 𝐴 ‘ 𝑖 ) − ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ) )
138 136 137 oveq12d ⊢ ( ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 𝐶 ‘ 𝑖 ) − ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ) ) )
139 138 breq1d ⊢ ( ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ( ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ↔ ( ( ( 𝐶 ‘ 𝑖 ) − ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ) ) ≤ 0 ) )
140 139 ralimi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ↔ ( ( ( 𝐶 ‘ 𝑖 ) − ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ) ) ≤ 0 ) )
141 ralbi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ↔ ( ( ( 𝐶 ‘ 𝑖 ) − ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ) ) ≤ 0 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ) ) ≤ 0 ) )
142 140 141 syl ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ) ) ≤ 0 ) )
143 oveq1 ⊢ ( ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) = ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) − ( 𝐶 ‘ 𝑖 ) ) )
144 143 oveq2d ⊢ ( ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) = ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) − ( 𝐶 ‘ 𝑖 ) ) ) )
145 144 breq1d ⊢ ( ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ( ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ↔ ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) )
146 145 ralimi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ↔ ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) )
147 ralbi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ↔ ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) )
148 146 147 syl ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) )
149 135 142 148 3orbi123d ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ) )
150 129 149 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) ∈ ℝ ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ) )
151 116 128 150 syl2an ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ) )
152 115 151 sylbird ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( ( 𝐴 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℝ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ) )
153 68 152 syldan ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 1 ... 𝑁 ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ) )
154 59 153 syld ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 1 ... 𝑁 ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) ) → ( ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ) )
155 48 154 syl5bi ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 1 ... 𝑁 ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ) )
156 155 rexlimdvaa ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ∃ 𝑝 ∈ ( 1 ... 𝑁 ) ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ) ) )
157 47 156 sylbid ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐶 ≠ 𝐴 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ) ) )
158 37 157 pm2.61dne ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ) )
159 158 pm4.71rd ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ↔ ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
160 andir ⊢ ( ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ∨ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
161 160 orbi1i ⊢ ( ( ( ( ∀ 𝑖 ∈ ( 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 ⊢ ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ↔ ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) )
163 162 anbi1i ⊢ ( ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ( ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
164 andir ⊢ ( ( ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ( ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ∨ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
165 163 164 bitri ⊢ ( ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ( ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ∨ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
166 df-3or ⊢ ( ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ∨ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ∨ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ) ↔ ( ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ∨ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ) ∨ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
167 161 165 166 3bitr4i ⊢ ( ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ∨ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ∨ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
168 159 167 bitr2di ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ∨ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ∨ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) · ( ( 𝐵 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ≤ 0 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
169 13 168 bitrd ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )