---

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

.....antecedent..... 
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
⊢ ab ⊥ pd
BY
{ ((Assert ab ⊥ dp BY (D 0 With ⌜d⌝  THEN Auto)) THEN EAuto 3) }

---

Latex:

---

Latex:
.....antecedent..... 
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)
20.  p  \mneq{}  d
21.  p  \mneq{}  d1
\mvdash{}  ab  \mbot{}  pd


By

---

Latex:
((Assert  ab  \mbot{}  dp  BY  (D  0  With  \mkleeneopen{}d\mkleeneclose{}    THEN  Auto))  THEN  EAuto  3)

---

Home Index