---

Step * 1 1 of Lemma no-three-colinear-on-circle


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. b ≠ a
5. c : Point
6. c ≠ a
7. c ≠ b
8. Colinear(a;b;c)
9. p : Point
10. pa ≅ pb
11. pb ≅ pc
12. p # ab
⊢ False
BY
{ ((((InstLemma `Euclid-midpoint` [⌜e⌝;⌜a⌝;⌜b⌝]⋅ THENA Auto) THEN D -1)
    THEN (Using [`c',⌜p⌝] (FLemma `midpoint-of-equidistant-points-is-perp` [-1])⋅ THENA Auto)
    )
   THEN ((InstLemma `Euclid-midpoint` [⌜e⌝;⌜b⌝;⌜c⌝]⋅ THENA Auto) THEN D -1)
   THEN (Using [`c',⌜p⌝] (FLemma `midpoint-of-equidistant-points-is-perp` [-1])⋅ THENA Auto)
   THEN (Assert ¬Colinear(p;a;b) BY
               (RWO "not-lsep-iff-colinear<" 0 THEN Auto))) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. b ≠ a
5. c : Point
6. c ≠ a
7. c ≠ b
8. Colinear(a;b;c)
9. p : Point
10. pa ≅ pb
11. pb ≅ pc
12. p # ab
13. d : Point
14. a=d=b
15. ab  ⊥d dp
16. d1 : Point
17. b=d1=c
18. bc  ⊥d1 d1p
19. ¬Colinear(p;a;b)
⊢ False

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  b  \mneq{}  a
5.  c  :  Point
6.  c  \mneq{}  a
7.  c  \mneq{}  b
8.  Colinear(a;b;c)
9.  p  :  Point
10.  pa  \mcong{}  pb
11.  pb  \mcong{}  pc
12.  p  \#  ab
\mvdash{}  False


By

---

Latex:
((((InstLemma  `Euclid-midpoint`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)
    THEN  (Using  [`c',\mkleeneopen{}p\mkleeneclose{}]  (FLemma  `midpoint-of-equidistant-points-is-perp`  [-1])\mcdot{}  THENA  Auto)
    )
  THEN  ((InstLemma  `Euclid-midpoint`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)
  THEN  (Using  [`c',\mkleeneopen{}p\mkleeneclose{}]  (FLemma  `midpoint-of-equidistant-points-is-perp`  [-1])\mcdot{}  THENA  Auto)
  THEN  (Assert  \mneg{}Colinear(p;a;b)  BY
                          (RWO  "not-lsep-iff-colinear<"  0  THEN  Auto)))

---

Home Index