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	bitrid	⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) = ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) ↔ ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
112	101 103 111	3bitr2d	⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) = ( 𝐵 ‘ 𝑖 ) ↔ ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
113	82 112	bitrid	⊢ ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐴 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑝 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑝 ) ∈ ℂ ) ∧ ( 𝐶 ‘ 𝑝 ) ≠ ( 𝐴 ‘ 𝑝 ) ) → ( ( 𝐵 ‘ 𝑖 ) = ( ( ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) / ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐴 ‘ 𝑖 ) ) ↔ ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) ) = ( ( ( 𝐵 ‘ 𝑝 ) − ( 𝐴 ‘ 𝑝 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )
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	biimtrid	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑝 ∈ ( 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 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) · ( ( 𝐶 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) ) = ( ( ( 𝐵 ‘ 𝑗 ) − ( 𝐴 ‘ 𝑗 ) ) · ( ( 𝐶 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑖 ) ) ) ) )