Step
*
1
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)
20. p ≠ d
21. p ≠ d1
⊢ False
BY
{ (InstLemma `geo-perp-unicity` [⌜e⌝;⌜a⌝;⌜b⌝;⌜p⌝;⌜d⌝;⌜d1⌝]⋅ THENA Auto) }
1
.....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
2
.....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 ⊥ pd1
3
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
22. d ≡ 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)
20. p \mneq{} d
21. p \mneq{} d1
\mvdash{} False
By
Latex:
(InstLemma `geo-perp-unicity` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}d1\mkleeneclose{}]\mcdot{} THENA Auto)
Home
Index