---

Step * of Lemma eu-colinear-transitivity

∀e:EuclideanPlane
  ∀[A,C,B,D:Point].  (Colinear(A;B;C) ⇒ Colinear(B;C;D) ⇒ {((¬(A = C ∈ Point)) ⇒ Colinear(A;C;D)) ∧ Colinear(A;B;D)})
BY
{ ((Auto THEN (Assert ¬(B = C ∈ Point) BY (RWO "eu-colinear-def" 7 THEN Auto)))
   THEN (D 0 THEN Auto)
   THEN Unhide
   THEN Auto
   THEN ColinearCases 6
   THEN Try ((D 8 THEN Eq))
   THEN Try ((D 9 THEN Eq))
   THEN Thin 6
   THEN Try (((Eliminate ⌜C⌝⋅ THENA Auto) THEN BLemma `eu-colinear-swap` THEN Complete (Auto)))
   THEN (ColinearCases 6 THEN Try ((Eliminate ⌜D⌝⋅ THENA Auto)))
   THEN (Try (Complete ((BLemma `eu-between-eq-implies-colinear` THEN Auto)))
         THEN Try (Complete ((BLemma `eu-between-eq-implies-colinear2` THEN Auto)))
         )
   THEN Try (Complete (((BLemma `eu-colinear-swap` THENA Auto) THEN BLemma `eu-between-eq-implies-colinear` THEN Auto)))
   THEN ...
   THEN Try (Complete ((BLemma `eu-colinear-permute`
                        THEN Auto
                        THEN BLemma `eu-colinear-swap`
                        THEN Auto
                        THEN BLemma `eu-between-eq-implies-colinear`
                        THEN Auto)))) }

1
1. e : EuclideanPlane
2. A : Point
3. C : Point
4. B : Point
5. D : Point
6. Colinear(B;C;D)
7. ¬(B = C ∈ Point)
8. ¬(A = C ∈ Point)
9. ¬(A = B ∈ Point)
10. C-A-B
11. ¬(B = C ∈ Point)
12. B-D-C
⊢ Colinear(A;C;D)

2
1. e : EuclideanPlane
2. A : Point
3. C : Point
4. B : Point
5. D : Point
6. Colinear(B;C;D)
7. ¬(B = C ∈ Point)
8. ¬(A = C ∈ Point)
9. ¬(A = B ∈ Point)
10. A-C-B
11. ¬(B = C ∈ Point)
12. B-C-D
⊢ Colinear(A;C;D)

3
1. e : EuclideanPlane
2. A : Point
3. C : Point
4. B : Point
5. D : Point
6. Colinear(B;C;D)
7. ¬(B = C ∈ Point)
8. ¬(A = C ∈ Point)
9. ¬(A = B ∈ Point)
10. A-B-C
11. ¬(B = C ∈ Point)
12. D-B-C
⊢ Colinear(A;C;D)

4
1. e : EuclideanPlane
2. A : Point
3. C : Point
4. B : Point
5. D : Point
6. Colinear(B;C;D)
7. ¬(B = C ∈ Point)
8. ¬(A = B ∈ Point)
9. C-A-B
10. ¬(B = C ∈ Point)
11. B-D-C
⊢ Colinear(A;B;D)

5
1. e : EuclideanPlane
2. A : Point
3. C : Point
4. B : Point
5. D : Point
6. Colinear(B;C;D)
7. ¬(B = C ∈ Point)
8. ¬(A = B ∈ Point)
9. A-C-B
10. ¬(B = C ∈ Point)
11. B-C-D
⊢ Colinear(A;B;D)

6
1. e : EuclideanPlane
2. A : Point
3. C : Point
4. B : Point
5. D : Point
6. Colinear(B;C;D)
7. ¬(B = C ∈ Point)
8. ¬(A = B ∈ Point)
9. A-B-C
10. ¬(B = C ∈ Point)
11. D-B-C
⊢ Colinear(A;B;D)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane
    \mforall{}[A,C,B,D:Point].
        (Colinear(A;B;C)  {}\mRightarrow{}  Colinear(B;C;D)  {}\mRightarrow{}  \{((\mneg{}(A  =  C))  {}\mRightarrow{}  Colinear(A;C;D))  \mwedge{}  Colinear(A;B;D)\})


By

---

Latex:
((Auto  THEN  (Assert  \mneg{}(B  =  C)  BY  (RWO  "eu-colinear-def"  7  THEN  Auto)))
  THEN  (D  0  THEN  Auto)
  THEN  Unhide
  THEN  Auto
  THEN  ColinearCases  6
  THEN  Try  ((D  8  THEN  Eq))
  THEN  Try  ((D  9  THEN  Eq))
  THEN  Thin  6
  THEN  Try  (((Eliminate  \mkleeneopen{}C\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  BLemma  `eu-colinear-swap`  THEN  Complete  (Auto)))
  THEN  (ColinearCases  6  THEN  Try  ((Eliminate  \mkleeneopen{}D\mkleeneclose{}\mcdot{}  THENA  Auto)))
  THEN  (Try  (Complete  ((BLemma  `eu-between-eq-implies-colinear`  THEN  Auto)))
              THEN  Try  (Complete  ((BLemma  `eu-between-eq-implies-colinear2`  THEN  Auto)))
              )
  THEN  Try  (Complete  (((BLemma  `eu-colinear-swap`  THENA  Auto)
                                            THEN  BLemma  `eu-between-eq-implies-colinear`
                                            THEN  Auto)))
  THEN  Try  (Complete  (((BLemma  `eu-colinear-swap`  THENA  Auto)
                                            THEN  BLemma  `eu-between-eq-implies-colinear2`
                                            THEN  Auto)))
  THEN  Try  (Complete  ((BLemma  `eu-colinear-permute`
                                            THEN  Auto
                                            THEN  BLemma  `eu-colinear-swap`
                                            THEN  Auto
                                            THEN  BLemma  `eu-between-eq-implies-colinear`
                                            THEN  Auto))))

---

Home Index