---

Step * 1 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
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
BY
{ (((StableCases ⌜p ≠ d⌝⋅ THENA Auto) THEN Try ((Fold `geo-eq` (-1) THEN D -2 THEN RWO  "-1" 0 THEN Auto)))
   THEN (StableCases ⌜p ≠ d1⌝⋅ THENA Auto)
   THEN Try ((Fold `geo-eq` (-1) THEN D -3 THEN RWO  "-1" 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)
20. p ≠ d
21. p ≠ d1
⊢ 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
13.  d  :  Point
14.  a=d=b
15.  ab    \mbot{}d  dp
16.  d1  :  Point
17.  b=d1=c
18.  bc    \mbot{}d1  d1p
19.  \mneg{}Colinear(p;a;b)
\mvdash{}  False


By

---

Latex:
(((StableCases  \mkleeneopen{}p  \mneq{}  d\mkleeneclose{}\mcdot{}  THENA  Auto)
    THEN  Try  ((Fold  `geo-eq`  (-1)  THEN  D  -2  THEN  RWO    "-1"  0  THEN  Auto))
    )
  THEN  (StableCases  \mkleeneopen{}p  \mneq{}  d1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((Fold  `geo-eq`  (-1)  THEN  D  -3  THEN  RWO    "-1"  0  THEN  Auto)))

---

Home Index