---

Step * 1 of Lemma eu-colinear-is-colinear-set


1. e : EuclideanPlane
2. A : Point
3. B : Point
4. C : Point
5. Colinear(A;B;C)
6. i : ℤ
7. i = 0 ∈ ℤ
8. B@0 : Point
9. i1 : ℕ
10. i1 < 3
11. ¬(i1 = 0 ∈ ℤ)
12. ¬(i1 = 1 ∈ ℤ)
13. i1 = 2 ∈ ℤ
14. C@0 : Point
15. i2 : ℕ
16. i2 < 3
17. ¬(i2 = 0 ∈ ℤ)
18. i2 = 1 ∈ ℤ
19. ¬(A = C ∈ Point)
⊢ Colinear(A;C;B)
BY
{ (FLemma `eu-colinear-cycle` [5] THEN Auto THEN BLemma `eu-colinear-swap` THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  A  :  Point
3.  B  :  Point
4.  C  :  Point
5.  Colinear(A;B;C)
6.  i  :  \mBbbZ{}
7.  i  =  0
8.  B@0  :  Point
9.  i1  :  \mBbbN{}
10.  i1  <  3
11.  \mneg{}(i1  =  0)
12.  \mneg{}(i1  =  1)
13.  i1  =  2
14.  C@0  :  Point
15.  i2  :  \mBbbN{}
16.  i2  <  3
17.  \mneg{}(i2  =  0)
18.  i2  =  1
19.  \mneg{}(A  =  C)
\mvdash{}  Colinear(A;C;B)


By

---

Latex:
(FLemma  `eu-colinear-cycle`  [5]  THEN  Auto  THEN  BLemma  `eu-colinear-swap`  THEN  Auto)

---

Home Index