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→ABtwnBC∨BBtwnCA∨CBtwnAB↔∀i∈1…N∀j∈1…NB⁡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→ABtwnBC↔∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i
2 brbtwn2 ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N→BBtwnCA↔∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∧∀i∈1…N∀j∈1…NC⁡i−B⁡i⁢A⁡j−B⁡j=C⁡j−B⁡j⁢A⁡i−B⁡i
3 2 3comr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnCA↔∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∧∀i∈1…N∀j∈1…NC⁡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…NC⁡i−B⁡i⁢A⁡j−B⁡j=C⁡j−B⁡j⁢A⁡i−B⁡i↔∀i∈1…N∀j∈1…NB⁡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…NC⁡i−B⁡i⁢A⁡j−B⁡j=C⁡j−B⁡j⁢A⁡i−B⁡i↔∀i∈1…N∀j∈1…NB⁡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…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∧∀i∈1…N∀j∈1…NC⁡i−B⁡i⁢A⁡j−B⁡j=C⁡j−B⁡j⁢A⁡i−B⁡i↔∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∧∀i∈1…N∀j∈1…NB⁡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→BBtwnCA↔∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i
8 brbtwn2 ⊢C∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N→CBtwnAB↔∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NA⁡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…NA⁡i−C⁡i⁢B⁡j−C⁡j=A⁡j−C⁡j⁢B⁡i−C⁡i↔∀i∈1…N∀j∈1…NB⁡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…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NA⁡i−C⁡i⁢B⁡j−C⁡j=A⁡j−C⁡j⁢B⁡i−C⁡i↔∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡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→CBtwnAB↔∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i
12 11 3coml ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→CBtwnAB↔∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡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→ABtwnBC∨BBtwnCA∨CBtwnAB↔∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡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…NB⁡i−C⁡i⁢C⁡i−C⁡i≤0
27 26 3adant1 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→∀i∈1…NB⁡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…NB⁡i−C⁡i⁢C⁡i−C⁡i≤0↔∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0
34 27 33 syl5ibcom ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→C=A→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0
35 3mix1 ⊢∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0
36 34 35 syl6 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→C=A→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0
37 36 a1dd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→C=A→∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡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…NC⁡p=A⁡p
41 38 39 40 syl2anc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→C=A↔∀p∈1…NC⁡p=A⁡p
42 41 necon3abid ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→C≠A↔¬∀p∈1…NC⁡p=A⁡p
43 df-ne ⊢C⁡p≠A⁡p↔¬C⁡p=A⁡p
44 43 rexbii ⊢∃p∈1…NC⁡p≠A⁡p↔∃p∈1…N¬C⁡p=A⁡p
45 rexnal ⊢∃p∈1…N¬C⁡p=A⁡p↔¬∀p∈1…NC⁡p=A⁡p
46 44 45 bitr2i ⊢¬∀p∈1…NC⁡p=A⁡p↔∃p∈1…NC⁡p≠A⁡p
47 42 46 bitrdi ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→C≠A↔∃p∈1…NC⁡p≠A⁡p
48 ralcom ⊢∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔∀j∈1…N∀i∈1…NB⁡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…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔∀i∈1…NB⁡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…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→∀i∈1…NB⁡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…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→∀i∈1…NB⁡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⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i↔B⁡p−A⁡pC⁡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⁡pC⁡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⁡pC⁡p−A⁡p⁢C⁡i−A⁡i∈ℂ
99 subadd2 ⊢B⁡i∈ℂ∧A⁡i∈ℂ∧B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i∈ℂ→B⁡i−A⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i↔B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i=B⁡i
100 99 bicomd ⊢B⁡i∈ℂ∧A⁡i∈ℂ∧B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i∈ℂ→B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i=B⁡i↔B⁡i−A⁡i=B⁡p−A⁡pC⁡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⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i=B⁡i↔B⁡i−A⁡i=B⁡p−A⁡pC⁡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⁡iC⁡p−A⁡p=B⁡p−A⁡pC⁡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⁡iC⁡p−A⁡p↔B⁡i−A⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i
104 eqcom ⊢B⁡i−A⁡i=B⁡p−A⁡p⁢C⁡i−A⁡iC⁡p−A⁡p↔B⁡p−A⁡p⁢C⁡i−A⁡iC⁡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⁡iC⁡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⁡iC⁡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 bitrid ⊢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⁡iC⁡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⁡pC⁡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 bitrid ⊢A⁡i∈ℂ∧B⁡i∈ℂ∧C⁡i∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠A⁡p→B⁡i=B⁡p−A⁡pC⁡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⁡pC⁡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…NB⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i↔∀i∈1…NB⁡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⁡pC⁡p−A⁡p∈ℝ
129 colinearalglem4 ⊢A∈𝔼⁡N∧C∈𝔼⁡N∧B⁡p−A⁡pC⁡p−A⁡p∈ℝ→∀i∈1…NB⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i-A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i⁢A⁡i−B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i≤0∨∀i∈1…NA⁡i−C⁡i⁢B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i-C⁡i≤0
130 oveq1 ⊢B⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i→B⁡i−A⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i-A⁡i
131 130 oveq1d ⊢B⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i→B⁡i−A⁡i⁢C⁡i−A⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i-A⁡i⁢C⁡i−A⁡i
132 131 breq1d ⊢B⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i→B⁡i−A⁡i⁢C⁡i−A⁡i≤0↔B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i-A⁡i⁢C⁡i−A⁡i≤0
133 132 ralimi ⊢∀i∈1…NB⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0↔B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i-A⁡i⁢C⁡i−A⁡i≤0
134 ralbi ⊢∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0↔B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i-A⁡i⁢C⁡i−A⁡i≤0→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0↔∀i∈1…NB⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i-A⁡i⁢C⁡i−A⁡i≤0
135 133 134 syl ⊢∀i∈1…NB⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0↔∀i∈1…NB⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i-A⁡i⁢C⁡i−A⁡i≤0
136 oveq2 ⊢B⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i→C⁡i−B⁡i=C⁡i−B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i
137 oveq2 ⊢B⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i→A⁡i−B⁡i=A⁡i−B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i
138 136 137 oveq12d ⊢B⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i→C⁡i−B⁡i⁢A⁡i−B⁡i=C⁡i−B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i⁢A⁡i−B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i
139 138 breq1d ⊢B⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i→C⁡i−B⁡i⁢A⁡i−B⁡i≤0↔C⁡i−B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i⁢A⁡i−B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i≤0
140 139 ralimi ⊢∀i∈1…NB⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i→∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0↔C⁡i−B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i⁢A⁡i−B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i≤0
141 ralbi ⊢∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0↔C⁡i−B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i⁢A⁡i−B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i≤0→∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0↔∀i∈1…NC⁡i−B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i⁢A⁡i−B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i≤0
142 140 141 syl ⊢∀i∈1…NB⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i→∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0↔∀i∈1…NC⁡i−B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i⁢A⁡i−B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i≤0
143 oveq1 ⊢B⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i→B⁡i−C⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i-C⁡i
144 143 oveq2d ⊢B⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i→A⁡i−C⁡i⁢B⁡i−C⁡i=A⁡i−C⁡i⁢B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i-C⁡i
145 144 breq1d ⊢B⁡i=B⁡p−A⁡pC⁡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⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i-C⁡i≤0
146 145 ralimi ⊢∀i∈1…NB⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i→∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0↔A⁡i−C⁡i⁢B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i-C⁡i≤0
147 ralbi ⊢∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0↔A⁡i−C⁡i⁢B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i-C⁡i≤0→∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0↔∀i∈1…NA⁡i−C⁡i⁢B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i-C⁡i≤0
148 146 147 syl ⊢∀i∈1…NB⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i→∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0↔∀i∈1…NA⁡i−C⁡i⁢B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i-C⁡i≤0
149 135 142 148 3orbi123d ⊢∀i∈1…NB⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0↔∀i∈1…NB⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i-A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i⁢A⁡i−B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i≤0∨∀i∈1…NA⁡i−C⁡i⁢B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i-C⁡i≤0
150 129 149 syl5ibrcom ⊢A∈𝔼⁡N∧C∈𝔼⁡N∧B⁡p−A⁡pC⁡p−A⁡p∈ℝ→∀i∈1…NB⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡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…NB⁡i=B⁡p−A⁡pC⁡p−A⁡p⁢C⁡i−A⁡i+A⁡i→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡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…NB⁡i−A⁡i⁢C⁡p−A⁡p=B⁡p−A⁡p⁢C⁡i−A⁡i→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡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…NB⁡i−A⁡i⁢C⁡p−A⁡p=B⁡p−A⁡p⁢C⁡i−A⁡i→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡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…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0
155 48 154 biimtrid ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧C⁡p≠A⁡p→∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0
156 155 rexlimdvaa ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→∃p∈1…NC⁡p≠A⁡p→∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡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…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0
158 37 157 pm2.61dne ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0
159 158 pm4.71rd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i
160 andir ⊢∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i
161 160 orbi1i ⊢∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i
162 df-3or ⊢∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0↔∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0
163 162 anbi1i ⊢∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i
164 andir ⊢∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i
165 163 164 bitri ⊢∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i
166 df-3or ⊢∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i
167 161 165 166 3bitr4i ⊢∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡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…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i∨∀i∈1…NC⁡i−B⁡i⁢A⁡i−B⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i∨∀i∈1…NA⁡i−C⁡i⁢B⁡i−C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔∀i∈1…N∀j∈1…NB⁡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→ABtwnBC∨BBtwnCA∨CBtwnAB↔∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i