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 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Btwn B C ∨ B Btwn C A ∨ C Btwn A B ↔ ∀ i ∈ 1 … N ∀ j ∈ 1 … N B ⁡ i − A ⁡ i ⁢ C ⁡ j − A ⁡ j = B ⁡ j − A ⁡ j ⁢ C ⁡ i − A ⁡ i

Proof

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